defpred S_{1}[ Element of NAT , set ] means $2 = (H . $1) . x;

A1: for n being Element of NAT ex y being Element of COMPLEX st S_{1}[n,y]

A2: for n being Element of NAT holds S_{1}[n,f . n]
from FUNCT_2:sch 3(A1);

take f ; :: thesis: for n being Nat holds f . n = (H . n) . x

let n be Nat; :: thesis: f . n = (H . n) . x

n in NAT by ORDINAL1:def 12;

hence f . n = (H . n) . x by A2; :: thesis: verum

A1: for n being Element of NAT ex y being Element of COMPLEX st S

proof

consider f being sequence of COMPLEX such that
let n be Element of NAT ; :: thesis: ex y being Element of COMPLEX st S_{1}[n,y]

(H . n) . x in COMPLEX by XCMPLX_0:def 2;

hence ex y being Element of COMPLEX st S_{1}[n,y]
; :: thesis: verum

end;(H . n) . x in COMPLEX by XCMPLX_0:def 2;

hence ex y being Element of COMPLEX st S

A2: for n being Element of NAT holds S

take f ; :: thesis: for n being Nat holds f . n = (H . n) . x

let n be Nat; :: thesis: f . n = (H . n) . x

n in NAT by ORDINAL1:def 12;

hence f . n = (H . n) . x by A2; :: thesis: verum