deffunc H₁( Nat) -> Element of REAL = In ((Entropy (Line (MR,$1))),REAL);
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 Nat st k in dom p holds
p . k = Entropy (Line (MR,k)) ) )
thus len p = len MR by A1; :: thesis: for k being Nat st k in dom p holds
p . k = Entropy (Line (MR,k))
let k be Nat; :: thesis: ( k in dom p implies p . k = Entropy (Line (MR,k)) )
assume k in dom p ; :: thesis: p . k = Entropy (Line (MR,k))
then p . k = H₁(k) by A2;
hence p . k = Entropy (Line (MR,k)) ; :: thesis: verum