deffunc H₂( set ) -> quasi-term of C = (((In $1,Vars ) -term C) at f) at g;
consider h being Function such that
A0: dom h = (dom f) \/ (dom g) and
A1: for x being set 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 set ; :: 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 set such that
A2: ( x in dom h & y = h . x ) by FUNCT_1:def 5;
y = H₂(x) by A0, A1, A2;
hence y in QuasiTerms C by ELEMENT; :: thesis: verum

end;

then reconsider h = h as valuation of C by A0, RELSET_1:11;
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 A0; :: 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 A0, A1;
hence h . x = ((x -term C) at f) at g by FUNCT_7:def 1; :: thesis: verum