deffunc H1( object ) -> object = 'not' (p . $1);
consider q being Function such that
A1: dom q = dom p and
A2: for x being object st x in dom p holds
q . x = H1(x) from FUNCT_1:sch 3();
 q is boolean-valued
proof
let x be object ; :: according to TARSKI:def 3,MARGREL1:def 16 :: thesis: ( not x in rng q or x in BOOLEAN )
assume x in rng q ; :: thesis: x in BOOLEAN
then consider y being object such that
A3: y in dom q and
A4: x = q . y by FUNCT_1:def 3;
x = 'not' (p . y) by A1, A2, A3, A4;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def 3;
hence x in BOOLEAN ; :: thesis: verum
end;
hence ex b1 being boolean-valued Function st
( dom b1 = dom p & ( for x being object st x in dom p holds
b1 . x = 'not' (p . x) ) ) by A1, A2; :: thesis: verum