set f = { [x,(x -term C)] where x is variable : x in X } ;
defpred S₁[ variable, set ] means $2 = $1 -term C;

AA: now

let x be variable; :: thesis: ex t being Element of QuasiTerms C st S₁[x,t]
reconsider t = x -term C as Element of QuasiTerms C by ELEMENT;
take t = t; :: thesis: S₁[x,t]
thus S₁[x,t] ; :: thesis: verum

end;

consider g being Function of Vars ,(QuasiTerms C) such that
A0: for x being variable holds S₁[x,g . x] from FUNCT_2:sch 3(AA);
{ [x,(x -term C)] where x is variable : x in X } c= g

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,(x -term C)] where x is variable : x in X } or a in g )
assume a in { [x,(x -term C)] where x is variable : x in X } ; :: thesis: a in g
then consider x being variable such that
A2: ( a = [x,(x -term C)] & x in X ) ;
( g . x = x -term C & dom g = Vars ) by A0, FUNCT_2:def 1;
hence a in g by A2, FUNCT_1:8; :: thesis: verum

end;

hence { [x,(x -term C)] where x is variable : x in X } is valuation of C by RELSET_1:4; :: thesis: verum