let F1, F2 be Function of (Class (PropRel Q)),(Class (PropRel Q)); :: thesis: ( ( 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) ; :: thesis: F1 = F2

now

let x be set ; :: thesis: ( x in Class (PropRel Q) implies F1 . x = F2 . x )
assume x in Class (PropRel Q) ; :: thesis: F1 . x = F2 . x
then consider p being Element of Prop Q such that
A11: x = Class (PropRel Q),p by EQREL_1:45;
F1 . x = Class (PropRel Q),('not' p) by A9, A11;
hence F1 . x = F2 . x by A10, A11; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:18; :: thesis: verum