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 A2: for h being Element of G holds u1 . h = - h ; :: thesis: ( ex h being Element of G st not u2 . h = - h or u1 = u2 )
assume A3: for h being Element of G holds u2 . h = - h ; :: thesis: u1 = u2
now :: thesis: for h being Element of G holds u1 . h = u2 . h
let h be Element of G; :: thesis: u1 . h = u2 . h
thus u1 . h = - h by A2
.= u2 . h by A3 ; :: thesis: verum
end;
hence u1 = u2 ; :: thesis: verum