deffunc H₂( object ) -> quasi-term of C = (((In ($1,Vars)) -term C) at f) at g;
consider h being Function such that
A1: dom h = (dom f) \/ (dom g) and
A2: for x being object st x in (dom f) \/ (dom g) holds
h . x = H₂(x) from FUNCT_1:sch 3();
rng h c= QuasiTerms C

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in QuasiTerms C )
assume y in rng h ; :: thesis: y in QuasiTerms C
then consider x being object such that
A3: x in dom h and
A4: y = h . x by FUNCT_1:def 3;
y = H₂(x) by A1, A2, A3, A4;
hence y in QuasiTerms C by Def28; :: thesis: verum

end;

then reconsider h = h as valuation of C by A1, RELSET_1:4;
take h ; :: thesis: ( dom h = (dom f) \/ (dom g) & ( for x being variable st x in dom h holds
h . x = ((x -term C) at f) at g ) )
thus dom h = (dom f) \/ (dom g) by A1; :: thesis: for x being variable st x in dom h holds
h . x = ((x -term C) at f) at g
let x be variable; :: thesis: ( x in dom h implies h . x = ((x -term C) at f) at g )
assume x in dom h ; :: thesis: h . x = ((x -term C) at f) at g
then h . x = H₂(x) by A1, A2;
hence h . x = ((x -term C) at f) at g ; :: thesis: verum