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 Def6;
len (Col ((M @),i)) = len (M @) by Def8;
then A2: len (Col ((M @),i)) = width M by Def6;
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 :: thesis: for j being Nat st j in dom (Col ((M @),i)) holds
(Line (M,i)) . j = (Col ((M @),i)) . j

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, Def7, ZFMISC_1:87;
hence (Line (M,i)) . j = (M @) * (j,i) by Def6
.= (Col ((M @),i)) . j by A1, A3, A7, A6, Def8 ;
:: thesis: verum

end;

len (Line (M,i)) = width M by Def7;
hence Line (M,i) = Col ((M @),i) by A2, A5, FINSEQ_2:9; :: thesis: verum