let p1, p2 be FinSequence of REAL ; :: thesis: ( len p1 = len MR & ( for k being Element of NAT st k in dom p1 holds
p1 . k = Entropy (Line MR,k) ) & len p2 = len MR & ( for k being Element of NAT st k in dom p2 holds
p2 . k = Entropy (Line MR,k) ) implies p1 = p2 )
assume that
A4: ( len p1 = len MR & ( for k being Element of NAT st k in dom p1 holds
p1 . k = Entropy (Line MR,k) ) ) and
A5: ( len p2 = len MR & ( for k being Element of NAT st k in dom p2 holds
p2 . k = Entropy (Line MR,k) ) ) ; :: thesis: p1 = p2
A6: dom p1 = dom p2 by A4, A5, FINSEQ_3:31;

now

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

end;

hence p1 = p2 by A6, FINSEQ_1:17; :: thesis: verum