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