let F1, F2 be Function of (Class (PropRel Q)),(Class (PropRel Q)); ( ( for p being Element of Prop Q holds F1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) & ( for p being Element of Prop Q holds F2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) implies F1 = F2 )
assume that
A9:
for p being Element of Prop Q holds F1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p))
and
A10:
for p being Element of Prop Q holds F2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p))
; F1 = F2
hence
F1 = F2
by FUNCT_2:12; verum