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;
B1: for x, y1, y2 being set st x in OwnSymbolsOf S & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( x in OwnSymbolsOf S & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume x in OwnSymbolsOf S ; :: thesis: ( not S₁[x,y1] or not S₁[x,y2] or y1 = y2 )
then reconsider s = x as own Element of S by FOMODEL1:def 19;
assume S₁[x,y1] ; :: thesis: ( not S₁[x,y2] or y1 = y2 )
then C1: y1 = X -freeInterpreter s ;
assume S₁[x,y2] ; :: thesis: y1 = y2
hence y1 = y2 by C1; :: thesis: verum

end;

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 FUNCT_1:sch 2(B1, 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;