set n = |.(ar s).|;

set D = |.(ar s).| -tuples_on U;

set h = |.(ar s).| -tuple2Class E;

set IT = f quotient E;

reconsider EE = |.(ar s).| -placesOf E as Equivalence_Relation of (|.(ar s).| -tuples_on U) ;

reconsider hr = |.(ar s).| -tuple2Class E as Relation ;

set D = |.(ar s).| -tuples_on U;

set h = |.(ar s).| -tuple2Class E;

set IT = f quotient E;

reconsider EE = |.(ar s).| -placesOf E as Equivalence_Relation of (|.(ar s).| -tuples_on U) ;

reconsider hr = |.(ar s).| -tuple2Class E as Relation ;

per cases
( not s is relational or s is relational )
;

end;

suppose A1:
not s is relational
; :: thesis: f quotient E is Interpreter of s, Class E

then reconsider g = f as EE,E -respecting Function of (|.(ar s).| -tuples_on U),U by Def10, FOMODEL2:def 2;

reconsider e = g quotient (EE,E) as Function of (Class EE),(Class E) ;

reconsider er = e as Relation ;

reconsider gr = g as Relation ;

f quotient E = e * (|.(ar s).| -tuple2Class E) by Def15, A1;

hence f quotient E is Interpreter of s, Class E by A1, FOMODEL2:def 2; :: thesis: verum

end;reconsider e = g quotient (EE,E) as Function of (Class EE),(Class E) ;

reconsider er = e as Relation ;

reconsider gr = g as Relation ;

f quotient E = e * (|.(ar s).| -tuple2Class E) by Def15, A1;

hence f quotient E is Interpreter of s, Class E by A1, FOMODEL2:def 2; :: thesis: verum

suppose A2:
s is relational
; :: thesis: f quotient E is Interpreter of s, Class E

then reconsider g = f as EE, id BOOLEAN -respecting Function of (|.(ar s).| -tuples_on U),BOOLEAN by Def10, FOMODEL2:def 2;

reconsider pr = peeler BOOLEAN as Relation ;

reconsider e = g quotient (EE,(id BOOLEAN)) as Function of (Class EE),{_{BOOLEAN}_} ;

reconsider er = e as Relation ;

reconsider gr = g as Relation ;

f quotient E = (peeler BOOLEAN) * (e * (|.(ar s).| -tuple2Class E)) by A2, Def15;

hence f quotient E is Interpreter of s, Class E by A2, FOMODEL2:def 2; :: thesis: verum

end;reconsider pr = peeler BOOLEAN as Relation ;

reconsider e = g quotient (EE,(id BOOLEAN)) as Function of (Class EE),{_{BOOLEAN}_} ;

reconsider er = e as Relation ;

reconsider gr = g as Relation ;

f quotient E = (peeler BOOLEAN) * (e * (|.(ar s).| -tuple2Class E)) by A2, Def15;

hence f quotient E is Interpreter of s, Class E by A2, FOMODEL2:def 2; :: thesis: verum