deffunc H_{1}( Nat) -> number = a #Q (s . $1);

consider s1 being Real_Sequence such that

A1: for n being Nat holds s1 . n = H_{1}(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

consider s1 being Real_Sequence such that

A1: for n being Nat holds s1 . n = H

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