deffunc H₁( Nat) -> Real = Entropy (Line MR,$1);
consider p being FinSequence of REAL such that
A1: len p = len MR and
A2: for k being Nat st k in dom p holds
p . k = H₁(k) from FINSEQ_2:sch 1();
take p ; :: thesis: ( len p = len MR & ( for k being Element of NAT st k in dom p holds
p . k = Entropy (Line MR,k) ) )
thus ( len p = len MR & ( for k being Element of NAT st k in dom p holds
p . k = Entropy (Line MR,k) ) ) by A1, A2; :: thesis: verum