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

now

let x be Element of REAL ; :: thesis: G1 . x = G2 . x
( G1 . x = x ^2 & G2 . x = x ^2 & x = x ) by A2;
hence G1 . x = G2 . x ; :: thesis: verum

end;

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