A2: for t being Element of NAT ex ff being Element of COMPLEX st P1[t,ff]
proof
let t be Element of NAT ; :: thesis: ex ff being Element of COMPLEX st P1[t,ff]
consider g being Complex such that
A3: P1[t,g] by A1;
reconsider g = g as Element of COMPLEX by XCMPLX_0:def 2;
take g ; :: thesis: P1[t,g]
thus P1[t,g] by A3; :: thesis: verum
end;
consider f being sequence of COMPLEX such that
A4: for t being Element of NAT holds P1[t,f . t] from FUNCT_2:sch 3(A2);
 reconsider s = f as Complex_Sequence ;
take s ; :: thesis: for n being Nat holds P1[n,s . n]
let n be Nat; :: thesis: P1[n,s . n]
n in NAT by ORDINAL1:def 12;
hence P1[n,s . n] by A4; :: thesis: verum