let M1, M2 be Matrix of REAL; :: thesis:
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))))) ; :: thesis:
A20: dom M1 = dom M2 by A16, A18, FINSEQ_3:29;

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

end;