deffunc H₁( Nat) -> Element of REAL = In (|.(p /. $1).|,REAL);
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).| ) )
A3: dom p = dom q by A1, FINSEQ_3:29;
thus len q = len p by A1; :: thesis: for n being Element of NAT st n in dom p holds
q /. n = |.(p /. n).|
let n be Element of NAT ; :: thesis: ( n in dom p implies q /. n = |.(p /. n).| )
assume A4: n in dom p ; :: thesis: q /. n = |.(p /. n).|
In (|.(p /. n).|,REAL) = |.(p /. n).| ;
hence q /. n = |.(p /. n).| by A2, A3, A4; :: thesis: verum