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