let IT1, IT2 be Function of COMPLEX,COMPLEX; :: thesis: ( ( for z being complex number holds IT1 . z = z + 1 ) & ( for z being complex number holds IT2 . z = z + 1 ) implies IT1 = IT2 )
assume B1: for z being complex number holds IT1 . z = z + 1 ; :: thesis: ( ex z being complex number st not IT2 . z = z + 1 or IT1 = IT2 )
assume B2: for z being complex number holds IT2 . z = z + 1 ; :: thesis: IT1 = IT2

now

let zz be Element of COMPLEX ; :: thesis: IT1 . zz = IT2 . zz
thus IT1 . zz = zz + 1 by B1
.= IT2 . zz by B2 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum