let f1, f2 be Function of COMPLEX , COMPLEX ; :: thesis: ( ( for z being complex number holds f1 . z = Sum (z ExpSeq ) ) & ( for z being complex number holds f2 . z = Sum (z ExpSeq ) ) implies f1 = f2 )
assume A5: for z being complex number holds f1 . z = Sum (z ExpSeq ) ; :: thesis: ( ex z being complex number st not f2 . z = Sum (z ExpSeq ) or f1 = f2 )
assume A6: for z being complex number holds f2 . z = Sum (z ExpSeq ) ; :: thesis: f1 = f2
for z being Element of COMPLEX holds f1 . z = f2 . z

proof

let z be Element of COMPLEX ; :: thesis: f1 . z = f2 . z
thus f1 . z = Sum (z ExpSeq ) by A5
.= f2 . z by A6 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:113; :: thesis: verum