deffunc H₁( Element of NAT ) -> Element of REAL = (g . $1) . x;
consider f being Real_Sequence such that
A1: for i being Element of NAT holds f . i = H₁(i) from FUNCT_2:sch 4();
take f ; :: thesis: for i being Nat holds f . i = (g . i) . x

hereby :: thesis: verum

let i be Nat; :: thesis: f . i = (g . i) . x
i in NAT by ORDINAL1:def 12;
hence f . i = (g . i) . x by A1; :: thesis: verum

end;