deffunc H₁( object ) -> object = (p . $1) '&' (q . $1);
consider s being Function such that
A13: dom s = (dom p) /\ (dom q) and
A14: for x being object st x in (dom p) /\ (dom q) holds
s . x = H₁(x) from FUNCT_1:sch 3();
s is boolean-valued

proof

let x be object ; :: according to TARSKI:def 3,MARGREL1:def 16 :: thesis: ( not x in rng s or x in BOOLEAN )
assume x in rng s ; :: thesis: x in BOOLEAN
then consider y being object such that
A15: y in dom s and
A16: x = s . y by FUNCT_1:def 3;
x = (p . y) '&' (q . y) by A13, A14, A15, A16;
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) /\ (dom q) & ( for x being object st x in dom b₁ holds
b₁ . x = (p . x) '&' (q . x) ) ) by A13, A14; :: thesis: verum