let o1, o2 be UnOp of {0,1,2}; :: thesis: ( ( for a being Element of {0,1,2} holds o1 . a = - a ) & ( for a being Element of {0,1,2} holds o2 . a = - a ) implies o1 = o2 )

assume that

A5: for a being Element of {0,1,2} holds o1 . a = - a and

A6: for a being Element of {0,1,2} holds o2 . a = - a ; :: thesis: o1 = o2

assume that

A5: for a being Element of {0,1,2} holds o1 . a = - a and

A6: for a being Element of {0,1,2} holds o2 . a = - a ; :: thesis: o1 = o2

now :: thesis: for a being Element of {0,1,2} holds o1 . a = o2 . a

hence
o1 = o2
by FUNCT_2:63; :: thesis: verumlet a be Element of {0,1,2}; :: thesis: o1 . a = o2 . a

thus o1 . a = - a by A5

.= o2 . a by A6 ; :: thesis: verum

end;thus o1 . a = - a by A5

.= o2 . a by A6 ; :: thesis: verum