deffunc H₁( set ) -> set = (p . $1) 'xor' (q . $1);
consider s being Function such that
A9: dom s = (dom p) /\ (dom q) and
A10: for x being set st x in (dom p) /\ (dom q) holds
s . x = H₁(x) from FUNCT_1:sch 3();
take s ; :: thesis: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'xor' (q . x) ) )
thus ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'xor' (q . x) ) ) by A9, A10; :: thesis: verum