deffunc H₁( object ) -> set = f . $1;
deffunc H₂( object ) -> set = g . $1;
defpred S₁[ object ] means $1 in dom g;
thus ex F being Function st
( dom F = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( S₁[x] implies F . x = H₂(x) ) & ( not S₁[x] implies F . x = H₁(x) ) ) ) ) from PARTFUN1:sch 1(); :: thesis: verum