let D be non empty set ; :: thesis: for M being Matrix of D
for j being Nat st j in Seg (width M) holds
Line ((M @),j) = Col (M,j)
let M be Matrix of D; :: thesis: for j being Nat st j in Seg (width M) holds
Line ((M @),j) = Col (M,j)
let j be Nat; :: thesis: ( j in Seg (width M) implies Line ((M @),j) = Col (M,j) )
assume A1: j in Seg (width M) ; :: thesis: Line ((M @),j) = Col (M,j)
then j in Seg (len (M @)) by Def6;
then A2: j in dom (M @) by FINSEQ_1:def 3;
per cases ( len M = 0 or len M > 0 ) ;
suppose A3: len M = 0 ; :: thesis: Line ((M @),j) = Col (M,j)
then Seg (len M) = {} ;
hence Line ((M @),j) = Col (M,j) by A1, A3, Def3; :: thesis: verum
end;
suppose A4: len M > 0 ; :: thesis: Line ((M @),j) = Col (M,j)
per cases ( width M = 0 or width M > 0 ) ;
suppose width M = 0 ; :: thesis: Line ((M @),j) = Col (M,j)
hence Line ((M @),j) = Col (M,j) by A1; :: thesis: verum
end;
suppose width M > 0 ; :: thesis: Line ((M @),j) = Col (M,j)
then (M @) @ = M by A4, Th57;
hence Line ((M @),j) = Col (M,j) by A2, Th58; :: thesis: verum
end;
end;
end;
end;