let z1, z2 be AlgSequence of F_Complex; :: thesis: ( ( for i being Element of NAT holds z1 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) & ( for i being Element of NAT holds z2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) implies z1 = z2 )
assume A4: for i being Element of NAT holds z1 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; :: thesis: ( ex i being Element of NAT st not z2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') or z1 = z2 )
assume A5: for i being Element of NAT holds z2 . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; :: thesis: z1 = z2

A6: now :: thesis: for x being object st x in dom z1 holds
z1 . x = z2 . x

let x be object ; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume x in dom z1 ; :: thesis: z1 . x = z2 . x
then reconsider x9 = x as Element of NAT ;
thus z1 . x = ((power F_Complex) . ((- (1_ F_Complex)),x9)) * ((f . x9) *') by A4
.= z2 . x by A5 ; :: thesis: verum

end;

dom z1 = NAT by FUNCT_2:def 1
.= dom z2 by FUNCT_2:def 1 ;
hence z1 = z2 by A6, FUNCT_1:2; :: thesis: verum