defpred S₁[ object , object ] means ex n being Element of NAT st
( n = $1 & $2 = ((power F_Complex) . ((- (1_ F_Complex)),n)) * ((f . n) *') );
A1: for x being object st x in NAT holds
ex y being object st
( y in the carrier of F_Complex & S₁[x,y] )

proof

let u be object ; :: thesis: ( u in NAT implies ex y being object st
( y in the carrier of F_Complex & S₁[u,y] ) )
assume u in NAT ; :: thesis: ex y being object st
( y in the carrier of F_Complex & S₁[u,y] )
then reconsider u9 = u as Element of NAT ;
take ((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *') ; :: thesis: ( ((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *') in the carrier of F_Complex & S₁[u,((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *')] )
thus ( ((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *') in the carrier of F_Complex & S₁[u,((power F_Complex) . ((- (1_ F_Complex)),u9)) * ((f . u9) *')] ) ; :: thesis: verum

end;

consider g being sequence of the carrier of F_Complex such that
A2: for x being object st x in NAT holds
S₁[x,g . x] from FUNCT_2:sch 1(A1);
reconsider g = g as sequence of F_Complex ;
ex n being Nat st
for i being Nat st i >= n holds
g . i = 0. F_Complex

proof

take n = len f; :: thesis: for i being Nat st i >= n holds
g . i = 0. F_Complex

now :: thesis: for i being Nat st i >= n holds
g . i = 0. F_Complex

let i be Nat; :: thesis: ( i >= n implies g . i = 0. F_Complex )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
assume A3: i >= n ; :: thesis: g . i = 0. F_Complex
ex m being Element of NAT st
( m = i1 & g . i1 = ((power F_Complex) . ((- (1_ F_Complex)),m)) * ((f . m) *') ) by A2;
hence g . i = ((power F_Complex) . ((- (1_ F_Complex)),i1)) * ((0. F_Complex) *') by A3, ALGSEQ_1:8
.= 0. F_Complex by COMPLFLD:47 ;
:: thesis: verum

end;

hence for i being Nat st i >= n holds
g . i = 0. F_Complex ; :: thesis: verum

end;

then reconsider p = g as AlgSequence of F_Complex by ALGSEQ_1:def 1;
take p ; :: thesis: for i being Element of NAT holds p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *')

now :: thesis: for i being Element of NAT holds p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *')

let i be Element of NAT ; :: thesis: p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *')
ex n being Element of NAT st
( n = i & p . i = ((power F_Complex) . ((- (1_ F_Complex)),n)) * ((f . n) *') ) by A2;
hence p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; :: thesis: verum

end;

hence for i being Element of NAT holds p . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; :: thesis: verum