let p1, p2 be FinSequence of REAL ; :: thesis: ( len p1 = len MR & ( for k being Nat st k in dom p1 holds
p1 . k = Entropy (Line (MR,k)) ) & len p2 = len MR & ( for k being Nat st k in dom p2 holds
p2 . k = Entropy (Line (MR,k)) ) implies p1 = p2 )
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: p1 = p2
A7: dom p1 = dom p2 by A3, A5, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom p1 holds
p1 . k = p2 . k

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

end;

hence p1 = p2 by A7, FINSEQ_1:13; :: thesis: verum