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]

let x be object ; :: thesis:
assume x in OwnSymbolsOf S ; :: thesis:
then reconsider s = x as own Element of S by FOMODEL1:def 19;
take y = the Interpreter of s,U; :: thesis:
take s ; :: thesis:
thus ( x = s & y is Interpreter of s,U ) ; :: thesis:

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:
thus for s being own Element of S holds f . s is Interpreter of s,U :: thesis:

let s be own Element of S; :: thesis:
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:

end;