set O = OwnSymbolsOf S;
defpred S₁[ object , object ] means ex s being own Element of S st
( $1 = s & $2 is Interpreter of s,U );
A1: 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 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
A2: ( dom f = OwnSymbolsOf S & ( for s being object st s in OwnSymbolsOf S holds
S₁[s,f . s] ) ) from CLASSES1:sch 1(A1);
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
consider s1 being own Element of S such that
A3: ( s = s1 & f . s is Interpreter of s1,U ) by A2, FOMODEL1:def 19;
thus f . s is Interpreter of s,U by A3; :: thesis: verum

end;