deffunc H₁( object ) -> object = (p . $1) 'or' (q . $1);
consider s being Function such that
A1: ( dom s = (dom p) /\ (dom q) & ( 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
A2: ( y in dom s & x = s . y ) by FUNCT_1:def 3;
x = (p . y) 'or' (q . y) by A1, A2;
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) 'or' (q . x) ) ) by A1; :: thesis: verum