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 MATRIX_1:def 7;
then A2: j in dom (M @) by FINSEQ_1:def 3;

per cases ( len M = 0 or len M > 0 ) ;

suppose S: len M = 0 ; :: thesis: Line ((M @),j) = Col (M,j)

then Seg (len M) = {} ;
hence Line ((M @),j) = Col (M,j) by A1, MATRIX_1:def 4, S; :: thesis: verum

end;

suppose A3: 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 A3, Th15;
hence Line ((M @),j) = Col (M,j) by A2, Th16; :: thesis: verum

end;

end;

end;

end;