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 A3: 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 A4: 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 A3
.= f2 . z by A4 ; :: thesis: verum

end;

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