deffunc H₁( Nat) -> Element of REAL = |.(p /. $1).|;
consider q being FinSequence of REAL such that
A1: len q = len p and
A2: for n being Nat st n in dom q holds
q /. n = H₁(n) from FINSEQ_4:sch 2();
take q ; :: thesis: ( len q = len p & ( for n being Element of NAT st n in dom p holds
q /. n = |.(p /. n).| ) )
dom p = dom q by A1, FINSEQ_3:29;
hence ( len q = len p & ( for n being Element of NAT st n in dom p holds
q /. n = |.(p /. n).| ) ) by A1, A2; :: thesis: verum