let p1, p2 be FinSequence of REAL ; :: thesis:
assume that
A3: len p1 = len MR and
A4: for k being Nat st k in dom p1 holds
p1 . k = Entropy (Line (MR,k)) and
A5: len p2 = len MR and
A6: for k being Nat st k in dom p2 holds
p2 . k = Entropy (Line (MR,k)) ; :: thesis:
A7: dom p1 = dom p2 by A3, A5, FINSEQ_3:29;

let k be Nat; :: thesis:
assume A8: k in dom p1 ; :: thesis:
thus p1 . k = Entropy (Line (MR,k)) by A4, A8
.= p2 . k by A6, A7, A8 ; :: thesis:

end;