set O = OwnSymbolsOf S;

set SS = AllSymbolsOf S;

defpred S_{1}[ 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_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2

ex y being object st S_{1}[x,y]

A4: ( dom f = OwnSymbolsOf S & ( for x being object st x in OwnSymbolsOf S holds

S_{1}[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

set SS = AllSymbolsOf S;

defpred S

$2 = X -freeInterpreter s;

A1: for x, y1, y2 being object st x in OwnSymbolsOf S & S

y1 = y2

proof

A3:
for x being object st x in OwnSymbolsOf S holds
let x, y1, y2 be object ; :: thesis: ( x in OwnSymbolsOf S & S_{1}[x,y1] & S_{1}[x,y2] implies y1 = y2 )

assume x in OwnSymbolsOf S ; :: thesis: ( not S_{1}[x,y1] or not S_{1}[x,y2] or y1 = y2 )

then reconsider s = x as own Element of S by FOMODEL1:def 19;

assume S_{1}[x,y1]
; :: thesis: ( not S_{1}[x,y2] or y1 = y2 )

then A2: y1 = X -freeInterpreter s ;

assume S_{1}[x,y2]
; :: thesis: y1 = y2

hence y1 = y2 by A2; :: thesis: verum

end;assume x in OwnSymbolsOf S ; :: thesis: ( not S

then reconsider s = x as own Element of S by FOMODEL1:def 19;

assume S

then A2: y1 = X -freeInterpreter s ;

assume S

hence y1 = y2 by A2; :: thesis: verum

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in OwnSymbolsOf S implies ex y being object st S_{1}[x,y] )

assume x in OwnSymbolsOf S ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider s = x as own Element of S by FOMODEL1:def 19;

take yy = X -freeInterpreter s; :: thesis: S_{1}[x,yy]

thus for ss being own Element of S st x = ss holds

yy = X -freeInterpreter ss ; :: thesis: verum

end;assume x in OwnSymbolsOf S ; :: thesis: ex y being object st S

then reconsider s = x as own Element of S by FOMODEL1:def 19;

take yy = X -freeInterpreter s; :: thesis: S

thus for ss being own Element of S st x = ss holds

yy = X -freeInterpreter ss ; :: thesis: verum

A4: ( dom f = OwnSymbolsOf S & ( for x being object st x in OwnSymbolsOf S holds

S

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