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
A14: ( 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)) ) ) and
A15: ( 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)) ) ) ; :: thesis: M1 = M2
A16: dom M1 = dom M2 by A14, A15, FINSEQ_3:31;

now

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

end;

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