let M1, M2 be Matrix of REAL; ( len M1 = len MR & width M1 = width MR & ( for k being 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 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 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 Nat st k in dom M2 holds
M2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k)))))
; M1 = M2
A20:
dom M1 = dom M2
by A16, A18, FINSEQ_3:29;
hence
M1 = M2
by A20, FINSEQ_1:13; verum