let f1, f2 be UnOp of (Pr D); :: thesis: ( ( for p being PartialPredicate of D holds f1 . p = PP_not p ) & ( for p being PartialPredicate of D holds f2 . p = PP_not p ) implies f1 = f2 )
assume that
A11: for p being PartialPredicate of D holds f1 . p = PP_not p and
A12: for p being PartialPredicate of D holds f2 . p = PP_not p ; :: thesis: f1 = f2
let x be Element of Pr D; :: according to FUNCT_2:def 8 :: thesis: f1 . x = f2 . x
reconsider x1 = x as PartialPredicate of D by PARTFUN1:46;
thus f1 . x = PP_not x1 by A11
.= f2 . x by A12 ; :: thesis: verum