let D be non empty set ; :: thesis: for M being Matrix of D
for i being Nat st i in dom M holds
Line M,i = Col (M @ ),i
let M be Matrix of D; :: thesis: for i being Nat st i in dom M holds
Line M,i = Col (M @ ),i
let i be Nat; :: thesis: ( i in dom M implies Line M,i = Col (M @ ),i )
assume A1: i in dom M ; :: thesis: Line M,i = Col (M @ ),i
A2: ( len (Line M,i) = width M & ( for j being Nat st j in Seg (width M) holds
(Line M,i) . j = M * i,j ) ) by MATRIX_1:def 8;
A3: ( len (Col (M @ ),i) = len (M @ ) & ( for j being Nat st j in dom (M @ ) holds
(Col (M @ ),i) . j = (M @ ) * j,i ) ) by MATRIX_1:def 9;
A4: len (M @ ) = width M by MATRIX_1:def 7;
A5: len (Col (M @ ),i) = width M by A3, MATRIX_1:def 7;
then X: dom (Col (M @ ),i) = Seg (width M) by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom (Col (M @ ),i) implies (Line M,i) . j = (Col (M @ ),i) . j )
assume A6: j in dom (Col (M @ ),i) ; :: thesis: (Line M,i) . j = (Col (M @ ),i) . j
then A7: (Line M,i) . j = M * i,j by X, MATRIX_1:def 8;
A8: [i,j] in Indices M by A1, A6, X, ZFMISC_1:106;
A9: dom (M @ ) = Seg (len (M @ )) by FINSEQ_1:def 3;
thus (Line M,i) . j = (M @ ) * j,i by A7, A8, MATRIX_1:def 7
.= (Col (M @ ),i) . j by A4, A6, A9, X, MATRIX_1:def 9 ; :: thesis: verum

end;

hence Line M,i = Col (M @ ),i by A2, A5, FINSEQ_2:10; :: thesis: verum