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

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

let x be Element of REAL ; :: 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