let D, E be non empty set ; :: thesis: for M being Matrix of D
for L being Matrix of E
for i being Nat st M = L & i in dom M holds
Line (M,i) = Line (L,i)
let M be Matrix of D; :: thesis: for L being Matrix of E
for i being Nat st M = L & i in dom M holds
Line (M,i) = Line (L,i)
let L be Matrix of E; :: thesis: for i being Nat st M = L & i in dom M holds
Line (M,i) = Line (L,i)
let i be Nat; :: thesis: ( M = L & i in dom M implies Line (M,i) = Line (L,i) )
assume AS1: ( M = L & i in dom M ) ; :: thesis: Line (M,i) = Line (L,i)
A1: ( 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_0:def 7;
A2: ( len (Line (L,i)) = width L & ( for j being Nat st j in Seg (width L) holds
(Line (L,i)) . j = L * (i,j) ) ) by MATRIX_0:def 7;
A3: dom (Line (M,i)) = Seg (width M) by A1, FINSEQ_1:def 3
.= dom (Line (L,i)) by AS1, A2, FINSEQ_1:def 3 ;
for j being Nat st j in dom (Line (M,i)) holds
(Line (M,i)) . j = (Line (L,i)) . j

proof

let j be Nat; :: thesis: ( j in dom (Line (M,i)) implies (Line (M,i)) . j = (Line (L,i)) . j )
assume j in dom (Line (M,i)) ; :: thesis: (Line (M,i)) . j = (Line (L,i)) . j
then A4: j in Seg (width M) by FINSEQ_1:def 3, A1;
then [i,j] in Indices M by AS1, ZFMISC_1:87;
then A5: M * (i,j) = L * (i,j) by AS1, EQ2;
thus (Line (M,i)) . j = M * (i,j) by A4, MATRIX_0:def 7
.= (Line (L,i)) . j by AS1, A4, A5, MATRIX_0:def 7 ; :: thesis: verum

end;

hence Line (M,i) = Line (L,i) by A3; :: thesis: verum