let G1, G2 be UnOp of COMPLEX; :: thesis: ( ( for c being Complex holds G1 . c = c ^2 ) & ( for c being Complex holds G2 . c = c ^2 ) implies G1 = G2 )
assume that
A2: for c being Complex holds G1 . c = c ^2 and
A3: for c being Complex holds G2 . c = c ^2 ; :: thesis: G1 = G2

now :: thesis: for x being Element of COMPLEX holds G1 . x = G2 . x

let x be Element of COMPLEX ; :: thesis: G1 . x = G2 . x
G1 . x = x ^2 by A2;
hence G1 . x = G2 . x by A3; :: thesis: verum

end;

hence G1 = G2 by FUNCT_2:63; :: thesis: verum