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
A7: for p being Element of Prop Q holds F1 . (Class (PropRel Q),p) = Class (PropRel Q),('not' p) and
A8: 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
A9: x = Class (PropRel Q),p by EQREL_1:45;
( F1 . x = Class (PropRel Q),('not' p) & F2 . x = Class (PropRel Q),('not' p) ) by A7, A8, A9;
hence F1 . x = F2 . x ; :: thesis: verum

end;

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