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 )
A1: len (M @ ) = width M by MATRIX_1:def 7;
len (Col (M @ ),i) = len (M @ ) by MATRIX_1:def 9;
then A2: len (Col (M @ ),i) = width M by MATRIX_1:def 7;
then A3: dom (Col (M @ ),i) = Seg (width M) by FINSEQ_1:def 3;
assume A4: i in dom M ; :: thesis: Line M,i = Col (M @ ),i

A5: now

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

end;

len (Line M,i) = width M by MATRIX_1:def 8;
hence Line M,i = Col (M @ ),i by A2, A5, FINSEQ_2:10; :: thesis: verum