set O = OwnSymbolsOf S;

defpred S_{1}[ 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_{1}[x,y]

A2: ( dom f = OwnSymbolsOf S & ( for s being object st s in OwnSymbolsOf S holds

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

defpred S

( $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

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 y = the Interpreter of s,U; :: thesis: S_{1}[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;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 y = the Interpreter of s,U; :: thesis: S

take s ; :: thesis: ( x = s & y is Interpreter of s,U )

thus ( x = s & y is Interpreter of s,U ) ; :: thesis: verum

A2: ( dom f = OwnSymbolsOf S & ( for s being object st s in OwnSymbolsOf S holds

S

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;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