defpred S1[ 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 & S1[x,y] )
proof
let u be object ; :: thesis: ( u in NAT implies ex y being object st
( y in the carrier of F_Complex & S1[u,y] ) )
assume u in NAT ; :: thesis: ex y being object st
( y in the carrier of F_Complex & S1[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 & S1[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 & S1[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
S1[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