let M1, M2 be Matrix of REAL ; :: thesis: ( len M1 = len MR & width M1 = width MR & ( for k being Element of NAT st k in dom M1 holds
M1 . k = mlt (Line MR,k),(FinSeq_log 2,(Line MR,k)) ) & len M2 = len MR & width M2 = width MR & ( for k being Element of NAT st k in dom M2 holds
M2 . k = mlt (Line MR,k),(FinSeq_log 2,(Line MR,k)) ) implies M1 = M2 )
assume that
A16: len M1 = len MR and
width M1 = width MR and
A17: for k being Element of NAT st k in dom M1 holds
M1 . k = mlt (Line MR,k),(FinSeq_log 2,(Line MR,k)) and
A18: len M2 = len MR and
width M2 = width MR and
A19: for k being Element of NAT st k in dom M2 holds
M2 . k = mlt (Line MR,k),(FinSeq_log 2,(Line MR,k)) ; :: thesis: M1 = M2
A20: dom M1 = dom M2 by A16, A18, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom M1 implies M1 . k = M2 . k )
assume A21: k in dom M1 ; :: thesis: M1 . k = M2 . k
thus M1 . k = mlt (Line MR,k),(FinSeq_log 2,(Line MR,k)) by A17, A21
.= M2 . k by A19, A20, A21 ; :: thesis: verum

end;

hence M1 = M2 by A20, FINSEQ_1:17; :: thesis: verum