deffunc H₁( object ) -> object = (p . $1) => (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();
take s ; :: thesis: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) => (q . x) ) )
thus ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) => (q . x) ) ) by A1; :: thesis: verum