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

A1: now :: thesis: for x being variable ex t being Element of QuasiTerms C st S₁[x,t]

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 Def28;
take t = t; :: thesis: S₁[x,t]
thus S₁[x,t] ; :: thesis: verum

end;

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

proof

let a be object ; :: 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
A3: a = [x,(x -term C)] and
x in X ;
A4: g . x = x -term C by A2;
dom g = Vars by FUNCT_2:def 1;
hence a in g by A3, A4, FUNCT_1:1; :: thesis: verum

end;

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