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

let x be set ; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume x in dom z1 ; :: thesis: z1 . x = z2 . x
then reconsider x' = x as Element of NAT ;
thus z1 . x = ((power F_Complex ) . (- (1_ F_Complex )),x') * ((f . x') *' ) 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:9; :: thesis: verum