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 len M = 0 ; :: thesis: Line (M @ ),j = Col M,j

hence Line (M @ ),j = Col M,j by A1, FINSEQ_1:4, MATRIX_1:def 4; :: 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;