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 :: thesis: for x being object st x in Class (PropRel Q) holds
F1 . x = F2 . x
let x be object ; :: 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:36;
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:12; :: thesis: verum