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 ;
per cases ( not s is relational or s is relational ) ;
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;
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;
end;