let u1, u2 be UnOp of G; :: thesis: ( ( for h being Element of G holds u1 . h = h " ) & ( for h being Element of G holds u2 . h = h " ) implies u1 = u2 )
assume that
A2: for h being Element of G holds u1 . h = h " and
A3: for h being Element of G holds u2 . h = h " ; :: thesis: u1 = u2
let h be Element of G; :: according to FUNCT_2:def 8 :: thesis: u1 . h = u2 . h
thus u1 . h = h " by A2
.= u2 . h by A3 ; :: thesis: verum