set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
defpred S₁[ object , object ] means for s being own Element of S st $1 = s holds
$2 = X -freeInterpreter s;
A1: for x, y1, y2 being object st x in OwnSymbolsOf S & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be object ; :: 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 A2: y1 = X -freeInterpreter s ;
assume S₁[x,y2] ; :: thesis: y1 = y2
hence y1 = y2 by A2; :: thesis: verum

end;

A3: for x being object st x in OwnSymbolsOf S holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in OwnSymbolsOf S implies ex y being object st S₁[x,y] )
assume x in OwnSymbolsOf S ; :: thesis: ex y being object 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
A4: ( dom f = OwnSymbolsOf S & ( for x being object st x in OwnSymbolsOf S holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A1, A3);
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 A4; :: 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 by A4, FOMODEL1:def 19; :: thesis: verum