deffunc H₁( 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 = H₁(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 b₁ being boolean-valued Function st
( dom b₁ = dom p & ( for x being object st x in dom p holds
b₁ . x = 'not' (p . x) ) ) by A1, A2; :: thesis: verum