A2: for t being Element of NAT ex ff being Element of COMPLEX st P₁[t,ff] by A1;
consider f being Function of NAT ,COMPLEX such that
A3: for t being Element of NAT holds P₁[t,f . t] from FUNCT_2:sch 3(A2);
reconsider s = f as Complex_Sequence ;
take s ; :: thesis: for n being Element of NAT holds P₁[n,s . n]
let n be Element of NAT ; :: thesis: P₁[n,s . n]
thus P₁[n,s . n] by A3; :: thesis: verum