deffunc H₁( Nat) -> number = a #Q (s . $1);
consider s1 being Real_Sequence such that
A1: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();
take s1 ; :: thesis: for n being Nat holds s1 . n = a #Q (s . n)
thus for n being Nat holds s1 . n = a #Q (s . n) by A1; :: thesis: verum