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

now :: thesis: for zz being Element of COMPLEX holds IT1 . zz = IT2 . zz

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

end;

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