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;