set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
defpred S₁[ set , set ] means for s being own Element of S st $1 = s holds
$2 = X -freeInterpreter s;
B2: for x being set st x in OwnSymbolsOf S holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in OwnSymbolsOf S implies ex y being set st S₁[x,y] )
assume x in OwnSymbolsOf S ; :: thesis: ex y being set st S₁[x,y]
then reconsider s = x as own Element of S by FOMODEL1:def 19;
take yy = X -freeInterpreter s; :: thesis: S₁[x,yy]
thus for ss being own Element of S st x = ss holds
yy = X -freeInterpreter ss ; :: thesis: verum

end;

consider f being Function such that
B3: ( dom f = OwnSymbolsOf S & ( for x being set st x in OwnSymbolsOf S holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(B2);
take f ; :: thesis: ( dom f = OwnSymbolsOf S & ( for s being own Element of S holds f . s = X -freeInterpreter s ) )
thus dom f = OwnSymbolsOf S by B3; :: thesis: for s being own Element of S holds f . s = X -freeInterpreter s
thus for s being own Element of S holds f . s = X -freeInterpreter s :: thesis: verum

proof

let s be own Element of S; :: thesis: f . s = X -freeInterpreter s
( s in OwnSymbolsOf S & s = s ) by FOMODEL1:def 19;
hence f . s = X -freeInterpreter s by B3; :: thesis: verum

end;