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

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

hence
F1 = F2
by FUNCT_2:12; :: thesis: verumF1 . 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;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