set O = OwnSymbolsOf S;
defpred S₁[ set , set ] means ex s being own Element of S st
( $1 = s & $2 is Interpreter of s,U );
B1: 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 y = the Interpreter of s,U; :: thesis: S₁[x,y]
take s ; :: thesis: ( x = s & y is Interpreter of s,U )
thus ( x = s & y is Interpreter of s,U ) ; :: thesis: verum

end;

consider f being Function such that
B2: ( dom f = OwnSymbolsOf S & ( for s being set st s in OwnSymbolsOf S holds
S₁[s,f . s] ) ) from CLASSES1:sch 1(B1);
take f ; :: thesis: for s being own Element of S holds f . s is Interpreter of s,U
thus for s being own Element of S holds f . s is Interpreter of s,U :: thesis: verum

proof

let s be own Element of S; :: thesis: f . s is Interpreter of s,U
s in OwnSymbolsOf S by FOMODEL1:def 19;
then consider s1 being own Element of S such that
C1: ( s = s1 & f . s is Interpreter of s1,U ) by B2;
thus f . s is Interpreter of s,U by C1; :: thesis: verum

end;