fomodel3.miz



    begin

    reserve A,B,C,X,Y,Z,x,x1,x2,y,z for set,

U,U1,U2,U3 for non empty set,

u,u1,u2 for Element of U,

P,Q,R for Relation,

f,g for Function,

k,m,n for Nat,

m1,n1 for non zero Nat,

kk,mm,nn for Element of NAT ,

p,p1,p2 for FinSequence,

q,q1,q2 for U -valued FinSequence;

    reserve S,S1,S2 for Language,

s,s1,s2 for Element of S,

l,l1,l2 for literal Element of S,

a for ofAtomicFormula Element of S,

r for relational Element of S,

w,w1,w2 for string of S,

t,t1,t2 for termal string of S;

    reserve phi0 for 0wff string of S,

psi,psi1,psi2,phi,phi1,phi2 for wff string of S,

I for S, U -interpreter-like Function;

    reserve tt,tt0,tt1,tt2 for Element of ( AllTermsOf S);

    definition

      let S, s;

      let V be Element of (((( AllSymbolsOf S) * ) \ { {} }) * );

      :: FOMODEL3:def1

      func s -compound (V) -> string of S equals ( <*s*> ^ ((S -multiCat ) . V));

      coherence

      proof

        set SS = ( AllSymbolsOf S), C = (S -multiCat );

        reconsider header = <*s*> as Element of (SS * );

        reconsider tailer = (C . V) as FinSequence of SS by FINSEQ_1:def 11;

        reconsider IT = (header ^ tailer) as FinSequence of SS;

        IT in (SS * ) & not IT in { {} };

        hence ( <*s*> ^ (C . V)) is string of S by XBOOLE_0:def 5;

      end;

    end

    registration

      let S, mm;

      let s be termal Element of S;

      let V be |.( ar s).| -element Element of (((S -termsOfMaxDepth ) . mm) * );

      cluster (s -compound V) -> (mm + 1) -termal;

      coherence

      proof

        set C = (S -multiCat ), t = (s -compound V), T = (S -termsOfMaxDepth ), L = ( LettersOf S), SS = ( AllSymbolsOf S), n = |.( ar s).|, A = ( AtomicTermsOf S), fam = { ( Compound (u,(T . mm))) where u be ofAtomicFormula Element of S : u is operational };

        

         A1: V is FinSequence of (T . mm) by FINSEQ_1:def 11;

        reconsider Ss = ((SS * ) \ { {} }) as Subset of (SS * );

        V in (Ss * );

        then

        reconsider VV = V as Element of ((SS * ) * );

        t = ( <*s*> ^ (C . VV)) & ( rng VV) c= (T . mm) by A1, FINSEQ_1:def 4;

        then

         A2: t in ( Compound (s,(T . mm)));

        per cases ;

          suppose s is literal;

          then

          reconsider v = s as literal Element of S;

          reconsider vv = v as Element of L by FOMODEL1:def 14;

          ( ar v) = 0 ;

          then n = 0 ;

          then

          reconsider VVV = V as 0 -element FinSequence;

          t = ( <*s*> ^ VVV)

          .= <*vv*>;

          then t in ( AtomicTermsOf S) by FINSEQ_2: 98;

          then (T . 0 ) c= (T . ( 0 + (mm + 1))) & t in (T . 0 ) by FOMODEL1:def 30, FOMODEL1: 4;

          hence thesis;

        end;

          suppose not s is literal;

          then ( Compound (s,(T . mm))) in fam;

          then t in ( union fam) by A2, TARSKI:def 4;

          then t in (( union fam) \/ (T . mm)) by XBOOLE_0:def 3;

          then t in (T . (mm + 1)) by FOMODEL1:def 30;

          hence thesis;

        end;

      end;

    end

    

     Lm1: not x in ((S -termsOfMaxDepth ) . (m + n)) implies not x in ((S -termsOfMaxDepth ) . m)

    proof

      set T = (S -termsOfMaxDepth );

      

       A1: (T . m) c= (T . (m + n)) by FOMODEL1: 4;

      assume not x in (T . (m + n));

      hence thesis by A1;

    end;

    

     Lm2: x in ((S -termsOfMaxDepth ) . n) implies { mm : not x in ((S -termsOfMaxDepth ) . mm) } c= n

    proof

      set T = (S -termsOfMaxDepth ), A = { mm : not x in (T . mm) };

      assume

       A1: x in (T . n);

      now

        let y be object;

        assume y in A;

        then

        consider mm such that

         A2: y = mm & not x in (T . mm);

        now

          assume mm >= n;

          then

          consider k such that

           A3: mm = (n + k) by NAT_1: 10;

          thus contradiction by A1, A2, A3, Lm1;

        end;

        hence y in ( Segm n) by A2, NAT_1: 44;

      end;

      hence thesis by TARSKI:def 3;

    end;

    

     Lm3: for V be Element of (( AllTermsOf S) * ) holds ex mm be Element of NAT st V is Element of (((S -termsOfMaxDepth ) . mm) * )

    proof

      set TT = ( AllTermsOf S), T = (S -termsOfMaxDepth );

      let V be Element of (TT * );

      deffunc F( object) = { mm : not (V . $1) in (T . mm) };

      set B = { F(nn) : nn in ( dom V) };

      

       A1: ( dom V) is finite;

      reconsider TF = T as Function;

       A2:

      now

        let x;

        assume x in B;

        then

        consider nn such that

         A3: x = { mm : not (V . nn) in (T . mm) } & nn in ( dom V);

        reconsider D = ( dom V) as non empty set by A3;

        ( rng V) c= TT by RELAT_1:def 19;

        then

        reconsider VV = V as Function of D, TT by FUNCT_2: 2;

        reconsider nnn = nn as Element of D by A3;

        consider kk be Element of NAT such that

         A4: (VV . nnn) in (TF . kk) by FOMODEL1: 5;

        x c= kk by Lm2, A3, A4;

        hence x is finite;

      end;

      B is finite from FRAENKEL:sch 21( A1);

      then

      reconsider BB = B as finite finite-membered set by A2, FINSET_1:def 6;

      reconsider C = ( union BB) as finite set;

      consider x be object such that

       A5: x in ( NAT \ C) by XBOOLE_0:def 1;

      reconsider mm = x as Element of NAT by A5;

      now

        let i be object;

        assume

         A6: i in ( dom V);

        then

        reconsider ii = i as Element of NAT ;

         not (V . i) in (T . mm) implies mm in C

        proof

          assume not (V . i) in (T . mm);

          then mm in F(i) & F(ii) in B by A6;

          hence mm in C by TARSKI:def 4;

        end;

        hence (V . i) in (T . mm) by A5, XBOOLE_0:def 5;

      end;

      then V is Function of ( dom V), (T . mm) by FUNCT_2: 3;

      then V is FinSequence of (T . mm) by FOMODEL0: 26;

      hence thesis;

    end;

    registration

      let S;

      let s be termal Element of S;

      let V be |.( ar s).| -element Element of (( AllTermsOf S) * );

      cluster (s -compound V) -> termal;

      coherence

      proof

        set T = (S -termsOfMaxDepth ), n = |.( ar s).|;

        consider mm such that

         A1: V is Element of ((T . mm) * ) by Lm3;

        reconsider VV = V as n -element Element of ((T . mm) * ) by A1;

        (s -compound VV) is (mm + 1) -termal string of S;

        hence thesis;

      end;

    end

    registration

      let S;

      let s be relational Element of S;

      let V be |.( ar s).| -element Element of (( AllTermsOf S) * );

      cluster (s -compound V) -> 0wff;

      coherence ;

    end

    definition

      let S, s;

      :: FOMODEL3:def2

      func s -compound -> Function of (((( AllSymbolsOf S) * ) \ { {} }) * ), ((( AllSymbolsOf S) * ) \ { {} }) means

      : Def2: for V be Element of (((( AllSymbolsOf S) * ) \ { {} }) * ) holds (it . V) = (s -compound V);

      existence

      proof

        set SS = ( AllSymbolsOf S);

        deffunc F( Element of (((SS * ) \ { {} }) * )) = (s -compound $1);

        consider f be Function of (((SS * ) \ { {} }) * ), ((SS * ) \ { {} }) such that

         A1: for x be Element of (((SS * ) \ { {} }) * ) holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set SS = ( AllSymbolsOf S);

        let IT1,IT2 be Function of (((SS * ) \ { {} }) * ), ((SS * ) \ { {} });

        assume that

         A2: for V be Element of (((SS * ) \ { {} }) * ) holds (IT1 . V) = (s -compound V) and

         A3: for V be Element of (((SS * ) \ { {} }) * ) holds (IT2 . V) = (s -compound V);

        now

          let V be Element of (((SS * ) \ { {} }) * );

          

          thus (IT1 . V) = (s -compound V) by A2

          .= (IT2 . V) by A3;

        end;

        hence IT1 = IT2 by FUNCT_2:def 8;

      end;

    end

    registration

      let S;

      let s be termal Element of S;

      cluster ((s -compound ) | ( |.( ar s).| -tuples_on ( AllTermsOf S))) -> ( AllTermsOf S) -valued;

      coherence

      proof

        set SS = ( AllSymbolsOf S), A = ( AllTermsOf S), n = |.( ar s).|, D = (n -tuples_on A), f = (s -compound ), IT = (f | D);

        now

          let y be object;

          assume y in ( rng IT);

          then y in (f .: D);

          then

          consider x be object such that

           A1: x in ( dom f) & x in D & y = (f . x) by FUNCT_1:def 6;

          reconsider V = x as n -element FinSequence of A by FOMODEL0: 12, A1;

          reconsider VV = V as n -element Element of (A * );

          reconsider Ss = ((SS * ) \ { {} }) as Subset of (SS * );

          VV is Element of (Ss * );

          then (s -compound VV) is termal string of S & VV is Element of ((SS * ) * );

          then (f . VV) is termal string of S by Def2;

          hence y in A by FOMODEL1:def 32, A1;

        end;

        hence thesis by RELAT_1:def 19, TARSKI:def 3;

      end;

    end

    registration

      let S;

      let s be relational Element of S;

      cluster ((s -compound ) | ( |.( ar s).| -tuples_on ( AllTermsOf S))) -> ( AtomicFormulasOf S) -valued;

      coherence

      proof

        set SS = ( AllSymbolsOf S), A = ( AllTermsOf S), n = |.( ar s).|, D = (n -tuples_on A), f = (s -compound ), IT = (f | D), AF = ( AtomicFormulasOf S);

        now

          let y be object;

          assume y in ( rng IT);

          then y in (f .: D);

          then

          consider x be object such that

           A1: x in ( dom f) & x in D & y = (f . x) by FUNCT_1:def 6;

          reconsider V = x as n -element FinSequence of A by FOMODEL0: 12, A1;

          reconsider VV = V as n -element Element of (A * );

          reconsider Ss = ((SS * ) \ { {} }) as Subset of (SS * );

          VV is Element of (Ss * );

          then (s -compound VV) is 0wff string of S & VV is Element of ((SS * ) * );

          then (f . VV) is 0wff string of S by Def2;

          hence y in AF by A1;

        end;

        hence thesis by RELAT_1:def 19, TARSKI:def 3;

      end;

    end

    definition

      let S;

      let s be ofAtomicFormula Element of S;

      let X be set;

      :: FOMODEL3:def3

      func X -freeInterpreter (s) -> set equals

      : Def3: ((s -compound ) | ( |.( ar s).| -tuples_on ( AllTermsOf S))) if not s is relational

      otherwise (((s -compound ) | ( |.( ar s).| -tuples_on ( AllTermsOf S))) * ( chi (X,( AtomicFormulasOf S))) qua Relation);

      coherence ;

      consistency ;

    end

    definition

      let S;

      let s be ofAtomicFormula Element of S;

      let X be set;

      :: original: -freeInterpreter

      redefine

      func X -freeInterpreter (s) -> Interpreter of s, ( AllTermsOf S) ;

      coherence

      proof

        set A = ( AllTermsOf S), n = |.( ar s).|, SS = ( AllSymbolsOf S), XF = (X -freeInterpreter s), AF = ( AtomicFormulasOf S);

        reconsider Ss = ((SS * ) \ { {} }) as Subset of (SS * );

        (n -tuples_on A) c= (A * ) by FINSEQ_2: 142;

        then (n -tuples_on A) c= (Ss * ) by XBOOLE_1: 1;

        then

        reconsider f = ((s -compound ) | (n -tuples_on A)) as Function of (n -tuples_on A), ((SS * ) \ { {} }) by FUNCT_2: 32;

        per cases ;

          suppose

           A1: s is relational;

          then

          reconsider ss = s as relational Element of S;

          ((ss -compound ) | ( |.( ar ss).| -tuples_on A)) is AF -valued;

          then ( rng f) c= AF by RELAT_1:def 19;

          then

          reconsider ff = f as Function of (n -tuples_on A), AF by RELSET_1: 6;

          reconsider g = ( chi (X,AF)) as Function of AF, BOOLEAN ;

          (g * ff) is Function of (n -tuples_on A), BOOLEAN ;

          then XF is Function of (n -tuples_on A), BOOLEAN by A1, Def3;

          hence thesis by A1, FOMODEL2:def 2;

        end;

          suppose

           A2: not s is relational;

          then

          reconsider ss = s as non relational ofAtomicFormula Element of S;

          ((ss -compound ) | ( |.( ar ss).| -tuples_on A)) is A -valued;

          then ( rng f) c= A by RELAT_1:def 19;

          then f is Function of (n -tuples_on A), A by RELSET_1: 6;

          then XF is Function of (n -tuples_on A), A by A2, Def3;

          hence thesis by A2, FOMODEL2:def 2;

        end;

      end;

    end

    definition

      let S, X;

      :: FOMODEL3:def4

      func (S,X) -freeInterpreter -> Function means

      : Def4: ( dom it ) = ( OwnSymbolsOf S) & for s be own Element of S holds (it . s) = (X -freeInterpreter s);

      existence

      proof

        set O = ( OwnSymbolsOf S), SS = ( AllSymbolsOf S);

        defpred P[ object, object] means for s be own Element of S st $1 = s holds $2 = (X -freeInterpreter s);

        

         A1: for x,y1,y2 be object st x in O & P[x, y1] & P[x, y2] holds y1 = y2

        proof

          let x,y1,y2 be object;

          assume x in O;

          then

          reconsider s = x as own Element of S by FOMODEL1:def 19;

          assume P[x, y1];

          then

           A2: y1 = (X -freeInterpreter s);

          assume P[x, y2];

          hence thesis by A2;

        end;

        

         A3: for x be object st x in O holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in O;

          then

          reconsider s = x as own Element of S by FOMODEL1:def 19;

          take yy = (X -freeInterpreter s);

          thus for ss be own Element of S st x = ss holds yy = (X -freeInterpreter ss);

        end;

        consider f be Function such that

         A4: ( dom f) = O & for x be object st x in O holds P[x, (f . x)] from FUNCT_1:sch 2( A1, A3);

        take f;

        thus ( dom f) = O by A4;

        thus for s be own Element of S holds (f . s) = (X -freeInterpreter s) by A4, FOMODEL1:def 19;

      end;

      uniqueness

      proof

        set O = ( OwnSymbolsOf S), SS = ( AllSymbolsOf S);

        let IT1,IT2 be Function;

        assume

         A5: ( dom IT1) = O & for s be own Element of S holds (IT1 . s) = (X -freeInterpreter s);

        assume

         A6: ( dom IT2) = O & for s be own Element of S holds (IT2 . s) = (X -freeInterpreter s);

        now

          thus ( dom IT1) = ( dom IT2) by A5, A6;

          let x be object;

          assume x in ( dom IT1);

          then

          reconsider s = x as own Element of S by FOMODEL1:def 19, A5;

          (IT1 . s) = (X -freeInterpreter s) by A5

          .= (IT2 . s) by A6;

          hence (IT1 . x) = (IT2 . x);

        end;

        hence thesis by FUNCT_1: 2;

      end;

    end

    registration

      let S, X;

      cluster ((S,X) -freeInterpreter ) -> Function-yielding;

      coherence

      proof

        set O = ( OwnSymbolsOf S), IT = ((S,X) -freeInterpreter );

        now

          let x be object;

          assume x in ( dom IT);

          then x in O by Def4;

          then

          reconsider s = x as own Element of S by FOMODEL1:def 19;

          (X -freeInterpreter s) is Function;

          hence (IT . x) is Function by Def4;

        end;

        hence thesis by FUNCOP_1:def 6;

      end;

    end

    definition

      let S, X;

      :: original: -freeInterpreter

      redefine

      func (S,X) -freeInterpreter -> Interpreter of S, ( AllTermsOf S) ;

      coherence

      proof

        set IT = ((S,X) -freeInterpreter ), A = ( AllTermsOf S);

        for s be own Element of S holds (IT . s) is Interpreter of s, A

        proof

          let s be own Element of S;

          (X -freeInterpreter s) is Interpreter of s, A;

          hence thesis by Def4;

        end;

        hence thesis by FOMODEL2:def 3;

      end;

    end

    registration

      let S, X;

      cluster ((S,X) -freeInterpreter ) -> S, ( AllTermsOf S) -interpreter-like;

      coherence ;

    end

    definition

      let S, X;

      :: original: -freeInterpreter

      redefine

      func (S,X) -freeInterpreter -> Element of (( AllTermsOf S) -InterpretersOf S) ;

      coherence

      proof

        set f = ((S,X) -freeInterpreter ), U = ( AllTermsOf S), O = ( OwnSymbolsOf S);

        ( dom f) c= O by Def4;

        then (f | O) = f by RELAT_1: 68;

        hence thesis by FOMODEL2: 2;

      end;

    end

    definition

      let X,Y be non empty set;

      let R be Relation of X, Y;

      let n be Nat;

      :: FOMODEL3:def5

      func n -placesOf R -> Relation of (n -tuples_on X), (n -tuples_on Y) equals { [p, q] where p be Element of (n -tuples_on X), q be Element of (n -tuples_on Y) : for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R };

      coherence

      proof

        set Xn = (n -tuples_on X), Yn = (n -tuples_on Y), IT = { [p, q] where p be Element of (n -tuples_on X), q be Element of (n -tuples_on Y) : for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R };

        now

          let x be object;

          assume x in IT;

          then

          consider p be Element of Xn, q be Element of Yn such that

           A1: x = [p, q] & for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R;

          thus x in [:Xn, Yn:] by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    

     Lm4: for n be zero Nat, X,Y be non empty set, R be Relation of X, Y holds (n -placesOf R) = { [ {} , {} ]}

    proof

      let n be zero Nat;

      let X,Y be non empty set;

      let R be Relation of X, Y;

      set RR = (n -placesOf R);

      

       A1: [:(n -tuples_on X), (n -tuples_on Y):] = [: { {} }, ( 0 -tuples_on Y):] by FOMODEL0: 10

      .= [: { {} }, { {} }:] by FOMODEL0: 10

      .= { [ {} , {} ]} by ZFMISC_1: 29;

       {} in { {} } by TARSKI:def 1;

      then

      reconsider p = {} as Element of (n -tuples_on X) by FOMODEL0: 10;

       {} in { {} } by TARSKI:def 1;

      then

      reconsider q = {} as Element of (n -tuples_on Y) by FOMODEL0: 10;

      for j be set st j in ( Seg 0 ) holds [(p . j), (q . j)] in R;

      then [p, q] in RR;

      then { [ {} , {} ]} c= RR by ZFMISC_1: 31;

      hence RR = { [ {} , {} ]} by A1;

    end;

    registration

      let X,Y be non empty set;

      let R be total Relation of X, Y;

      let n be non zero Nat;

      cluster (n -placesOf R) -> total;

      coherence

      proof

        set RR = (n -placesOf R), XX = (n -tuples_on X);

        

         A1: ( dom R) = X by PARTFUN1:def 2;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        now

          let x be object;

          assume x in XX;

          then

          reconsider xx = x as Element of XX;

          reconsider xxx = xx as Element of ( Funcs (( Seg n),X)) by FOMODEL0: 11;

          defpred P[ set, set] means [(xx . $1), $2] in R;

          

           A2: for m st m in ( Seg n) holds ex d be Element of Y st P[m, d]

          proof

            let m;

            assume m in ( Seg n);

            then

            reconsider mm = m as Element of ( Seg n);

            (xxx . mm) in ( dom R) by A1;

            then

            consider y be object such that

             A3: [(xx . m), y] in R by XTUPLE_0:def 12;

            reconsider yy = y as Element of Y by ZFMISC_1: 87, A3;

            take yy;

            thus thesis by A3;

          end;

          consider f be FinSequence of Y such that

           A4: ( len f) = n & for m st m in ( Seg n) holds P[m, (f /. m)] from FINSEQ_4:sch 1( A2);

          reconsider ff = f as Element of (nn -tuples_on Y) by FINSEQ_2: 133, A4;

          reconsider fff = ff as Element of ( Funcs (( Seg nn),Y)) by FOMODEL0: 11;

          

           A5: ( dom fff) = ( Seg nn) by FUNCT_2:def 1;

          now

            let j be set;

            assume

             A6: j in ( Seg n);

            then

            reconsider jj = j as Element of NAT ;

            jj in ( dom ff) & P[jj, (f /. jj)] by A6, A4, A5;

            hence [(xx . j), (ff . j)] in R by PARTFUN1:def 6;

          end;

          then [xx, ff] in RR;

          hence x in ( dom RR) by XTUPLE_0:def 12;

        end;

        then XX c= ( dom RR) & ( dom RR) c= XX by TARSKI:def 3;

        hence thesis by PARTFUN1:def 2, XBOOLE_0:def 10;

      end;

    end

    registration

      let X,Y be non empty set;

      let R be total Relation of X, Y;

      let n be Nat;

      cluster (n -placesOf R) -> total;

      coherence

      proof

        set RR = (n -placesOf R);

        per cases ;

          suppose n is non zero;

          then

          reconsider nn = n as non zero Nat;

          (nn -placesOf R) is total;

          hence thesis;

        end;

          suppose n is zero;

          then

          reconsider nn = n as zero Nat;

          (nn -placesOf R) = { [ {} , {} ]} by Lm4;

          

          then ( dom RR) = { {} } by RELAT_1: 9

          .= (nn -tuples_on X) by FOMODEL0: 10;

          hence thesis by PARTFUN1:def 2;

        end;

      end;

    end

    registration

      let X,Y be non empty set;

      let R be Relation of X, Y;

      let n be zero Nat;

      cluster (n -placesOf R) -> Function-like;

      coherence

      proof

        set IT = (n -placesOf R);

        reconsider f = { [ {} , {} ]} as Function;

        now

          let x be object;

          assume x in IT;

          then

          consider p be Element of (n -tuples_on X), q be Element of (n -tuples_on Y) such that

           A1: x = [p, q] & for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R;

          p = {} & q = {} ;

          hence x in f by TARSKI:def 1, A1;

        end;

        then

        reconsider ITT = IT as Subset of f by TARSKI:def 3;

        ITT is Function-like;

        hence thesis;

      end;

    end

    definition

      let X be non empty set;

      let R be Relation of X;

      let n be Nat;

      :: FOMODEL3:def6

      func n -placesOf R -> Relation of (n -tuples_on X) equals (n -placesOf R qua Relation of X, X);

      coherence ;

    end

    definition

      let X be non empty set;

      let R be Relation of X;

      let n be zero Nat;

      :: original: -placesOf

      redefine

      :: FOMODEL3:def7

      func n -placesOf R -> Relation of (n -tuples_on X) equals { [ {} , {} ]};

      coherence ;

      compatibility by Lm4;

    end

    

     Lm5: for n be non zero Nat, X be non empty set, x,y be Element of ( Funcs (( Seg n),X)), R be Relation of X holds ( [x, y] in (n -placesOf R) iff for j be Element of ( Seg n) holds [(x . j), (y . j)] in R)

    proof

      let n be non zero Nat, X be non empty set, x,y be Element of ( Funcs (( Seg n),X)), R be Relation of X;

      reconsider xa = x as Element of (n -tuples_on X) by FINSEQ_2: 93;

      reconsider ya = y as Element of (n -tuples_on X) by FINSEQ_2: 93;

      thus [x, y] in (n -placesOf R) implies for j be Element of ( Seg n) holds [(x . j), (y . j)] in R

      proof

        assume [x, y] in (n -placesOf R);

        then

        consider p,q be Element of (n -tuples_on X) such that

         A1: [x, y] = [p, q] & for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R;

        x = p & y = q by A1, XTUPLE_0: 1;

        hence thesis by A1;

      end;

      thus (for j be Element of ( Seg n) holds [(x . j), (y . j)] in R) implies [x, y] in (n -placesOf R)

      proof

        assume for j be Element of ( Seg n) holds [(x . j), (y . j)] in R;

        then for j be set st j in ( Seg n) holds [(xa . j), (ya . j)] in R;

        hence thesis;

      end;

    end;

    

     Lm6: for n be non zero Nat, X be non empty set, r be total symmetric Relation of X holds (n -placesOf r) is symmetric total Relation of (n -tuples_on X)

    proof

      let n be non zero Nat, X be non empty set, r be total symmetric Relation of X;

      

       A1: ( field r) = X by ORDERS_1: 12;

      set R = (n -placesOf r);

      

       A2: ( field R) = (n -tuples_on X) by ORDERS_1: 12;

      now

        let x,y be object;

        assume x in (n -tuples_on X);

        then

        reconsider xa = x as Element of ( Funcs (( Seg n),X)) by FINSEQ_2: 93;

        assume y in (n -tuples_on X);

        then

        reconsider ya = y as Element of ( Funcs (( Seg n),X)) by FINSEQ_2: 93;

        assume

         A3: [x, y] in R;

        now

          let j be Element of ( Seg n);

          (xa . j) in X & (ya . j) in X & [(xa . j), (ya . j)] in r by Lm5, A3;

          hence [(ya . j), (xa . j)] in r by RELAT_2:def 11, A1, RELAT_2:def 3;

        end;

        hence [y, x] in R by Lm5;

      end;

      hence thesis by RELAT_2:def 3, RELAT_2:def 11, A2;

    end;

    

     Lm7: for n be non zero Nat, X be non empty set, r be transitive total Relation of X holds (n -placesOf r) is transitive total Relation of (n -tuples_on X)

    proof

      let n be non zero Nat, X be non empty set, r be transitive total Relation of X;

      

       A1: ( field r) = X by ORDERS_1: 12;

      set R = (n -placesOf r);

      

       A2: ( field R) = (n -tuples_on X) by ORDERS_1: 12;

      now

        let x,y,z be object;

        assume x in (n -tuples_on X);

        then

        reconsider xa = x as Element of ( Funcs (( Seg n),X)) by FINSEQ_2: 93;

        assume y in (n -tuples_on X);

        then

        reconsider ya = y as Element of ( Funcs (( Seg n),X)) by FINSEQ_2: 93;

        assume z in (n -tuples_on X);

        then

        reconsider za = z as Element of ( Funcs (( Seg n),X)) by FINSEQ_2: 93;

        assume

         A3: [x, y] in R;

        assume

         A4: [y, z] in R;

        now

          let j be Element of ( Seg n);

          (xa . j) in X & (ya . j) in X & (za . j) in X & [(xa . j), (ya . j)] in r & [(ya . j), (za . j)] in r by Lm5, A3, A4;

          hence [(xa . j), (za . j)] in r by A1, RELAT_2:def 8, RELAT_2:def 16;

        end;

        hence [x, z] in R by Lm5;

      end;

      hence thesis by RELAT_2:def 8, RELAT_2:def 16, A2;

    end;

    

     Lm8: for n be zero Nat, X be non empty set, r be Relation of X holds (n -placesOf r) is total symmetric transitive

    proof

      let n be zero Nat;

      let X be non empty set;

      let r be Relation of X;

      set R = (n -placesOf r);

      now

        let x be object;

        assume x in (n -tuples_on X);

        then x = {} ;

        then [x, x] in R by TARSKI:def 1;

        hence ex y be object st [x, y] in R;

      end;

      then ( dom R) = (n -tuples_on X) by RELSET_1: 9;

      hence R is total by PARTFUN1:def 2;

      then

       A1: ( field R) = (n -tuples_on X) by ORDERS_1: 12;

      thus R is symmetric

      proof

        let x,y be object;

        assume x in ( field R);

        then

         A2: x = {} by A1;

        assume y in ( field R);

        then

         A3: y = {} by A1;

        assume [x, y] in R;

        thus [y, x] in R by TARSKI:def 1, A2, A3;

      end;

      

       A4: for x,y,z be object st x in (n -tuples_on X) & y in (n -tuples_on X) & z in (n -tuples_on X) & [x, y] in R & [y, z] in R holds [x, z] in R;

      thus thesis by A4, A1, RELAT_2:def 8;

    end;

    registration

      let X be non empty set;

      let R be symmetric total Relation of X;

      let n;

      cluster (n -placesOf R) -> total;

      coherence ;

    end

    registration

      let X be non empty set;

      let R be symmetric total Relation of X;

      let n;

      cluster (n -placesOf R) -> symmetric;

      coherence

      proof

        per cases ;

          suppose n is zero;

          hence thesis by Lm8;

        end;

          suppose not n is zero;

          hence thesis by Lm6;

        end;

      end;

    end

    registration

      let X be non empty set;

      let R be symmetric total Relation of X;

      let n;

      cluster (n -placesOf R) -> symmetric;

      coherence ;

    end

    registration

      let X be non empty set;

      let R be transitive total Relation of X;

      let n;

      cluster (n -placesOf R) -> transitive;

      coherence

      proof

        per cases ;

          suppose n is zero;

          hence thesis by Lm8;

        end;

          suppose not n is zero;

          hence thesis by Lm7;

        end;

      end;

    end

    registration

      let X be non empty set;

      let R be Equivalence_Relation of X;

      let n;

      cluster (n -placesOf R) -> total;

      coherence ;

    end

    definition

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      let R be Relation;

      :: FOMODEL3:def8

      func R quotient (E,F) -> set equals { [e, f] where e be Element of ( Class E), f be Element of ( Class F) : ex x,y be set st x in e & y in f & [x, y] in R };

      coherence ;

    end

    definition

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      let R be Relation;

      :: original: quotient

      redefine

      func R quotient (E,F) -> Relation of ( Class E), ( Class F) ;

      coherence

      proof

        set IT = (R quotient (E,F));

        now

          let x be object;

          assume x in IT;

          then

          consider e be Element of ( Class E), f be Element of ( Class F) such that

           A1: x = [e, f] & ex x,y be set st x in e & y in f & [x, y] in R;

          thus x in [:( Class E), ( Class F):] by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let E be Relation;

      let F be Relation;

      let f be Function;

      :: FOMODEL3:def9

      attr f is E,F -respecting means

      : Def9: for x1,x2 be set holds ( [x1, x2] in E) implies [(f . x1), (f . x2)] in F;

    end

    definition

      let S, U;

      let s be ofAtomicFormula Element of S;

      let E be Relation of U;

      let f be Interpreter of s, U;

      :: FOMODEL3:def10

      attr f is E -respecting means

      : Def10: f is ( |.( ar s).| -placesOf E), E -respecting if not s is relational

      otherwise f is ( |.( ar s).| -placesOf E), ( id BOOLEAN ) -respecting;

      consistency ;

    end

    registration

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      cluster E, F -respecting for Function of X, Y;

      existence

      proof

        consider y be object such that

         A1: y in Y by XBOOLE_0: 7;

        set R = (X --> y);

         {y} c= Y & ( dom R) = X & ( rng R) c= {y} by ZFMISC_1: 31, A1;

        then

        reconsider f = R as Function of X, Y by FUNCT_2: 2;

        now

          let x1,x2 be set;

          assume [x1, x2] in E;

          then x1 in X & x2 in X by ZFMISC_1: 87;

          then

           A2: (f . x1) = y & (f . x2) = y by FUNCOP_1: 7;

          thus [(f . x1), (f . x2)] in F by A2, A1, EQREL_1: 5;

        end;

        then f is E, F -respecting;

        hence thesis;

      end;

    end

    registration

      let S, U;

      let s be ofAtomicFormula Element of S;

      let E be Equivalence_Relation of U;

      cluster E -respecting for Interpreter of s, U;

      existence

      proof

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

        reconsider EE = (n -placesOf E) as Equivalence_Relation of (n -tuples_on U);

        set f = the (n -placesOf E), E -respecting Function of (n -tuples_on U), U;

        set g = the (n -placesOf E), ( id BOOLEAN ) -respecting Function of (n -tuples_on U), BOOLEAN ;

        per cases ;

          suppose

           A1: s is relational;

          then

          reconsider gg = g as Interpreter of s, U by FOMODEL2:def 2;

          gg is E -respecting by Def10, A1;

          hence thesis;

        end;

          suppose

           A2: not s is relational;

          then

          reconsider ff = f as Interpreter of s, U by FOMODEL2:def 2;

          ff is E -respecting by Def10, A2;

          hence thesis;

        end;

      end;

    end

    registration

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      cluster E, F -respecting for Function;

      existence

      proof

        take the E, F -respecting Function of X, Y;

        thus thesis;

      end;

    end

    definition

      let X be non empty set;

      let E be Equivalence_Relation of X;

      let n;

      :: original: -placesOf

      redefine

      func n -placesOf E -> Equivalence_Relation of (n -tuples_on X) ;

      coherence ;

    end

    definition

      let X be non empty set, x be Element of ( SmallestPartition X);

      :: FOMODEL3:def11

      func DeTrivial (x) -> Element of X means

      : Def11: x = {it };

      existence

      proof

        set XX = ( SmallestPartition X);

        consider y be object such that

         A1: x = {y} & y in X by RELSET_2: 1;

        reconsider yy = y as Element of X by A1;

        take yy;

        thus thesis by A1;

      end;

      uniqueness by ZFMISC_1: 3;

    end

    definition

      let X be non empty set;

      :: FOMODEL3:def12

      func peeler (X) -> Function of ( SmallestPartition X), X means

      : Def12: for x be Element of ( SmallestPartition X) holds (it . x) = ( DeTrivial x);

      existence

      proof

        deffunc F( Element of ( SmallestPartition X)) = ( DeTrivial $1);

        consider f be Function of ( SmallestPartition X), X such that

         A1: for x be Element of ( SmallestPartition X) holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function of ( SmallestPartition X), X;

        assume that

         A2: for x be Element of ( SmallestPartition X) holds (IT1 . x) = ( DeTrivial x) and

         A3: for x be Element of ( SmallestPartition X) holds (IT2 . x) = ( DeTrivial x);

        now

          let x be Element of ( SmallestPartition X);

          

          thus (IT1 . x) = ( DeTrivial x) by A2

          .= (IT2 . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      let X be non empty set, EqR be Equivalence_Relation of X;

      cluster -> non empty for Element of ( Class EqR);

      coherence ;

    end

    

     Lm9: for X be non empty set, E be Equivalence_Relation of X, x,y be set, C be Element of ( Class E) st x in C & y in C holds [x, y] in E

    proof

      let X be non empty set, E be Equivalence_Relation of X, x,y be set, C be Element of ( Class E);

      assume

       A1: x in C & y in C;

      reconsider EE = E as transitive Tolerance of X;

      consider xe be object such that

       A2: xe in X & C = ( Class (E,xe)) by EQREL_1:def 3;

      thus thesis by EQREL_1: 22, A1, A2;

    end;

    

     Lm10: for X be non empty set, E be Equivalence_Relation of X, C1,C2 be Element of ( Class E), x1,x2 be set st x1 in C1 & x2 in C2 & [x1, x2] in E holds C1 = C2

    proof

      let X be non empty set, E be Equivalence_Relation of X, C1,C2 be Element of ( Class E), x1,x2 be set;

      reconsider EE = E as Tolerance of X;

      assume

       A1: x1 in C1;

      then

      reconsider x11 = x1 as Element of X;

      x11 in X;

      then x1 in ( Class (EE,x1)) by EQREL_1: 20;

      then

       A2: C1 = ( EqClass (E,x11)) by EQREL_1:def 4, A1, XBOOLE_0: 3;

      assume

       A3: x2 in C2;

      then

      reconsider x22 = x2 as Element of X;

      x22 in X;

      then x2 in ( Class (EE,x2)) by EQREL_1: 20;

      then

       A4: C2 = ( EqClass (E,x22)) by EQREL_1:def 4, A3, XBOOLE_0: 3;

      assume [x1, x2] in E;

      hence thesis by A2, A4, EQREL_1: 35;

    end;

    registration

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      let f be E, F -respecting Function;

      cluster (f quotient (E,F)) -> Function-like;

      coherence

      proof

        set IT = (f quotient (E,F));

        reconsider P = ( Class E) as a_partition of X;

        reconsider EEE = E as Relation of X, X;

        now

          let e,f1,f2 be object;

          assume [e, f1] in IT;

          then

          consider ee1 be Element of ( Class E), ff1 be Element of ( Class F) such that

           A1: [e, f1] = [ee1, ff1] & ex x1,y1 be set st x1 in ee1 & y1 in ff1 & [x1, y1] in f;

          consider x1,y1 be set such that

           A2: x1 in ee1 & y1 in ff1 & [x1, y1] in f by A1;

          assume [e, f2] in IT;

          then

          consider ee2 be Element of ( Class E), ff2 be Element of ( Class F) such that

           A3: [e, f2] = [ee2, ff2] & ex x2,y2 be set st x2 in ee2 & y2 in ff2 & [x2, y2] in f;

          

           A4: ee1 = e & ee2 = e & ff1 = f1 & ff2 = f2 by A1, A3, XTUPLE_0: 1;

          consider x2,y2 be set such that

           A5: x2 in ee2 & y2 in ff2 & [x2, y2] in f by A3;

          

           A6: [x1, x2] in E by Lm9, A2, A5, A4;

          y2 = (f . x2) & y1 = (f . x1) by A5, A2, FUNCT_1: 1;

          then [y1, y2] in F by Def9, A6;

          hence f1 = f2 by A4, A2, A5, Lm10;

        end;

        hence thesis by FUNCT_1:def 1;

      end;

    end

    registration

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      let R be total Relation of X, Y;

      cluster (R quotient (E,F)) -> total;

      coherence

      proof

        set RR = (R quotient (E,F));

        reconsider Q = ( Class F) as a_partition of Y;

        now

          let e be object;

          reconsider ee = e as set by TARSKI: 1;

          assume e in ( Class E);

          then

          reconsider ee = e as Element of ( Class E);

          set xx = the Element of ee;

          reconsider x = xx as Element of X;

          ( dom R) = X by PARTFUN1:def 2;

          then

          consider y be object such that

           A1: [x, y] in R by XTUPLE_0:def 12;

          reconsider yy = y as Element of Y by ZFMISC_1: 87, A1;

          reconsider f = ( EqClass (yy,Q)) as Element of ( Class F);

           [e, f] = [e, f] & x in ee & y in f & [x, y] in R by A1, EQREL_1:def 6;

          then [e, f] in RR;

          hence e in ( dom RR) by XTUPLE_0:def 12;

        end;

        then ( Class E) c= ( dom RR) by TARSKI:def 3;

        hence thesis by PARTFUN1:def 2, XBOOLE_0:def 10;

      end;

    end

    definition

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      let f be E, F -respecting Function of X, Y;

      :: original: quotient

      redefine

      func f quotient (E,F) -> Function of ( Class E), ( Class F) ;

      coherence

      proof

        thus (f quotient (E,F)) is Function of ( Class E), ( Class F);

      end;

    end

    definition

      let X be non empty set, E be Equivalence_Relation of X;

      :: FOMODEL3:def13

      func E -class -> Function of X, ( Class E) means

      : Def13: for x be Element of X holds (it . x) = ( EqClass (E,x));

      existence

      proof

        deffunc F( Element of X) = ( EqClass (E,$1));

        consider f be Function of X, ( Class E) such that

         A1: for x be Element of X holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function of X, ( Class E);

        assume

         A2: for x be Element of X holds (IT1 . x) = ( EqClass (E,x));

        assume

         A3: for x be Element of X holds (IT2 . x) = ( EqClass (E,x));

        now

          let x be Element of X;

          

          thus (IT1 . x) = ( EqClass (E,x)) by A2

          .= (IT2 . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      let X be non empty set, E be Equivalence_Relation of X;

      cluster (E -class ) -> onto;

      coherence

      proof

        set P = (E -class );

        now

          let c be object;

          assume

           A1: c in ( Class E);

          then

          reconsider cc = c as Subset of X;

          consider x be object such that

           A2: x in X & cc = ( Class (E,x)) by EQREL_1:def 3, A1;

          reconsider xx = x as Element of X by A2;

          (P . xx) = cc by A2, Def13;

          hence c in ( rng P) by FUNCT_2: 4;

        end;

        then ( Class E) c= ( rng P) & ( rng P) c= ( Class E) by RELAT_1:def 19, TARSKI:def 3;

        hence thesis by FUNCT_2:def 3, XBOOLE_0:def 10;

      end;

    end

    registration

      let X,Y be non empty set;

      cluster onto for Relation of X, Y;

      existence

      proof

         [:X, Y:] c= [:X, Y:];

        then

        reconsider R = [:X, Y:] as Relation of X, Y;

        ( rng R) = Y;

        then R is onto by FUNCT_2:def 3;

        hence thesis;

      end;

    end

    registration

      let Y be non empty set;

      cluster onto for Y -valued Relation;

      existence

      proof

        take the onto Relation of Y, Y;

        thus thesis;

      end;

    end

    registration

      let Y be non empty set, R be Y -valued Relation;

      cluster (R ~ ) -> Y -defined;

      coherence

      proof

        ( rng R) c= Y & ( dom (R ~ )) = ( rng R) by RELAT_1: 20;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let Y be non empty set, R be ontoY -valued Relation;

      cluster (R ~ ) -> total;

      coherence

      proof

        ( dom (R ~ )) = ( rng R) by RELAT_1: 20

        .= Y by FUNCT_2:def 3;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let X,Y be non empty set, R be onto Relation of X, Y;

      cluster (R ~ ) -> total;

      coherence ;

    end

    registration

      let Y be non empty set;

      let R be ontoY -valued Relation;

      cluster (R ~ ) -> total;

      coherence ;

    end

    

     Lm11: for E be Equivalence_Relation of U, n be non zero Nat holds ((n -placesOf ((E -class ) qua Relation of U, ( Class E) ~ )) * ((n -placesOf E) -class )) is Function-like

    proof

      let E be Equivalence_Relation of U, n be non zero Nat;

      set En = (n -placesOf E);

      reconsider f1 = (E -class ) as Function of U, ( Class E);

      reconsider r1 = (E -class ) as Relation of U, ( Class E);

      reconsider r2 = (r1 ~ ) as Relation of ( Class E), U;

      reconsider r3 = (n -placesOf r2) as Relation of (n -tuples_on ( Class E)), (n -tuples_on U);

      reconsider f4 = (En -class ) as Function of (n -tuples_on U), ( Class (n -placesOf E));

      reconsider r4 = f4 as Relation of (n -tuples_on U), ( Class (n -placesOf E));

      now

        let x,z1,z2 be object;

        assume

         A1: [x, z1] in (r3 * r4) & [x, z2] in (r3 * r4);

        consider y1 be object such that

         A2: [x, y1] in r3 & [y1, z1] in r4 by A1, RELAT_1:def 8;

        consider y2 be object such that

         A3: [x, y2] in r3 & [y2, z2] in r4 by A1, RELAT_1:def 8;

        

         A4: (f4 . y1) = z1 & (f4 . y2) = z2 by FUNCT_1: 1, A2, A3;

        reconsider y11 = y1, y22 = y2 as Element of (n -tuples_on U) by ZFMISC_1: 87, A2, A3;

        consider p1 be Element of (n -tuples_on ( Class E)), q1 be Element of (n -tuples_on U) such that

         A5: [x, y1] = [p1, q1] & for j be set st j in ( Seg n) holds [(p1 . j), (q1 . j)] in r2 by A2;

        consider p2 be Element of (n -tuples_on ( Class E)), q2 be Element of (n -tuples_on U) such that

         A6: [x, y2] = [p2, q2] & for j be set st j in ( Seg n) holds [(p2 . j), (q2 . j)] in r2 by A3;

        

         A7: x = p1 & y1 = q1 & x = p2 & y2 = q2 by XTUPLE_0: 1, A5, A6;

        reconsider q11 = q1 as Element of ( Funcs (( Seg n),U)) by FOMODEL0: 11;

        reconsider q22 = q2 as Element of ( Funcs (( Seg n),U)) by FOMODEL0: 11;

        now

          let j be set;

          assume

           A8: j in ( Seg n);

          then

          reconsider jj = j as Element of ( Seg n);

           [(p1 . j), (q1 . j)] in r2 & [(p2 . j), (q2 . j)] in r2 by A5, A6, A8;

          then [(q1 . j), (p1 . j)] in f1 & [(q2 . j), (p2 . j)] in f1 by RELAT_1:def 7;

          then (f1 . (q1 . jj)) = (p1 . jj) & (f1 . (q2 . jj)) = (p2 . jj) by FUNCT_1: 1;

          then ( Class (E,(q11 . jj))) = (p1 . jj) & ( Class (E,(q22 . jj))) = (p2 . jj) by Def13;

          hence [(q1 . j), (q2 . j)] in E by A7, EQREL_1: 35;

        end;

        then

         A9: [y1, y2] in (n -placesOf E) by A7;

        ((En -class ) . y11) = ( Class (En,y11)) & ((En -class ) . y22) = ( Class (En,y22)) by Def13;

        hence z1 = z2 by A9, EQREL_1: 35, A4;

      end;

      hence thesis by FUNCT_1:def 1;

    end;

    definition

      let U, n;

      let E be Equivalence_Relation of U;

      :: FOMODEL3:def14

      func n -tuple2Class E -> Relation of (n -tuples_on ( Class E)), ( Class (n -placesOf E)) equals ((n -placesOf ((E -class ) qua Relation of U, ( Class E) ~ )) * ((n -placesOf E) -class ));

      coherence ;

    end

    registration

      let U, n;

      let E be Equivalence_Relation of U;

      cluster (n -tuple2Class E) -> Function-like;

      coherence

      proof

        per cases ;

          suppose n is non zero;

          hence thesis by Lm11;

        end;

          suppose n is zero;

          then

          reconsider m = n as zero Nat;

          set En = (n -placesOf E);

          reconsider f1 = (E -class ) as Function of U, ( Class E);

          reconsider r1 = (E -class ) as Relation of U, ( Class E);

          reconsider r2 = (r1 ~ ) as Relation of ( Class E), U;

          reconsider f3 = (m -placesOf r2) as PartFunc of (m -tuples_on ( Class E)), (m -tuples_on U);

          reconsider f4 = (En -class ) as Function of (n -tuples_on U), ( Class (n -placesOf E));

          (f3 * f4) is Function-like;

          hence thesis;

        end;

      end;

    end

    registration

      let U, n;

      let E be Equivalence_Relation of U;

      cluster (n -tuple2Class E) -> total;

      coherence ;

    end

    definition

      let U, n;

      let E be Equivalence_Relation of U;

      :: original: -tuple2Class

      redefine

      func n -tuple2Class E -> Function of (n -tuples_on ( Class E)), ( Class (n -placesOf E)) ;

      coherence ;

    end

    definition

      let S, U;

      let s be ofAtomicFormula Element of S;

      let E be Equivalence_Relation of U;

      let f be Interpreter of s, U;

      :: FOMODEL3:def15

      func f quotient E -> set equals

      : Def15: (( |.( ar s).| -tuple2Class E) * (f quotient (( |.( ar s).| -placesOf E),E))) if not s is relational

      otherwise ((( |.( ar s).| -tuple2Class E) * (f quotient (( |.( ar s).| -placesOf E),( id BOOLEAN )))) * ( peeler BOOLEAN ));

      coherence ;

      consistency ;

    end

    definition

      let S, U;

      let s be ofAtomicFormula Element of S;

      let E be Equivalence_Relation of U;

      let f be E -respecting Interpreter of s, U;

      :: original: quotient

      redefine

      func f quotient E -> Interpreter of s, ( Class E) ;

      coherence

      proof

        set n = |.( ar s).|, D = (n -tuples_on U), h = (n -tuple2Class E), IT = (f quotient E);

        reconsider EE = (n -placesOf E) as Equivalence_Relation of D;

        reconsider hr = h as Relation;

        per cases ;

          suppose

           A1: not s is relational;

          then

          reconsider g = f as EE, E -respecting Function of D, 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;

          IT = (e * h) by Def15, A1;

          hence thesis by A1, FOMODEL2:def 2;

        end;

          suppose

           A2: s is relational;

          then

          reconsider g = f as EE, ( id BOOLEAN ) -respecting Function of D, 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;

          IT = (( peeler BOOLEAN ) * (e * h)) by A2, Def15;

          hence thesis by A2, FOMODEL2:def 2;

        end;

      end;

    end

    theorem :: FOMODEL3:1

    for X be non empty set, E be Equivalence_Relation of X, C1,C2 be Element of ( Class E) st C1 meets C2 holds C1 = C2 by EQREL_1:def 4;

    registration

      let S;

      cluster -> own for Element of ( OwnSymbolsOf S);

      coherence ;

      cluster -> ofAtomicFormula for Element of ( OwnSymbolsOf S);

      coherence ;

    end

    registration

      let S, U;

      let o be non relational ofAtomicFormula Element of S;

      let E be Relation of U;

      cluster E -respecting -> ( |.( ar o).| -placesOf E), E -respecting for Interpreter of o, U;

      coherence by Def10;

    end

    registration

      let S, U;

      let r be relational Element of S;

      let E be Relation of U;

      cluster E -respecting -> ( |.( ar r).| -placesOf E), ( id BOOLEAN ) -respecting for Interpreter of r, U;

      coherence by Def10;

    end

    registration

      let n;

      let U1,U2 be non empty set;

      let f be Function-like Relation of U1, U2;

      cluster (n -placesOf f) -> Function-like;

      coherence

      proof

        set IT = (n -placesOf f);

        per cases ;

          suppose n = 0 ;

          hence thesis;

        end;

          suppose n <> 0 ;

          then

          reconsider n as non zero Nat;

          now

            let x,y1,y2 be object;

            assume [x, y1] in IT;

            then

            consider p1 be Element of (n -tuples_on U1), q1 be Element of (n -tuples_on U2) such that

             A1: [x, y1] = [p1, q1] & for j be set st j in ( Seg n) holds [(p1 . j), (q1 . j)] in f;

            assume [x, y2] in IT;

            then

            consider p2 be Element of (n -tuples_on U1), q2 be Element of (n -tuples_on U2) such that

             A2: [x, y2] = [p2, q2] & for j be set st j in ( Seg n) holds [(p2 . j), (q2 . j)] in f;

            

             A3: x = p1 & y1 = q1 & x = p2 & y2 = q2 by A1, A2, XTUPLE_0: 1;

            reconsider xx = x as Function by A2, XTUPLE_0: 1;

            reconsider qq1 = q1, qq2 = q2 as Element of ( Funcs (( Seg n),U2)) by FOMODEL0: 11;

            now

              let j be Element of ( Seg n);

               [(xx . j), (q1 . j)] in f & [(xx . j), (q2 . j)] in f by A1, A2, A3;

              hence (qq1 . j) = (qq2 . j) by FUNCT_1:def 1;

            end;

            hence y1 = y2 by A3, FUNCT_2: 63;

          end;

          hence thesis by FUNCT_1:def 1;

        end;

      end;

    end

    registration

      let U1, U2;

      let n be zero Nat, R be Relation of U1, U2;

      cluster ((n -placesOf R) \+\ ( id { {} })) -> empty;

      coherence

      proof

        set A = { [ {} , {} ]};

        (A \+\ ( id { {} })) = {} & (n -placesOf R) = A by Lm4;

        hence thesis;

      end;

    end

    registration

      let X;

      let Y be functional set;

      cluster (X /\ Y) -> functional;

      coherence ;

    end

    theorem :: FOMODEL3:2

    for V be Element of (( AllTermsOf S) * ) holds ex mm be Element of NAT st V is Element of (((S -termsOfMaxDepth ) . mm) * ) by Lm3;

    definition

      let S, U;

      let E be Equivalence_Relation of U;

      let I be S, U -interpreter-like Function;

      :: FOMODEL3:def16

      attr I is E -respecting means

      : Def16: for s be own Element of S holds (I . s) qua Interpreter of s, U is E -respecting;

    end

    definition

      let S, U;

      let E be Equivalence_Relation of U;

      let I be S, U -interpreter-like Function;

      :: FOMODEL3:def17

      func I quotient E -> Function means

      : Def17: ( dom it ) = ( OwnSymbolsOf S) & for o be Element of ( OwnSymbolsOf S) holds (it . o) = ((I . o) quotient E);

      existence

      proof

        set O = ( OwnSymbolsOf S), AT = ( AllTermsOf S);

        deffunc F( Element of O) = ((I . $1) quotient E);

        consider f be Function such that

         A1: ( dom f) = O & for d be Element of O holds (f . d) = F(d) from FUNCT_1:sch 4;

        take f;

        thus ( dom f) = O & for o be Element of O holds (f . o) = ((I . o) quotient E) by A1;

      end;

      uniqueness

      proof

        set O = ( OwnSymbolsOf S), AT = ( AllTermsOf S);

        let IT1,IT2 be Function;

        deffunc F( Element of O) = ((I . $1) quotient E);

        assume

         A2: ( dom IT1) = O & for o be Element of O holds (IT1 . o) = F(o);

        assume

         A3: ( dom IT2) = O & for o be Element of O holds (IT2 . o) = F(o);

        ( dom IT1) = ( dom IT2) & for x be object st x in ( dom IT1) holds (IT1 . x) = (IT2 . x)

        proof

          thus ( dom IT1) = ( dom IT2) by A2, A3;

          let x be object;

          assume x in ( dom IT1);

          then

          reconsider o = x as Element of O by A2;

          (IT1 . o) = F(o) by A2

          .= (IT2 . o) by A3;

          hence thesis;

        end;

        hence thesis by FUNCT_1: 2;

      end;

    end

    definition

      let S, U;

      let E be Equivalence_Relation of U;

      let I be S, U -interpreter-like Function;

      :: original: quotient

      redefine

      :: FOMODEL3:def18

      func I quotient E means

      : Def18: ( dom it ) = ( OwnSymbolsOf S) & for o be own Element of S holds (it . o) = ((I . o) quotient E);

      compatibility

      proof

        set O = ( OwnSymbolsOf S), IT0 = (I quotient E);

        defpred P[ Function] means ( dom $1) = O & for o be own Element of S holds ($1 . o) = ((I . o) quotient E);

        let IT be Function;

        thus IT = IT0 implies P[IT]

        proof

          assume

           A1: IT = IT0;

          hence ( dom IT) = O by Def17;

          now

            let o be own Element of S;

            reconsider oo = o as Element of O by FOMODEL1:def 19;

            (IT0 . oo) = ((I . oo) quotient E) by Def17;

            hence (IT . o) = ((I . o) quotient E) by A1;

          end;

          hence thesis;

        end;

        assume

         A2: P[IT];

        for o be Element of O holds (IT . o) = ((I . o) quotient E) by A2;

        hence IT = IT0 by A2, Def17;

      end;

    end

    registration

      let S, U;

      let I be S, U -interpreter-like Function;

      let E be Equivalence_Relation of U;

      cluster (I quotient E) -> ( OwnSymbolsOf S) -defined;

      coherence

      proof

        set II = (I quotient E), O = ( OwnSymbolsOf S);

        ( dom II) c= O by Def17;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let S, U;

      let E be Equivalence_Relation of U;

      cluster E -respecting for Element of (U -InterpretersOf S);

      existence

      proof

        set O = ( OwnSymbolsOf S), C = ( PFuncs ((U * ),(U \/ BOOLEAN ))), II = (U -InterpretersOf S);

        deffunc F( Element of O) = the E -respecting Interpreter of $1, U;

        consider f be Function such that

         A1: ( dom f) = O & for d be Element of O holds (f . d) = F(d) from FUNCT_1:sch 4;

         A2:

        now

          let x be object;

          assume x in ( dom f);

          then

          reconsider o = x as Element of O by A1;

          (f . o) = F(o) by A1;

          hence (f . x) is Function;

        end;

        for s be own Element of S holds (f . s) is Interpreter of s, U

        proof

          let s be own Element of S;

          reconsider o = s as Element of O by FOMODEL1:def 19;

          (f . o) = F(o) by A1;

          hence thesis;

        end;

        then

        reconsider ff = f as Interpreter of S, U by FOMODEL2:def 3;

        reconsider fff = ff as S, U -interpreter-like Function by A2, FUNCOP_1:def 6, FOMODEL2:def 4;

        reconsider ffff = fff as O -defined Function by A1, RELAT_1:def 18;

        (fff | O) is C -valued & (ffff | O) = (ffff null O);

        then fff = fff & ( dom fff) = O & ( rng fff) c= C by RELAT_1:def 19, A1;

        then

        reconsider IT = fff as Element of ( Funcs (O,C)) by FUNCT_2:def 2;

        IT in II;

        then

        reconsider ITT = IT as Element of II;

        take ITT;

        now

          let s be own Element of S;

          reconsider o = s as Element of O by FOMODEL1:def 19;

          (fff . o) = F(o) by A1;

          hence (ITT . s) is E -respecting;

        end;

        hence thesis;

      end;

    end

    registration

      let S, U;

      let E be Equivalence_Relation of U;

      cluster E -respecting for S, U -interpreter-like Function;

      existence

      proof

        take IT = the E -respecting Element of (U -InterpretersOf S);

        thus thesis;

      end;

    end

    registration

      let S, U;

      let E be Equivalence_Relation of U;

      let o be own Element of S;

      let I be E -respectingS, U -interpreter-like Function;

      cluster (I . o) -> E -respecting;

      coherence by Def16;

    end

    registration

      let S, U;

      let E be Equivalence_Relation of U;

      let I be E -respectingS, U -interpreter-like Function;

      cluster (I quotient E) -> S, ( Class E) -interpreter-like;

      coherence

      proof

        set IT = (I quotient E), O = ( OwnSymbolsOf S);

        

         A1: for o be Element of O holds (IT . o) is Interpreter of o, ( Class E) & (IT . o) is Function

        proof

          let o be Element of O;

          reconsider i = (I . o) as E -respecting Interpreter of o, U;

          

           A2: (i quotient E) is Interpreter of o, ( Class E);

          hence (IT . o) is Interpreter of o, ( Class E) by Def17;

          thus (IT . o) is Function by A2, Def17;

        end;

        

         A3: for x be object st x in ( dom IT) holds (IT . x) is Function by A1;

        now

          let o be own Element of S;

          reconsider oo = o as Element of O by FOMODEL1:def 19;

          (IT . oo) is Interpreter of oo, ( Class E) by A1;

          hence (IT . o) is Interpreter of o, ( Class E);

        end;

        then IT is Interpreter of S, ( Class E) by FOMODEL2:def 3;

        hence thesis by A3, FUNCOP_1:def 6;

      end;

    end

    definition

      let S, U;

      let E be Equivalence_Relation of U;

      let I be E -respectingS, U -interpreter-like Function;

      :: original: quotient

      redefine

      func I quotient E -> Element of (( Class E) -InterpretersOf S) ;

      coherence

      proof

        set J = (I quotient E), O = ( OwnSymbolsOf S), II = (( Class E) -InterpretersOf S);

        (J null O) in II by FOMODEL2: 2;

        hence thesis;

      end;

    end

    

     Lm12: for R be Relation of U1, U2 holds (n -placesOf R) = { [p, q] where p be Element of (n -tuples_on U1), q be Element of (n -tuples_on U2) : q c= (p * R) }

    proof

      let R be Relation of U1, U2;

      deffunc F( set, set) = [$1, $2];

      defpred P[ Function, Function] means for j be set st j in ( Seg n) holds [($1 . j), ($2 . j)] in R;

      defpred Q[ Relation, set] means $2 c= ($1 * R);

      set N1 = (n -tuples_on U1), N2 = (n -tuples_on U2), D = ( Seg n), LH = { F(p,q) where p be Element of N1, q be Element of N2 : P[p, q] }, RH = { F(p,q) where p be Element of N1, q be Element of N2 : Q[p, q] };

      

       A1: for u be Element of N1, v be Element of N2 holds P[u, v] iff Q[u, v]

      proof

        let u be Element of N1, v be Element of N2;

        

         A2: ( len u) = n & ( len v) = n by CARD_1:def 7;

        then ( dom u) = D & ( dom v) = D by FINSEQ_1:def 3;

        then

         A3: u = { [x, (u . x)] where x be Element of D : x in D } & v = { [x, (v . x)] where x be Element of D : x in D } by FOMODEL0: 20;

        thus P[u, v] implies Q[u, v]

        proof

          assume

           A4: P[u, v];

          now

            let z be object;

            assume z in v;

            then

            consider x be Element of D such that

             A5: z = [x, (v . x)] & x in D by A3;

            

             A6: [(u . x), (v . x)] in R by A4, A5;

             [x, (u . x)] in u by A3, A5;

            hence z in (u * R) by A5, A6, RELAT_1:def 8;

          end;

          hence thesis by TARSKI:def 3;

        end;

        assume

         A7: Q[u, v];

        now

          let j be set;

          assume

           A8: j in D;

          then

          reconsider x = j as Element of D;

           [x, (v . x)] in v by A3, A8;

          then

          consider z be object such that

           A9: [x, z] in u & [z, (v . x)] in R by A7, RELAT_1:def 8;

          

           A10: z is set by TARSKI: 1;

          x in ( dom u) by A2, FINSEQ_1:def 3, A8;

          then z = (u . x) by A9, FUNCT_1:def 2, A10;

          hence [(u . j), (v . j)] in R by A9;

        end;

        hence thesis;

      end;

      LH = RH from FRAENKEL:sch 4( A1);

      hence thesis;

    end;

    

     Lm13: for U be non empty Subset of U2, P be Relation of U1, U, Q be Relation of U2, U3 holds ((n -placesOf P) * (n -placesOf Q)) c= (n -placesOf (P * Q))

    proof

      let U be non empty Subset of U2;

      let P be Relation of U1, U, Q be Relation of U2, U3;

      set R = (P * Q), LH = (n -placesOf R), Pn = (n -placesOf P), Qn = (n -placesOf Q), RH = (Pn * Qn), N = (n -tuples_on U), N1 = (n -tuples_on U1), N2 = (n -tuples_on U2), N3 = (n -tuples_on U3);

      

       A1: LH = { [p, q] where p be Element of N1, q be Element of N3 : q c= (p * R) } & Pn = { [p, q] where p be Element of N1, q be Element of N : q c= (p * P) } & Qn = { [p, q] where p be Element of N2, q be Element of N3 : q c= (p * Q) } by Lm12;

      now

        let t be object;

        assume

         A2: t in RH;

        then

        consider x,z be object such that

         A3: t = [x, z] by RELAT_1:def 1;

        consider y be object such that

         A4: [x, y] in Pn & [y, z] in Qn by A3, A2, RELAT_1:def 8;

        consider p1 be Element of N1, p2 be Element of N such that

         A5: [p1, p2] = [x, y] & p2 c= (p1 * P) by A1, A4;

        consider q1 be Element of N2, q2 be Element of N3 such that

         A6: [q1, q2] = [y, z] & q2 c= (q1 * Q) by A1, A4;

        

         A7: (p2 * Q) c= ((p1 * P) * Q) & p1 = x & p2 = y & q1 = y & q2 = z by XTUPLE_0: 1, RELAT_1: 30, A5, A6;

        then q2 c= ((p1 * P) * Q) by XBOOLE_1: 1, A6;

        then [p1, q2] = [p1, q2] & q2 c= (p1 * R) by RELAT_1: 36;

        hence t in LH by A3, A7, A1;

      end;

      hence thesis by TARSKI:def 3;

    end;

    

     Lm14: for U be non empty Subset of U2, P be Relation of U1, U, Q be Relation of U2, U3 holds (n -placesOf (P * Q)) c= ((n -placesOf P) * (n -placesOf Q))

    proof

      let U be non empty Subset of U2;

      let P be Relation of U1, U, Q be Relation of U2, U3;

      set R = (P * Q), LH = (n -placesOf R), Pn = (n -placesOf P), Qn = (n -placesOf Q), RH = (Pn * Qn), N = (n -tuples_on U), N1 = (n -tuples_on U1), N2 = (n -tuples_on U2), N3 = (n -tuples_on U3);

      reconsider nn = n as Element of NAT by ORDINAL1:def 12;

      now

        let x be object;

        assume x in LH;

        then

        consider p be Element of N1, q be Element of N3 such that

         A1: x = [p, q] & for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R;

        defpred Z[ set, set] means [(p . $1), $2] in P & [$2, (q . $1)] in Q;

        

         A2: for k be Nat st k in ( Seg n) holds ex y be Element of U st Z[k, y]

        proof

          let k be Nat;

          assume k in ( Seg n);

          then [(p . k), (q . k)] in R by A1;

          then

          consider y be object such that

           A3: [(p . k), y] in P & [y, (q . k)] in Q by RELAT_1:def 8;

          y in ( rng P) & ( rng P) c= U by A3, XTUPLE_0:def 13;

          then

          reconsider yy = y as Element of U;

          take yy;

          thus thesis by A3;

        end;

        consider r be FinSequence of U such that

         A4: ( dom r) = ( Seg n) & for k be Nat st k in ( Seg n) holds Z[k, (r . k)] from FINSEQ_1:sch 5( A2);

        ( len r) = nn by FINSEQ_1:def 3, A4;

        then

        reconsider rr = r as n -element FinSequence of U by CARD_1:def 7;

        reconsider rrr = rr as Element of N by FOMODEL0: 16;

        reconsider rrrr = rrr as Element of N2 by FOMODEL0: 16;

         [p, rrr] = [p, rrr] & for j be set st j in ( Seg n) holds [(p . j), (rrr . j)] in P by A4;

        then

         A5: [p, rrr] in Pn;

         [rrrr, q] = [rrrr, q] & for j be set st j in ( Seg n) holds [(rrrr . j), (q . j)] in Q by A4;

        then [rrrr, q] in Qn;

        hence x in RH by A1, A5, RELAT_1:def 8;

      end;

      hence thesis by TARSKI:def 3;

    end;

    

     Lm15: for U be non empty Subset of U2, P be Relation of U1, U, Q be Relation of U2, U3 holds (n -placesOf (P * Q)) = ((n -placesOf P) * (n -placesOf Q)) by Lm13, Lm14;

    

     Lm16: for P be Relation of U1, U2, Q be Relation of U2, U3 holds (n -placesOf (P * Q)) = ((n -placesOf P) * (n -placesOf Q))

    proof

      reconsider U = (U2 /\ U2) as non empty Subset of U2;

      let P be Relation of U1, U2, Q be Relation of U2, U3;

      reconsider PP = P as Relation of U1, U;

      (n -placesOf (PP * Q)) = ((n -placesOf PP) * (n -placesOf Q)) by Lm15;

      hence thesis;

    end;

    

     Lm17: for R be Relation of U1, U2 holds (n -placesOf (R ~ )) = ((n -placesOf R) ~ )

    proof

      let R be Relation of U1, U2;

      set N1 = (n -tuples_on U1), N2 = (n -tuples_on U2), IT = { [q, p] where p be Element of N1, q be Element of N2 : for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R };

      reconsider Q = (R ~ ) as Relation of U2, U1;

      reconsider Rn = (n -placesOf R) as Relation of (n -tuples_on U1), (n -tuples_on U2);

      reconsider LH = (n -placesOf Q) as Relation of (n -tuples_on U2), (n -tuples_on U1);

      reconsider RH = (Rn ~ ) as Relation of (n -tuples_on U2), (n -tuples_on U1);

      now

        let x be object;

        assume x in LH;

        then

        consider p be Element of N2, q be Element of N1 such that

         A1: x = [p, q] & for j be set st j in ( Seg n) holds [(p . j), (q . j)] in (R ~ );

        for j be set st j in ( Seg n) holds [(q . j), (p . j)] in R

        proof

          let j be set;

          assume j in ( Seg n);

          then [(p . j), (q . j)] in (R ~ ) by A1;

          hence thesis by RELAT_1:def 7;

        end;

        then [q, p] in Rn;

        hence x in RH by RELAT_1:def 7, A1;

      end;

      then

       A2: LH c= RH by TARSKI:def 3;

      now

        let x be object;

        assume x in (RH ~ );

        then

        consider p be Element of N1, q be Element of N2 such that

         A3: x = [p, q] & for j be set st j in ( Seg n) holds [(p . j), (q . j)] in R;

        for j be set st j in ( Seg n) holds [(q . j), (p . j)] in (R ~ )

        proof

          let j be set;

          assume j in ( Seg n);

          then [(p . j), (q . j)] in R by A3;

          hence thesis by RELAT_1:def 7;

        end;

        then [q, p] in LH;

        hence x in (LH ~ ) by A3, RELAT_1:def 7;

      end;

      then (RH ~ ) c= (LH ~ ) by TARSKI:def 3;

      then ((RH ~ ) \ (LH ~ )) = {} ;

      then ((RH \ LH) ~ ) = {} by RELAT_1: 24;

      then (((RH \ LH) ~ ) ~ ) = {} ;

      then RH c= LH by XBOOLE_1: 37;

      hence thesis by A2;

    end;

    

     Lm18: for X,Y be non empty set, E be Equivalence_Relation of X, F be Equivalence_Relation of Y, g be E, F -respecting Function of X, Y holds ((F -class ) * g) = ((g quotient (E,F)) * (E -class ))

    proof

      let X,Y be non empty set;

      let E be Equivalence_Relation of X;

      let F be Equivalence_Relation of Y;

      let g be E, F -respecting Function of X, Y;

      set G = (g quotient (E,F));

      

       A1: ( dom G) = ( Class E) by FUNCT_2:def 1;

      reconsider LH = ((F -class ) * g), RH = (G * (E -class )) as Function of X, ( Class F);

      

       A2: ( dom LH) = X & ( dom RH) = X by FUNCT_2:def 1;

      now

        let x be Element of X;

        reconsider F1 = (LH . x), F2 = (RH . x) as Element of ( Class F);

        

         A3: F1 = ((F -class ) . (g . x)) & F2 = (G . ((E -class ) . x)) by A2, FUNCT_1: 12;

        then F2 = (G . ( EqClass (E,x))) by Def13;

        then [( EqClass (E,x)), F2] in G by A1, FUNCT_1: 1;

        then

        consider e be Element of ( Class E), f be Element of ( Class F) such that

         A4: [( EqClass (E,x)), F2] = [e, f] & ex a,b be set st a in e & b in f & [a, b] in g;

        consider a,b be set such that

         A5: a in e & b in f & [a, b] in g by A4;

        

         A6: ( EqClass (E,x)) = e & F2 = f by A4, XTUPLE_0: 1;

        then

         A7: a in ( EqClass (E,x)) & [a, x] in E & b in F2 by A5, EQREL_1: 19;

        a in X by A5;

        then a in ( dom g) by FUNCT_2:def 1;

        then b = (g . a) by A5, FUNCT_1:def 2;

        then [b, (g . x)] in F by A7, Def9;

        then b in ( EqClass (F,(g . x))) by EQREL_1: 19;

        then b in F1 by A3, Def13;

        hence (LH . x) = (RH . x) by EQREL_1:def 4, A5, A6, XBOOLE_0: 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm19: for p be m -elementU1 -valued FinSequence, f be Function of U1, U2 holds (f * p) = ((m -placesOf f) . p)

    proof

      let p be m -elementU1 -valued FinSequence;

      let f be Function of U1, U2;

      set F = (m -placesOf f);

      

       A1: ( dom f) = U1 & ( dom F) = (m -tuples_on U1) & p in (m -tuples_on U1) & (f * p) in (m -tuples_on U2) by FUNCT_2:def 1, FOMODEL0: 16;

      reconsider pp = p as Element of (m -tuples_on U1) by FOMODEL0: 16;

      pp is Element of ( Funcs (( Seg m),U1)) by FOMODEL0: 11;

      then

      reconsider ppp = pp as Function of ( Seg m), U1;

      reconsider LH = (f * p) as Element of ( Funcs (( Seg m),U2)) by FOMODEL0: 11, A1;

      reconsider RH = (F . pp) as Element of ( Funcs (( Seg m),U2)) by FOMODEL0: 11;

      reconsider LHH = LH, RHH = RH as Function of ( Seg m), U2;

      reconsider LHHH = LH, RHHH = RH as Element of (m -tuples_on U2) by FOMODEL0: 11;

      

       A2: ( dom ppp) = ( Seg m) & ( rng ppp) c= U1 & ( dom LH) = ( Seg m) & ( dom LH) = ( Seg m) by FUNCT_2:def 1, RELAT_1:def 19;

       [p, LH] in F

      proof

        for j be set st j in ( Seg m) holds [(pp . j), (LHHH . j)] in f

        proof

          let j be set;

          assume

           A3: j in ( Seg m);

          then

           A4: (LH . j) = (f . (p . j)) by A2, FUNCT_1: 12;

          (ppp . j) in ( rng ppp) by FUNCT_1: 3, A3, A2;

          hence thesis by A1, A2, A4, FUNCT_1: 1;

        end;

        hence thesis;

      end;

      hence thesis by FUNCT_1: 1;

    end;

    

     Lm20: for E be Equivalence_Relation of U holds ((n -placesOf E) -class ) = ((n -tuple2Class E) * (n -placesOf (E -class )))

    proof

      let E be Equivalence_Relation of U;

      set UN = (n -tuples_on U), A = (n -tuple2Class E), RH = (A * (n -placesOf (E -class ))), LH = ((n -placesOf E) -class );

      reconsider RA = (n -placesOf (E -class )) as Relation of (n -tuples_on U), (n -tuples_on ( Class E));

      reconsider ER = (E -class ) as Relation of U, ( Class E);

      reconsider RB = (n -placesOf (ER ~ )) as Relation of (n -tuples_on ( Class E)), (n -tuples_on U);

      reconsider RC = ((n -placesOf ER) ~ ) as Relation of (n -tuples_on ( Class E)), (n -tuples_on U);

      

       A1: ( dom LH) = UN & ( dom RH) = UN by FUNCT_2:def 1;

      reconsider FA = RA as Function of UN, (n -tuples_on ( Class E));

      reconsider RAA = RA as totalUN -defined Relation;

      RH = ((RA * RB) * ((n -placesOf E) -class )) by RELAT_1: 36

      .= ((RA * RC) * LH) by Lm17;

      then (( id UN) qua Relation * LH) c= RH by FOMODEL0: 21, RELAT_1: 30;

      then (LH | UN) c= RH by RELAT_1: 65;

      hence thesis by GRFUNC_1: 3, A1;

    end;

    

     Lm21: for E be Equivalence_Relation of U1, F be Equivalence_Relation of U2, g be (n -placesOf E), F -respecting Function of (n -tuples_on U1), U2 holds ((g quotient ((n -placesOf E),F)) * (n -tuple2Class E)) = ((n -placesOf ((E -class ) qua Relation of U1, ( Class E) ~ )) * ((F -class ) * g))

    proof

      set X = U1, Y = U2;

      let E be Equivalence_Relation of X, F be Equivalence_Relation of Y;

      let g be (n -placesOf E), F -respecting Function of (n -tuples_on X), Y;

      reconsider G = (g quotient ((n -placesOf E),F)) as Function of ( Class (n -placesOf E)), ( Class F);

      reconsider R = G as Relation of ( Class (n -placesOf E)), ( Class F);

      reconsider projector = (E -class ) as Relation of X, ( Class E);

      (G * (n -tuple2Class E)) = ((n -placesOf (projector ~ )) * (((n -placesOf E) -class ) * R)) by RELAT_1: 36

      .= ((n -placesOf (projector ~ )) * ((F -class ) * g)) by Lm18;

      hence thesis;

    end;

    

     Lm22: for R be total reflexive Relation of U st x in ( dom f) & f is U -valued holds f is ( id {x}), R -respecting

    proof

      let R be total reflexive Relation of U;

      set E = ( id {x});

      assume

       A1: x in ( dom f);

      then

      reconsider D = ( dom f) as non empty set;

      (E \+\ { [x, x]}) = {} ;

      then

       A2: E = { [x, x]} by FOMODEL0: 29;

      reconsider xx = x as Element of D by A1;

      assume f is U -valued;

      then ( rng f) c= U by RELAT_1:def 19;

      then

      reconsider ff = f as Function of D, U by FUNCT_2: 2;

      now

        let x1,x2 be set;

        assume [x1, x2] in E;

        then [x1, x2] = [x, x] by A2, TARSKI:def 1;

        then

         A3: x1 = x & x2 = x by XTUPLE_0: 1;

        (f . xx) = (f . xx) & (ff . xx) in U;

        hence [(f . x1), (f . x2)] in R by EQREL_1: 5, A3;

      end;

      hence thesis;

    end;

    

     Lm23: (( peeler U) * (( id U) -class )) = ( id U)

    proof

      set X = U, P = ( peeler X), IX = ( id X), I = (IX -class ), IT = (P * I);

      reconsider Pf = P, If = I as Function;

      

       A1: ( dom I) = X & ( dom IX) = X by FUNCT_2:def 1;

      

       A2: {_{X}_} = the set of all {x} where x be Element of X by EQREL_1: 37;

      reconsider PP = P as Function of ( Class IX), X;

      reconsider II = I as Function of X, ( Class IX);

      reconsider LH = (PP * II), RH = IX as Function of X, X;

      now

        let x be Element of X;

        set xx = x;

         {x} in {_{X}_} by A2;

        then

        reconsider xton = {x} as Element of {_{X}_};

        ((Pf * If) . x) = (Pf . (If . xx)) by A1, FUNCT_1: 13

        .= (P . ( Class (( id X),xx))) by Def13

        .= (P . xton) by EQREL_1: 25

        .= ( DeTrivial xton) by Def12

        .= xx by Def11

        .= (IX . x);

        hence (IX . x) = ((PP * II) . x);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm24: for E be Equivalence_Relation of U, I be E -respectingS, U -interpreter-like Function holds ((((I quotient E),((E -class ) . u)) -TermEval ) . k) = ((E -class ) * (((I,u) -TermEval ) . k))

    proof

      let E be Equivalence_Relation of U;

      reconsider e = ((E -class ) . u) as Element of ( Class E);

      let I be E -respectingS, U -interpreter-like Function;

      set te = ((I,u) -TermEval ), II = (I quotient E), TE = ((II,e) -TermEval ), F = (S -firstChar ), O = ( OwnSymbolsOf S), TT = ( AllTermsOf S);

      defpred P[ Nat] means (TE . $1) = ((E -class ) * (te . $1));

      

       A1: P[ 0 ]

      proof

        

         A2: (TE . 0 ) = (TT --> e) & (te . 0 ) = (TT --> u) by FOMODEL2:def 8;

        ( dom (E -class )) = U by FUNCT_2:def 1;

        hence thesis by A2, FUNCOP_1: 17;

      end;

      

       A3: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        assume

         A4: P[m];

        reconsider mm = m, MM = (m + 1) as Element of NAT by ORDINAL1:def 12;

        (te . mm) is Element of ( Funcs (TT,U)) & (te . MM) is Element of ( Funcs (TT,U));

        then

        reconsider tm = (te . mm), tmm = (te . MM) as Function of TT, U;

        (TE . mm) is Element of ( Funcs (TT,( Class E))) & (TE . MM) is Element of ( Funcs (TT,( Class E)));

        then

        reconsider TM = (TE . mm), TMM = (TE . MM) as Function of TT, ( Class E);

        now

          let tt;

          reconsider t = tt as termal string of S;

          set s = (F . t), g = (I . s), G = (II . s), sub = ( SubTerms t), n = |.( ar s).|;

          reconsider gg = g as (n -placesOf E), E -respecting Function of (n -tuples_on U), U by FOMODEL2:def 2;

          

           A5: (g quotient E) = ((gg quotient ((n -placesOf E),E)) * (n -tuple2Class E)) by Def15;

          reconsider ggg = (gg quotient ((n -placesOf E),E)) as Function;

          

           A6: (tm * sub) is n -elementU -valued FinSequence & ( dom (n -placesOf (E -class ))) = (n -tuples_on U) & ( dom gg) = (n -tuples_on U) & ( dom tmm) = TT by FUNCT_2:def 1;

          

          thus (TMM . tt) = (G . ((TE . m) * sub)) by FOMODEL2: 3

          .= ((g quotient E) . ((TE . m) * sub)) by Def18

          .= ((g quotient E) . ((E -class ) * (tm * sub))) by RELAT_1: 36, A4

          .= ((g quotient E) . ((n -placesOf (E -class )) . (tm * sub))) by Lm19

          .= (((ggg * (n -tuple2Class E)) * (n -placesOf (E -class ))) . (tm * sub)) by A5, A6, FOMODEL0: 16, FUNCT_1: 13

          .= ((ggg * ((n -tuple2Class E) * (n -placesOf (E -class )))) . (tm * sub)) by RELAT_1: 36

          .= ((ggg * ((n -placesOf E) -class )) . (tm * sub)) by Lm20

          .= (((E -class ) * gg) . (tm * sub)) by Lm18

          .= ((E -class ) . (gg . (tm * sub))) by A6, FOMODEL0: 16, FUNCT_1: 13

          .= ((E -class ) . ((te . (m + 1)) . t)) by FOMODEL2: 3

          .= (((E -class ) * tmm) . tt) by A6, FUNCT_1: 13;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      for n holds P[n] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    

     Lm25: for E be Equivalence_Relation of U, I be E -respectingS, U -interpreter-like Function holds ((I quotient E) -TermEval ) = ((E -class ) * (I -TermEval ))

    proof

      let E be Equivalence_Relation of U;

      set u = the Element of U;

      let I be E -respectingS, U -interpreter-like Function;

      reconsider e = ((E -class ) . u) as Element of ( Class E);

      set F = (S -firstChar ), II = (I quotient E), te = ((I,u) -TermEval ), TE = ((II,e) -TermEval ), O = ( OwnSymbolsOf S), TT = ( AllTermsOf S), tee = (I -TermEval ), TEE = (II -TermEval ), T = (S -termsOfMaxDepth );

      reconsider TF = T as Function;

      now

        let tt be Element of TT;

        consider mm such that

         A1: tt in (TF . mm) by FOMODEL1: 5;

        set v = (I -TermEval tt), V = (II -TermEval tt);

        reconsider MM = (mm + 1) as Element of NAT ;

        (te . MM) is Element of ( Funcs (TT,U));

        then

         A2: ( dom (te . MM)) = TT & ( dom tee) = TT by FUNCT_2:def 1;

        

        thus (TEE . tt) = V by FOMODEL2:def 10

        .= ((TE . (mm + 1)) . tt) by FOMODEL2:def 9, A1

        .= (((E -class ) * (te . (mm + 1))) . tt) by Lm24

        .= ((E -class ) . ((te . (mm + 1)) . tt)) by FUNCT_1: 13, A2

        .= ((E -class ) . v) by FOMODEL2:def 9, A1

        .= ((E -class ) . (tee . tt)) by FOMODEL2:def 10

        .= (((E -class ) * tee) . tt) by A2, FUNCT_1: 13;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm26: for R be Equivalence_Relation of U1, phi be 0wff string of S, i be R -respectingS, U1 -interpreter-like Function st ((S -firstChar ) . phi) <> ( TheEqSymbOf S) holds ((i quotient R) -AtomicEval phi) = (i -AtomicEval phi)

    proof

      let R be Equivalence_Relation of U1, phi be 0wff string of S, i be R -respectingS, U1 -interpreter-like Function;

      set TT = ( AllTermsOf S), E = ( TheEqSymbOf S), p = ( SubTerms phi), F = (S -firstChar ), r = (F . phi), n = |.( ar r).|, U = ( Class R), I = (i quotient R), UV = (I -TermEval ), N1 = (n -tuples_on U1), V = (I -AtomicEval phi), uv = (i -TermEval ), v = (i -AtomicEval phi), f = ((I === ) . r), G = (I . r), g = (i . r), d = (U -deltaInterpreter );

      

       A1: p in (n -tuples_on TT) & ( dom (n -placesOf ((R -class ) * uv))) = (n -tuples_on TT) & ( dom (n -placesOf uv)) = (n -tuples_on TT) by FUNCT_2:def 1, FOMODEL0: 16;

      assume

       A2: r <> E;

      

      then

       A3: V = (G . (UV * p)) by FOMODEL2: 14

      .= (G . (((R -class ) * uv) * p)) by Lm25

      .= (G . ((n -placesOf ((R -class ) * uv)) . p)) by Lm19

      .= ((G * (n -placesOf ((R -class ) * uv))) . p) by FUNCT_1: 13, A1;

      reconsider o = r as Element of ( OwnSymbolsOf S) by A2, FOMODEL1: 15;

      set gg = (i . o), GG = (I . o);

      reconsider ggg = gg as (n -placesOf R), ( id BOOLEAN ) -respecting Function of (n -tuples_on U1), BOOLEAN by FOMODEL2:def 2, Def10;

      set F = (ggg quotient ((n -placesOf R),( id BOOLEAN )));

      reconsider P = ( peeler BOOLEAN ) as Function;

      reconsider nuisance1 = F, nuisance2 = (n -tuple2Class R), nuisance3 = P as Relation;

      reconsider RR = (R -class ) as Relation of U1, ( Class R);

      

       A4: GG = (gg quotient R) by Def18

      .= (( peeler BOOLEAN ) * (F * (n -tuple2Class R))) by Def15;

      

       A5: ((n -tuple2Class R) * (n -placesOf ((R -class ) * uv))) = (((n -placesOf R) -class ) * (n -placesOf uv))

      proof

        set x = (n -placesOf ((R -class ) * uv));

        

         A6: ((n -tuple2Class R) * (n -placesOf ((R -class ) * uv))) = (((n -placesOf uv) * (n -placesOf RR)) * ((n -placesOf (RR ~ )) * ((n -placesOf R) -class ))) by Lm16

        .= ((n -placesOf uv) * ((n -placesOf RR) * ((n -placesOf (RR ~ )) * ((n -placesOf R) -class )))) by RELAT_1: 36

        .= ((n -placesOf uv) * (((n -placesOf RR) * (n -placesOf (RR ~ ))) * ((n -placesOf R) -class ))) by RELAT_1: 36

        .= ((n -placesOf uv) * (((n -placesOf RR) * ((n -placesOf RR) ~ )) * ((n -placesOf R) -class ))) by Lm17;

        ((n -placesOf uv) * (((n -placesOf RR) * ((n -placesOf RR) ~ )) * ((n -placesOf R) -class ))) = (((n -placesOf uv) * ((n -placesOf RR) * ((n -placesOf RR) ~ ))) * ((n -placesOf R) -class )) by RELAT_1: 36

        .= ((((n -placesOf uv) * (n -placesOf RR)) * ((n -placesOf RR) ~ )) * ((n -placesOf R) -class )) by RELAT_1: 36;

        hence thesis by A6, FOMODEL0: 27;

      end;

      ((P * (F * (n -tuple2Class R))) * (n -placesOf ((R -class ) * uv))) = (P * ((F * (n -tuple2Class R)) * (n -placesOf ((R -class ) * uv)))) by RELAT_1: 36

      .= (P * (F * (((n -placesOf R) -class ) * (n -placesOf uv)))) by A5, RELAT_1: 36;

      

      then V = ((P * ((F * ((n -placesOf R) -class )) * (n -placesOf uv))) . p) by A3, A4, RELAT_1: 36

      .= (((P * (F * ((n -placesOf R) -class ))) * (n -placesOf uv)) . p) by RELAT_1: 36

      .= ((P * (F * ((n -placesOf R) -class ))) . ((n -placesOf uv) . p)) by FUNCT_1: 13, A1

      .= ((P * (F * ((n -placesOf R) -class ))) . (uv * p)) by Lm19

      .= ((P * ((( id BOOLEAN ) -class ) * ggg)) . (uv * p)) by Lm18

      .= (((P * (( id BOOLEAN ) -class )) * ggg) . (uv * p)) by RELAT_1: 36

      .= ((( id BOOLEAN ) * ggg) . (uv * p)) by Lm23

      .= (ggg . (uv * p)) by FUNCT_2: 17

      .= (i -AtomicEval phi) by FOMODEL2: 14;

      hence thesis;

    end;

    

     Lm27: for t be 0 -termal string of S holds ((((((S,X) -freeInterpreter ),tt) -TermEval ) . (m + 1)) . t) = t

    proof

      let t be 0 -termal string of S;

      set I = ((S,X) -freeInterpreter ), TT = ( AllTermsOf S), F = (S -firstChar ), v = (F . t), n = |.( ar v).|, C = (S -multiCat ), II = ((I,tt) -TermEval ), SS = ( AllSymbolsOf S), ff = ((v -compound ) | (n -tuples_on TT));

      reconsider f = (X -freeInterpreter v) as Function of (n -tuples_on TT), TT by FOMODEL2:def 2;

      

       A1: ff = f by Def3;

      reconsider E = {} as Element of (((SS * ) \ { {} }) * ) by FINSEQ_1: 49;

      ( dom f) = ( 0 -tuples_on TT) by FUNCT_2:def 1;

      then ( dom f) = { {} } by FOMODEL0: 10;

      then

       A2: {} in ( dom ff) by A1, TARSKI:def 1;

      

      thus ((II . (m + 1)) . t) = ((I . v) . {} ) by FOMODEL2: 3

      .= (f . {} ) by Def4

      .= (ff . {} ) by Def3

      .= ((v -compound ) . {} ) by A2, FUNCT_1: 47

      .= (v -compound E) by Def2

      .= ( <*v*> null {} )

      .= t by FOMODEL2: 1;

    end;

    

     Lm28: ((((((S,X) -freeInterpreter ),tt) -TermEval ) . (m + 1)) | ((S -termsOfMaxDepth ) . m)) = ( id ((S -termsOfMaxDepth ) . m))

    proof

      set I = ((S,X) -freeInterpreter ), TE = ((I,tt) -TermEval ), T = (S -termsOfMaxDepth ), F = (S -firstChar ), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S);

      defpred P[ Nat] means ((TE . ($1 + 1)) | (T . $1)) = ( id (T . $1));

      

       A1: P[ 0 ]

      proof

        reconsider Z = 0 , O = 1 as Element of NAT ;

        (TE . O) is Element of ( Funcs (TT,TT));

        then (TE . O) is Function of TT, TT & (T . Z) c= TT by FOMODEL1: 2;

        then

        reconsider f = ((TE . 1) | (T . 0 )) as Function of (T . 0 ), TT by FUNCT_2: 32;

        

         A2: ( dom f) = (T . 0 ) by FUNCT_2:def 1;

        now

          let x be object;

          assume x in (T . 0 );

          then

          reconsider xx = x as Element of (T . Z);

          reconsider t = xx as 0 -termal string of S by FOMODEL1:def 33;

          

          thus (f . x) = ((TE . ( 0 + 1)) . t) by A2, FUNCT_1: 47

          .= x by Lm27;

        end;

        hence thesis by FUNCT_1: 17, A2;

      end;

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        reconsider nn = n, NN = (n + 1), NNN = ((n + 1) + 1) as Element of NAT by ORDINAL1:def 12;

        (TE . NNN) is Element of ( Funcs (TT,TT));

        then (TE . NNN) is Function of TT, TT & (T . NN) c= TT by FOMODEL1: 2;

        then

        reconsider f = ((TE . NNN) | (T . NN)) as Function of (T . NN), TT by FUNCT_2: 32;

        

         A5: ( dom f) = ( dom ( id (T . NN))) by FUNCT_2:def 1;

        now

          let x be object;

          assume

           A6: x in ( dom f);

          then

          reconsider tt = x as Element of (T . (nn + 1));

          reconsider t = tt as (nn + 1) -termal string of S by FOMODEL1:def 33;

          set s = (F . t), p = |.( ar s).|;

          

           A7: ( dom (X -freeInterpreter s)) = (p -tuples_on TT) by FUNCT_2:def 1;

          reconsider subt = ( SubTerms t) as (T . n) -valued Function;

          reconsider subtt = subt as Element of ( dom (X -freeInterpreter s)) by FOMODEL0: 16, A7;

          

           A8: subtt in ( dom (X -freeInterpreter s)) & (X -freeInterpreter s) = ((s -compound ) | (p -tuples_on TT)) by Def3;

          ( SubTerms t) in (TT * );

          then

          reconsider subttt = ( SubTerms t) as Element of (((SS * ) \ { {} }) * );

          reconsider temp = (subt null (T . n)) as Function;

          

          thus (f . x) = ((TE . NNN) . x) by A6, FUNCT_1: 47

          .= ((I . s) . ((TE . (n + 1)) * ((T . n) |` subt))) by FOMODEL2: 3

          .= ((I . s) . ((TE . (n + 1)) * (( id (T . n)) * subt))) by RELAT_1: 92

          .= ((I . s) . (((TE . (n + 1)) * ( id (T . n))) * subt)) by RELAT_1: 36

          .= ((I . s) . (((TE . (n + 1)) | (T . n)) * subt)) by RELAT_1: 65

          .= ((I . s) . ((T . n) |` subt)) by RELAT_1: 92, A4

          .= ((X -freeInterpreter s) . subt) by Def4

          .= ((s -compound ) . subttt) by A8, FUNCT_1: 47

          .= (s -compound subttt) by Def2

          .= (( id (T . (n + 1))) . x) by FOMODEL1:def 37;

        end;

        hence thesis by A5, FUNCT_1: 2;

      end;

       P[n] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    

     Lm29: (((S,X) -freeInterpreter ) -TermEval ) = ( id ( AllTermsOf S))

    proof

      set u = the Element of ( AllTermsOf S), I = ((S,X) -freeInterpreter ), TE = ((I,u) -TermEval ), T = (S -termsOfMaxDepth ), F = (S -firstChar ), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S);

      reconsider Tf = T as Function;

      reconsider LH = (I -TermEval ), RH = ( id TT) as Function of TT, TT;

      now

        let tt be Element of TT;

        consider mm such that

         A1: tt in (Tf . mm) by FOMODEL1: 5;

        reconsider ttt = tt as Element of (T . mm) by A1;

        reconsider M = (mm + 1) as Element of NAT ;

        reconsider tttt = tt as Element of (T . mm) by A1;

        set uv = (I -TermEval tt);

        (TE . M) is Element of ( Funcs (TT,TT));

        then

        reconsider f = (TE . (mm + 1)) as Function of TT, TT;

        (((f | (T . mm)) . ttt) \+\ (f . ttt)) = {} ;

        then

         A2: ((f | (T . mm)) . ttt) = (f . ttt) by FOMODEL0: 29;

        

         A3: (( id (T . mm)) . tttt) = tttt & (( id TT) . tt) = tt;

        

        thus (LH . tt) = uv by FOMODEL2:def 10

        .= (f . tt) by FOMODEL2:def 9, A1

        .= (RH . tt) by A3, A2, Lm28;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm30: for R be Relation of U1, U2 holds ( 0 -placesOf R) = ( id { {} })

    proof

      let R be Relation of U1, U2;

      (( 0 -placesOf R) \+\ ( id { {} })) = {} ;

      hence thesis by FOMODEL0: 29;

    end;

    theorem :: FOMODEL3:3

    for E be Equivalence_Relation of U, I be E -respectingS, U -interpreter-like Function holds ((I quotient E) -TermEval ) = ((E -class ) * (I -TermEval )) by Lm25;

    theorem :: FOMODEL3:4

    (((S,X) -freeInterpreter ) -TermEval ) = ( id ( AllTermsOf S)) by Lm29;

    theorem :: FOMODEL3:5

    for R be Equivalence_Relation of U1, phi be 0wff string of S, i be R -respectingS, U1 -interpreter-like Function st ((S -firstChar ) . phi) <> ( TheEqSymbOf S) holds ((i quotient R) -AtomicEval phi) = (i -AtomicEval phi) by Lm26;

    

     Lm31: ((l1 SubstWith l2) | ((S -termsOfMaxDepth ) . m)) is Function of ((S -termsOfMaxDepth ) . m), ((S -termsOfMaxDepth ) . m)

    proof

      set T = (S -termsOfMaxDepth ), F = (S -firstChar ), C = (S -multiCat ), SS = ( AllSymbolsOf S);

      set strings = ((SS * ) \ { {} }), g = (SS -concatenation ), G = ( MultPlace g), e = (l1 SubstWith l2);

      

       A1: for t be 0 -termal string of S holds (e . t) in (T . 0 )

      proof

        let t be 0 -termal string of S;

        set l = (F . t);

        

         A2: t = <*l*> by FOMODEL2: 1;

        l = l1 or l <> l1;

        then (e . <*l*>) = <*l2*> or (e . <*l*>) = <*l*> by FOMODEL0: 35;

        hence thesis by A2, FOMODEL1:def 33;

      end;

      defpred P[ Nat] means (e | (T . $1)) is Function of (T . $1), (T . $1);

      

       A3: P[ 0 ]

      proof

        reconsider z = 0 as Element of NAT ;

        reconsider T0 = (T . z) as Subset of (SS * ) by XBOOLE_1: 1;

        set f = (e | T0);

        

         A4: ( dom f) = T0 by PARTFUN1:def 2;

        now

          let x be object;

          assume

           A5: x in T0;

          reconsider t = x as 0 -termal string of S by A5, FOMODEL1:def 33;

          set l = (F . t);

          reconsider tt = t as Element of T0 by FOMODEL1:def 33;

          ((f . tt) \+\ (e . tt)) = {} ;

          then (f . x) = (e . x) by FOMODEL0: 29;

          then (f . t) in T0 by A1;

          hence (f . x) in T0;

        end;

        hence thesis by A4, FUNCT_2: 3;

      end;

      

       A6: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        reconsider mm = m, MM = (m + 1) as Element of NAT by ORDINAL1:def 12;

        assume

         A7: P[m];

        reconsider Tm = (T . mm), TM = (T . MM) as Subset of (SS * ) by XBOOLE_1: 1;

        reconsider f = (e | (T . m)) as Function of (T . mm), (T . mm) by A7;

        set ff = (e | TM);

        

         A8: ( dom ff) = TM by PARTFUN1:def 2;

        now

          let tt be object;

          assume tt in TM;

          then

          reconsider ttt = tt as Element of TM;

          reconsider t = ttt as (mm + 1) -termal string of S by TARSKI:def 3, FOMODEL1:def 33;

          set ST = ( SubTerms t);

          ( dom f) = (T . mm) by FUNCT_2:def 1;

          then ( rng ST) c= ( dom f) by RELAT_1:def 19;

          then

           A9: (e * ST) = (f * ST) by RELAT_1: 165;

          reconsider s = (F . t) as termal Element of S;

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

          (f * ST) is FinSequence of (T . mm) by FOMODEL0: 26;

          then

          reconsider newtt = (f * ST) as l -element Element of ((T . mm) * );

          ((ff . ttt) \+\ (e . ttt)) = {} ;

          then

           A10: (ff . tt) = (e . tt) by FOMODEL0: 29;

          (s = l1 implies (e . <*s*>) = <*l2*> & ( ar s) = ( ar l2)) & (s <> l1 implies (e . <*s*>) = <*s*> & ( ar s) = ( ar s)) by FOMODEL0: 35;

          then

          consider ss be termal Element of S such that

           A11: (e . <*s*>) = <*ss*> & ( ar s) = ( ar ss);

          reconsider newttt = newtt as |.( ar ss).| -element Element of ((T . mm) * ) by A11;

          (e . t) = (e . ( <*(F . t)*> ^ (C . ST))) by FOMODEL1:def 37

          .= ((e . <*s*>) ^ (e . (C . ST))) by FOMODEL0: 36

          .= (ss -compound newttt) by FOMODEL0: 37, A9, A11;

          hence (ff . tt) in (T . (mm + 1)) by A10, FOMODEL1:def 33;

        end;

        hence thesis by A8, FUNCT_2: 3;

      end;

      for n holds P[n] from NAT_1:sch 2( A3, A6);

      hence thesis;

    end;

    definition

      let S, x, s, w;

      :: original: -SymbolSubstIn

      redefine

      func (x,s) -SymbolSubstIn w -> string of S ;

      coherence

      proof

        ((x,s) -SymbolSubstIn (w null w)) is (( len w) + 0 ) -element;

        hence thesis by FOMODEL0: 30;

      end;

    end

    registration

      let S, l1, l2, m;

      let t be m -termal string of S;

      cluster ((l1,l2) -SymbolSubstIn t) -> m -termal;

      coherence

      proof

        set e = (l1 SubstWith l2), T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S), IT = ((l1,l2) -SymbolSubstIn t);

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        reconsider f = (e | (T . m)) as Function of (T . m), (T . m) by Lm31;

        reconsider tt = t as Element of (T . m) by FOMODEL1:def 33;

        ((f . tt) \+\ (e . tt)) = {} ;

        then (f . tt) = (e . tt) by FOMODEL0: 29;

        then (e . t) in (T . mm);

        then IT in (T . mm) by FOMODEL0:def 22;

        hence thesis;

      end;

    end

    registration

      let S, t, l1, l2;

      cluster ((l1,l2) -SymbolSubstIn t) -> termal;

      coherence

      proof

        set IT = ((l1,l2) -SymbolSubstIn t), TT = ( AllTermsOf S), T = (S -termsOfMaxDepth );

        reconsider TF = T as Function;

        t in TT by FOMODEL1:def 32;

        then

        consider mm such that

         A1: t in (TF . mm) by FOMODEL1: 5;

        reconsider tm = t as mm -termal string of S by A1, FOMODEL1:def 33;

        ((l1,l2) -SymbolSubstIn tm) is mm -termal;

        hence thesis;

      end;

    end

    

     Lm32: ((l1 SubstWith l2) | ( AllTermsOf S)) is Function of ( AllTermsOf S), ( AllTermsOf S)

    proof

      set e = (l1 SubstWith l2), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S);

      (TT /\ ((SS * ) \ { {} })) = (TT null ((SS * ) \ { {} }))

      .= TT;

      then

      reconsider TTT = TT as non empty Subset of (SS * );

      set f = (e | TTT);

      

       A1: ( dom f) = TTT by PARTFUN1:def 2;

      now

        let x be object;

        assume

         A2: x in TTT;

        then

        reconsider t = x as termal string of S;

        reconsider xx = x as Element of TTT by A2;

        ((f . xx) \+\ (e . xx)) = {} ;

        

        then (f . xx) = (e . xx) by FOMODEL0: 29

        .= ((l1,l2) -SymbolSubstIn t) by FOMODEL0:def 22;

        hence (f . x) in TTT by FOMODEL1:def 32;

      end;

      hence thesis by FUNCT_2: 3, A1;

    end;

    registration

      let S, l1, l2;

      let phi be 0wff string of S;

      cluster ((l1,l2) -SymbolSubstIn phi) -> 0wff;

      coherence

      proof

        set psi = ((l1,l2) -SymbolSubstIn phi), e = (l1 SubstWith l2), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S), C = (S -multiCat );

        (TT /\ ((SS * ) \ { {} })) = (TT null ((SS * ) \ { {} }))

        .= TT;

        then

        reconsider TTT = TT as non empty Subset of (SS * );

        reconsider f = (e | TT) as Function of TT, TT by Lm32;

        consider r be relational Element of S, V be |.( ar r).| -element Element of (TT * ) such that

         A1: phi = ( <*r*> ^ (C . V)) by FOMODEL1:def 35;

        set m = |.( ar r).|;

        reconsider FV = V as m -element FinSequence of TT by FOMODEL0: 26;

        reconsider newstrings = (f * FV) as m -element FinSequence of TT;

        V in (TTT * );

        then

        reconsider VV = V as Element of ((SS * ) * );

        

         A2: ( rng V) c= TT & ( dom f) = TT by FUNCT_2:def 1, RELAT_1:def 19;

        psi = (e . phi) by FOMODEL0:def 22

        .= ((e . <*r*>) ^ (e . (C . VV))) by A1, FOMODEL0: 36

        .= ( <*r*> ^ (e . (C . VV))) by FOMODEL0: 35

        .= ( <*r*> ^ (C . (e * VV))) by FOMODEL0: 37

        .= ( <*r*> ^ (C . newstrings)) by A2, RELAT_1: 165;

        hence thesis;

      end;

    end

    registration

      let S;

      let m0 be zero number;

      let phi be m0 -wff string of S;

      cluster ( Depth phi) -> zero;

      coherence by FOMODEL2:def 31;

    end

    

     Lm33: ex psi2 be wff string of S st (( Depth psi1) = ( Depth psi2) & ((l1 SubstWith l2) . psi1) = psi2)

    proof

      set e = (l1 SubstWith l2), N = ( TheNorSymbOf S), L = ( LettersOf S);

      defpred Q[ wff string of S] means ex psi be wff string of S st (( Depth psi) = ( Depth $1) & (e . $1) = psi);

      defpred P[ Nat] means ( Depth phi) <= $1 implies Q[phi];

      

       A1: P[ 0 ]

      proof

        thus ( Depth phi) <= 0 implies Q[phi]

        proof

          set D = ( Depth phi);

          assume D <= 0 ;

          then D = 0 ;

          then

          reconsider p0 = phi as 0 -wff string of S by FOMODEL2:def 31;

          reconsider psi = ((l1,l2) -SymbolSubstIn p0) as 0wff string of S;

          take psi;

          thus ( Depth psi) = D;

          thus (e . phi) = psi by FOMODEL0:def 22;

        end;

      end;

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        set Fn = (S -formulasOfMaxDepth n);

        assume

         A3: P[n];

        thus ( Depth phi) <= (n + 1) implies Q[phi]

        proof

          set D = ( Depth phi);

          assume

           A4: D <= (n + 1);

          per cases ;

            suppose phi is 0wff;

            then

            reconsider p0 = phi as 0wff string of S;

            reconsider psi = ((l1,l2) -SymbolSubstIn p0) as 0wff string of S;

            take psi;

            thus ( Depth psi) = D;

            thus (e . phi) = psi by FOMODEL0:def 22;

          end;

            suppose

             A5: phi is exal;

            then

            consider m such that

             A6: D = (m + 1) by NAT_1: 6;

            phi in (m -ExFormulasOf S) by A6, A5, FOMODEL2: 18;

            then

            consider v be Element of L, phi1 be Element of (S -formulasOfMaxDepth m) such that

             A7: phi = ( <*v*> ^ phi1);

            reconsider l = v as literal Element of S;

            reconsider phi11 = phi1 as m -wff string of S by FOMODEL2:def 24;

            set m1 = ( Depth phi11);

            (m1 + 1) <= (n + 1) by A4, A7, FOMODEL2: 17;

            then

            consider psi1 be wff string of S such that

             A8: ( Depth psi1) = ( Depth phi11) & (e . phi11) = psi1 by A3, XREAL_1: 8;

            l = l1 or l <> l1;

            then (e . <*l*>) = <*l2*> or (e . <*l*>) = <*l*> by FOMODEL0: 35;

            then

            consider s be literal Element of S such that

             A9: (e . <*l*>) = <*s*>;

            take psi = ( <*s*> ^ psi1);

            

            thus ( Depth psi) = (( Depth psi1) + 1) by FOMODEL2: 17

            .= D by A8, A7, FOMODEL2: 17;

            thus (e . phi) = psi by A9, A8, A7, FOMODEL0: 36;

          end;

            suppose

             A10: not (phi is exal or phi is 0wff);

            then

            consider m such that

             A11: D = (m + 1) by NAT_1: 6;

            phi in (m -NorFormulasOf S) by FOMODEL2: 18, A10, A11;

            then

            consider phi1,phi2 be Element of (S -formulasOfMaxDepth m) such that

             A12: phi = (( <*N*> ^ phi1) ^ phi2);

            reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by FOMODEL2:def 24;

            set m1 = ( Depth phi11), m2 = ( Depth phi22), M = ( max (m1,m2));

            

             A13: ((M - m1) + m1) >= ( 0 + m1) & ((M - m2) + m2) >= ( 0 + m2) by XREAL_1: 6;

            (n + 1) >= (M + 1) by FOMODEL2: 17, A4, A12;

            then n >= M by XREAL_1: 8;

            then Q[phi11] & Q[phi22] by A3, A13, XXREAL_0: 2;

            then

            consider psi1,psi2 be wff string of S such that

             A14: ( Depth psi1) = ( Depth phi11) & (e . phi11) = psi1 & ( Depth psi2) = ( Depth phi22) & (e . phi22) = psi2;

            take psi = (( <*N*> ^ psi1) ^ psi2);

            

            thus D = (M + 1) by A12, FOMODEL2: 17

            .= ( Depth psi) by A14, FOMODEL2: 17;

            

            thus (e . phi) = ((e . ( <*N*> ^ phi11)) ^ (e . phi22)) by A12, FOMODEL0: 36

            .= (((e . <*N*>) ^ (e . phi11)) ^ psi2) by A14, FOMODEL0: 36

            .= psi by FOMODEL0: 35, A14;

          end;

        end;

      end;

      for n holds P[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    definition

      let S, m, w;

      :: original: null

      redefine

      func w null m -> string of S ;

      coherence ;

    end

    registration

      let S, phi, m;

      cluster (phi null m) -> (( Depth phi) + m) -wff;

      coherence

      proof

        set D = ( Depth phi);

        phi is (D + ( 0 * m)) -wff by FOMODEL2:def 31;

        hence thesis;

      end;

    end

    registration

      let S, m;

      let phi be m -wff string of S;

      cluster (m - ( Depth phi)) -> non negative;

      coherence

      proof

        set D = ( Depth phi);

        D <= m by FOMODEL2:def 31;

        then (D - D) <= (m - D) by XREAL_1: 9;

        hence thesis;

      end;

    end

    registration

      let S, l1, l2, m;

      let phi be m -wff string of S;

      cluster ((l1,l2) -SymbolSubstIn phi) -> m -wff;

      coherence

      proof

        set D = ( Depth phi), e = (l1 SubstWith l2);

        reconsider d = (m - D) as Nat;

        consider psi be wff string of S such that

         A1: ( Depth psi) = D & (e . phi) = psi by Lm33;

        set DD = ( Depth psi);

        (psi null d) is (DD + d) -wff;

        hence thesis by A1, FOMODEL0:def 22;

      end;

    end

    registration

      let S, l1, l2, phi;

      cluster ((l1,l2) -SymbolSubstIn phi) -> wff;

      coherence

      proof

        set psi = ((l1,l2) -SymbolSubstIn phi);

        consider m such that

         A1: phi is m -wff by FOMODEL2:def 25;

        thus thesis by A1;

      end;

    end

    

     Lm34: ( Depth psi1) = ( Depth ((l1,l2) -SymbolSubstIn psi1))

    proof

      set e = (l1 SubstWith l2), psi = ((l1,l2) -SymbolSubstIn psi1);

      consider psi2 such that

       A1: ( Depth psi2) = ( Depth psi1) & psi2 = (e . psi1) by Lm33;

      thus thesis by A1, FOMODEL0:def 22;

    end;

    registration

      let S, l1, l2, phi;

      cluster (( Depth ((l1,l2) -SymbolSubstIn phi)) \+\ ( Depth phi)) -> empty;

      coherence

      proof

        ( Depth ((l1,l2) -SymbolSubstIn phi)) = ( Depth phi) by Lm34;

        hence thesis;

      end;

    end

    theorem :: FOMODEL3:6

    for T be |.( ar a).| -element Element of (( AllTermsOf S) * ) holds ( not a is relational implies ((X -freeInterpreter a) . T) = (a -compound T)) & (a is relational implies ((X -freeInterpreter a) . T) = (( chi (X,( AtomicFormulasOf S))) . (a -compound T)))

    proof

      set AT = ( AllTermsOf S), SS = ( AllSymbolsOf S), I = (X -freeInterpreter a), f = (a -compound ), m = |.( ar a).|, g = (f | (m -tuples_on AT)), AF = ( AtomicFormulasOf S), ch = ( chi (X,AF));

      let T be m -element Element of (AT * );

      

       A1: ( dom f) = (((SS * ) \ { {} }) * ) by FUNCT_2:def 1;

      

       A2: (g . T) = (f . T) & (a -compound T) = (f . T) by FOMODEL0: 16, FUNCT_1: 49, Def2;

      thus not a is relational implies (I . T) = (a -compound T) by A2, Def3;

      assume a is relational;

      

      then I = (ch * g) by Def3

      .= ((ch * f) | (m -tuples_on AT)) by RELAT_1: 83;

      

      then (I . T) = ((ch * f) . T) by FUNCT_1: 49, FOMODEL0: 16

      .= (ch . (f . T)) by FUNCT_1: 13, A1;

      hence thesis by Def2;

    end;

    registration

      let S be Language;

      cluster termal for string of S;

      existence

      proof

        take w = <* the literal Element of S*>;

        thus thesis;

      end;

      cluster 0wff for string of S;

      existence

      proof

        take the Element of ( AtomicFormulasOf S);

        thus thesis;

      end;

    end

    theorem :: FOMODEL3:7

    

     Th7: (((I -TermEval ) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter )),tt0) -TermEval ) . n)) | ((S -termsOfMaxDepth ) . n)) = ((((((l,((I -TermEval ) . tt0)) ReassignIn I),((I -TermEval ) . tt0)) -TermEval ) . n) | ((S -termsOfMaxDepth ) . n))

    proof

      set II = (U -InterpretersOf S);

      reconsider u = ((I -TermEval ) . tt0) as Element of U;

      set F = (S -firstChar ), FI = ((S,X) -freeInterpreter ), H = ((l,tt0) ReassignIn FI), TT = ( AllTermsOf S), TI = ((I,u) -TermEval ), TF = ((FI,tt0) -TermEval ), TH = ((H,tt0) -TermEval ), TII = (I -TermEval ), J = ((l,(TII . tt0)) ReassignIn I), TJ = ((J,u) -TermEval ), C = (S -multiCat ), SS = ( AllSymbolsOf S), T = (S -termsOfMaxDepth );

      reconsider t0 = tt0 as termal string of S;

      set k = ( Depth t0);

      reconsider t00 = t0 as k -termal string of S by FOMODEL1:def 40;

      

       A1: l in {l} & ( dom (l .--> ( {} .--> tt0))) = {l} & ( dom (l .--> ( {} .--> (TII . tt0)))) = {l} by TARSKI:def 1;

      then (H . l) = ((l .--> ( {} .--> tt0)) . l) & (J . l) = ((l .--> ( {} .--> (TII . tt0))) . l) by FUNCT_4: 13;

      then

       A2: (H . l) = ( {} .--> tt0) & (J . l) = ( {} .--> (TII . tt0)) by A1, FUNCOP_1: 7;

      defpred P[ Nat] means ((TII * (TH . $1)) | (T . $1)) = ((TJ . $1) | (T . $1));

      

       A3: P[ 0 ]

      proof

        

         A4: ( dom (TT --> u)) = TT & ( dom (TT --> tt0)) = TT & ( dom TII) = TT by FUNCT_2:def 1;

        (TI . 0 ) = (TT --> u) & (TH . 0 ) = (TT --> tt0) by FOMODEL2:def 8;

        

        then (TII * (TH . 0 )) = (TT --> (TII . tt0)) by FUNCOP_1: 17, A4

        .= (TJ . 0 ) by FOMODEL2:def 8;

        hence thesis;

      end;

      

       A5: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        reconsider mm = m, MM = (m + 1) as Element of NAT by ORDINAL1:def 12;

        assume

         A6: P[m];

        reconsider TM = (T . MM), Tm = (T . mm) as Subset of TT by FOMODEL1: 2;

        (TJ . mm) is Element of ( Funcs (TT,U)) & (TI . MM) is Element of ( Funcs (TT,U)) & (TJ . MM) is Element of ( Funcs (TT,U)) & (TI . mm) is Element of ( Funcs (TT,U));

        then

        reconsider Jm = (TJ . mm), JM = (TJ . MM), IM = (TI . MM), Imm = (TI . mm) as Function of TT, U;

        (TH . mm) is Element of ( Funcs (TT,TT)) & (TH . MM) is Element of ( Funcs (TT,TT));

        then

        reconsider Hm = (TH . mm), HM = (TH . MM) as Function of TT, TT;

        set LH = ((TII * HM) | TM), RH = (JM | TM);

        

         A7: ( dom LH) = TM & ( dom RH) = TM by PARTFUN1:def 2;

        now

          let x be object;

          assume

           A8: x in ( dom LH);

          then

          reconsider tt = x as Element of TT by A7;

          reconsider t = x as (mm + 1) -termal string of S by A7, FOMODEL1:def 33, A8;

          reconsider ttt = x as Element of TM by A8;

          set ST = ( SubTerms t), o = (F . t), n = |.( ar o).|;

          ((((IM * HM) | TM) . ttt) \+\ ((IM * HM) . ttt)) = {} & (((JM | TM) . ttt) \+\ (JM . ttt)) = {} & ((((TII * HM) | TM) . ttt) \+\ ((TII * HM) . ttt)) = {} ;

          then

           A9: (((IM * HM) | TM) . x) = ((IM * HM) . x) & ((JM | TM) . x) = (JM . x) & (((TII * HM) | TM) . x) = ((TII * HM) . x) by FOMODEL0: 29;

          (((IM * HM) . tt) \+\ (IM . (HM . tt))) = {} & (((TII * HM) . tt) \+\ (TII . (HM . tt))) = {} ;

          then

           A10: ((IM * HM) . t) = (IM . (HM . t)) & ((TII * HM) . tt) = (TII . (HM . tt)) by FOMODEL0: 29;

          reconsider newterms = (Hm * ST) as n -element FinSequence of TT by FOMODEL0: 26;

          reconsider newtermss = newterms as Element of (n -tuples_on TT) by FOMODEL0: 16;

          reconsider newtermsss = newterms as FinSequence of ((SS * ) \ { {} }) by FOMODEL0: 26;

          ((((o -compound ) | (n -tuples_on TT)) . newtermss) \+\ ((o -compound ) . newtermss)) = {} ;

          then

           A11: (((o -compound ) | (n -tuples_on TT)) . newterms) = ((o -compound ) . newterms) by FOMODEL0: 29;

          per cases ;

            suppose o = l;

            then o = l & t is 0 -termal by FOMODEL1: 16;

            then ((TII * HM) . t) = (TII . (( {} .--> tt0) . {} )) & (JM . t) = (( {} .--> (TII . tt0)) . {} ) & {} in { {} } by FOMODEL2: 3, TARSKI:def 1, A10, A2;

            then ((TII * HM) . t) = (TII . tt0) & (JM . t) = (TII . tt0) by FUNCOP_1: 7;

            hence (LH . x) = (RH . x) by A9;

          end;

            suppose o <> l;

            then

             A12: not o in ( dom (l .--> ( {} .--> tt0))) & not o in ( dom (l .--> ( {} .--> (TII . tt0)))) by TARSKI:def 1;

            then (FI . o) = (H . o) by FUNCT_4: 11;

            

            then (H . o) = (X -freeInterpreter o) by Def4

            .= ((o -compound ) | (n -tuples_on TT)) by Def3;

            then

             A13: ((H . o) . newterms) = (o -compound newtermsss) by A11, Def2;

            reconsider newtermssss = newterms as n -element Element of (TT * );

            reconsider t1 = (o -compound newtermssss) as termal string of S;

            set p = ( Depth t1);

            reconsider pp = p as Element of NAT by ORDINAL1:def 12;

            reconsider t111 = t1 as p -termal string of S by FOMODEL1:def 40;

            reconsider t11 = t1 as Element of TT by FOMODEL1:def 32;

            (TI . pp) is Element of ( Funcs (TT,U));

            then

            reconsider Ip = (TI . pp) as Function of TT, U;

            

             A14: (F . t1) = (t1 . 1) by FOMODEL0: 6

            .= o by FINSEQ_1: 41;

            then

             A15: ( SubTerms t1) = newtermssss by FOMODEL1:def 37;

            

             A16: ( dom (Hm | Tm)) = Tm & ( dom (Jm | Tm)) = Tm & ( rng ST) c= Tm by RELAT_1:def 19, PARTFUN1:def 2;

            ((TII * HM) . t) = (TII . t1) by A13, FOMODEL2: 3, A10

            .= ((I . o) . (TII * ( SubTerms t1))) by A14, FOMODEL2: 21

            .= ((I . o) . (TII * ((Hm | Tm) * ST))) by A16, RELAT_1: 165, A15

            .= ((I . o) . ((TII * (Hm | Tm)) * ST)) by RELAT_1: 36

            .= ((I . o) . (((TII * Hm) | Tm) * ST)) by RELAT_1: 83

            .= ((I . o) . (Jm * ST)) by A6, A16, RELAT_1: 165

            .= ((J . o) . (Jm * ST)) by FUNCT_4: 11, A12

            .= (JM . t) by FOMODEL2: 3;

            hence (LH . x) = (RH . x) by A9;

          end;

        end;

        hence thesis by A7, FUNCT_1: 2;

      end;

      for m holds P[m] from NAT_1:sch 2( A3, A5);

      hence thesis;

    end;

    definition

      let S, l, tt, phi0;

      :: FOMODEL3:def19

      func (l,tt) AtomicSubst phi0 -> FinSequence equals ( <*((S -firstChar ) . phi0)*> ^ ((S -multiCat ) . ((((l,tt) ReassignIn ((S, {} ) -freeInterpreter )) -TermEval ) * ( SubTerms phi0))));

      coherence ;

    end

    

     Lm35: ((l,tt) AtomicSubst phi0) is 0wff string of S

    proof

      set ST = ( SubTerms phi0), FI = ((S, {} ) -freeInterpreter ), I = ((l,tt) ReassignIn FI), C = (S -multiCat ), F = (S -firstChar ), r = (F . phi0), n = |.( ar r).|, TT = ( AllTermsOf S), TE = (I -TermEval ), SS = ( AllSymbolsOf S);

      reconsider STT = ST as FinSequence of TT by FOMODEL0: 26;

      reconsider newterms = (TE * STT) as FinSequence of TT;

      reconsider newtermss = newterms as Element of ((SS * ) * ) by TARSKI:def 3;

      reconsider IT = ( <*(F . phi0)*> ^ (C . newtermss)) as string of S by FOMODEL0: 30;

      IT is 0wff;

      hence thesis;

    end;

    definition

      let S, l, tt, phi0;

      :: original: AtomicSubst

      redefine

      func (l,tt) AtomicSubst phi0 -> string of S ;

      coherence by Lm35;

    end

    registration

      let S, l, tt, phi0;

      cluster ((l,tt) AtomicSubst phi0) -> 0wff;

      coherence by Lm35;

    end

    

     Lm36: ((S -firstChar ) . ((l,tt) AtomicSubst phi0)) = ((S -firstChar ) . phi0) & ( SubTerms ((l,tt) AtomicSubst phi0)) = ((((l,tt) ReassignIn ((S, {} ) -freeInterpreter )) -TermEval ) * ( SubTerms phi0))

    proof

      set psi0 = ((l,tt) AtomicSubst phi0), F = (S -firstChar ), C = (S -multiCat ), TT = ( AllTermsOf S), FI = ((S, {} ) -freeInterpreter ), I = ((l,tt) ReassignIn FI), s1 = (F . phi0), s2 = (F . psi0), n1 = |.( ar s1).|, n2 = |.( ar s2).|;

      

      thus

       A1: (F . psi0) = (psi0 . 1) by FOMODEL0: 6

      .= (F . phi0) by FINSEQ_1: 41;

      reconsider ST = ( SubTerms phi0) as n1 -element FinSequence of TT by FOMODEL0: 26;

      reconsider newST = ((I -TermEval ) * ST) as n2 -element FinSequence of TT by A1;

      newST = ( SubTerms psi0) by A1, FOMODEL1:def 38;

      hence thesis;

    end;

    

     Lm37: ((I -TermEval ) * (((l,tt) ReassignIn ((S,X) -freeInterpreter )) -TermEval )) = (((l,((I -TermEval ) . tt)) ReassignIn I) -TermEval )

    proof

      set TI = (I -TermEval ), u = (TI . tt), J = ((l,u) ReassignIn I), TJ = (J -TermEval ), F = (S -firstChar ), C = (S -multiCat ), FI = ((S,X) -freeInterpreter ), FJ = ((l,tt) ReassignIn FI), TF = (FJ -TermEval ), TT = ( AllTermsOf S), T = (S -termsOfMaxDepth );

      reconsider LH = (TI * TF), RH = TJ as Function of TT, U;

      now

        let tt0 be Element of TT;

        reconsider t = tt0 as termal string of S;

        set n = ( Depth t);

        reconsider nn = n, NN = (n + 1) as Element of NAT by ORDINAL1:def 12;

        reconsider tn = t as n -termal string of S by FOMODEL1:def 40;

        tn is (n + ( 0 * 1)) -termal;

        then

        reconsider tN = tn as NN -termal string of S;

        reconsider TN = (T . NN), Tn = (T . nn) as Subset of TT by FOMODEL1: 2;

        reconsider tnn = tn as Element of Tn by FOMODEL1:def 33;

        reconsider tNN = tN as Element of TN by FOMODEL1:def 33;

        (((FJ,tt) -TermEval ) . NN) is Element of ( Funcs (TT,TT));

        then

        reconsider FJN = (((FJ,tt) -TermEval ) . NN) as Function of TT, TT;

        (((J,u) -TermEval ) . NN) is Element of ( Funcs (TT,U));

        then

        reconsider JN = (((J,u) -TermEval ) . NN) as Function of TT, U;

        ((TI . (FJN . tt0)) \+\ ((TI * FJN) . tt0)) = {} & ((((TI * FJN) | TN) . tNN) \+\ ((TI * FJN) . tNN)) = {} & (((JN | TN) . tNN) \+\ (JN . tNN)) = {} ;

        then

         A1: ((TI * FJN) . tt0) = (TI . (FJN . tt0)) & (((TI * FJN) | TN) . tt0) = ((TI * FJN) . tt0) & ((JN | TN) . tt0) = (JN . tt0) by FOMODEL0: 29;

        ((LH . tt0) \+\ (TI . (TF . tt0))) = {} ;

        

        then (LH . tt0) = (TI . (TF . tt0)) by FOMODEL0: 29

        .= (TI . (FJ -TermEval tt0)) by FOMODEL2:def 10

        .= (TI . (FJN . tnn)) by FOMODEL2:def 9

        .= ((((J,u) -TermEval ) . NN) . tnn) by A1, Th7

        .= (J -TermEval tt0) by FOMODEL2:def 9

        .= (TJ . tt0) by FOMODEL2:def 10;

        hence (LH . tt0) = (RH . tt0);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FOMODEL3:8

    

     Th8: (I -AtomicEval ((l,tt) AtomicSubst phi0)) = (((l,((I -TermEval ) . tt)) ReassignIn I) -AtomicEval phi0)

    proof

      set psi0 = ((l,tt) AtomicSubst phi0), u = ((I -TermEval ) . tt), J = ((l,u) ReassignIn I), F = (S -firstChar ), C = (S -multiCat ), FI = ((S, {} ) -freeInterpreter ), s1 = (F . phi0), s2 = (F . psi0), n1 = |.( ar s1).|, n2 = |.( ar s2).|, TI = (I -TermEval ), TJ = (J -TermEval ), E = ( TheEqSymbOf S), FJ = ((l,tt) ReassignIn FI), d = (U -deltaInterpreter );

       not s1 in ( dom (l .--> ( {} .--> u))) by TARSKI:def 1;

      then

       A1: s1 = s2 & (J . s1) = (I . s1) by FUNCT_4: 11, Lm36;

      

       A2: (TI * ( SubTerms psi0)) = (TI * ((FJ -TermEval ) * ( SubTerms phi0))) by Lm36

      .= ((TI * (FJ -TermEval )) * ( SubTerms phi0)) by RELAT_1: 36

      .= (TJ * ( SubTerms phi0)) by Lm37;

      per cases ;

        suppose

         A3: s2 <> E;

        

        then (I -AtomicEval psi0) = ((J . s1) . (TJ * ( SubTerms phi0))) by FOMODEL2: 14, A1, A2

        .= (J -AtomicEval phi0) by FOMODEL2: 14, A3, A1;

        hence thesis;

      end;

        suppose

         A4: s2 = E;

        

        then (I -AtomicEval psi0) = (d . (TI * ( SubTerms psi0))) by FOMODEL2: 14

        .= (J -AtomicEval phi0) by FOMODEL2: 14, A4, A1, A2;

        hence thesis;

      end;

    end;

    registration

      let S, l1, l2, m;

      cluster ((l1 SubstWith l2) | ((S -termsOfMaxDepth ) . m)) -> ((S -termsOfMaxDepth ) . m) -valued;

      coherence

      proof

        set s = (l1 SubstWith l2), T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S);

        reconsider Tm = (T . m) as Subset of (SS * ) by XBOOLE_1: 1;

        set f = (s | Tm);

        

         A1: ( dom f) = Tm by PARTFUN1:def 2;

        now

          let x be object;

          assume x in Tm;

          then

          reconsider xx = x as Element of Tm;

          reconsider t = xx as m -termal string of S by TARSKI:def 3, FOMODEL1:def 33;

          ((f . xx) \+\ (s . xx)) = {} ;

          

          then (f . x) = (s . t) by FOMODEL0: 29

          .= ((l1,l2) -SymbolSubstIn t) by FOMODEL0:def 22;

          hence (f . x) in (T . m) by FOMODEL1:def 33;

        end;

        hence thesis by FUNCT_2: 3, A1;

      end;

    end

    registration

      let S, l1, l2;

      cluster ((l1 SubstWith l2) | ( AllTermsOf S)) -> ( AllTermsOf S) -valued;

      coherence

      proof

        set f = (l1 SubstWith l2), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S);

        reconsider TTT = TT as non empty Subset of (SS * ) by XBOOLE_1: 1;

        

         A1: ( dom (f | TTT)) = TTT by PARTFUN1:def 2;

        now

          let x be object;

          assume x in TTT;

          then

          reconsider tt = x as Element of TTT;

          reconsider t = tt as termal string of S by TARSKI:def 3;

          (((f | TTT) . tt) \+\ (f . tt)) = {} ;

          

          then ((f | TTT) . x) = (f . t) by FOMODEL0: 29

          .= ((l1,l2) -SymbolSubstIn t) by FOMODEL0:def 22;

          hence ((f | TTT) . x) in TTT by FOMODEL1:def 32;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    

     Lm38: ( SubTerms ((l1,l2) -SymbolSubstIn t)) = ((l1 SubstWith l2) * ( SubTerms t))

    proof

      set s = (l1 SubstWith l2), newt = ((l1,l2) -SymbolSubstIn t), ST = ( SubTerms t), F = (S -firstChar ), C = (S -multiCat ), ST2 = ( SubTerms newt), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S);

      reconsider TTT = TT as Subset of (SS * ) by XBOOLE_1: 1;

      

       A1: ( rng ST) c= TT & ( dom (s | TTT)) = TTT & ( rng (s | TT)) c= TT by RELAT_1:def 19, PARTFUN1:def 2;

      then

      reconsider ss = (s | TT) as Function of TT, TT by FUNCT_2: 2;

      per cases ;

        suppose not t is 0 -termal;

        then

        reconsider s1 = (F . t) as non literal ofAtomicFormula Element of S by FOMODEL1: 16;

        reconsider h = ((l1,l2) -SymbolSubstIn <*s1*>) as 1 -elementSS -valued FinSequence;

        set s2 = (F . newt), n1 = |.( ar s1).|, n2 = |.( ar s2).|;

        (ss * ST) = (s * ST) by RELAT_1: 165, A1;

        then

        reconsider p = (s * ST) as n1 -element FinSequence of TT by FOMODEL0: 26;

        

         A2: newt = ( <*s2*> ^ (C . ST2)) by FOMODEL1:def 37;

        t = ( <*s1*> ^ (C . ST)) by FOMODEL1:def 37;

        

        then (s . t) = ((s . <*s1*>) ^ (s . (C . ST))) by FOMODEL0: 36

        .= (h ^ (s . (C . ST))) by FOMODEL0:def 22

        .= (h ^ (C . (s * ST))) by FOMODEL0: 37;

        then

         A3: newt = (h ^ (C . p)) by FOMODEL0:def 22;

        then h = <*s2*> & h = <*s1*> by A2, FOMODEL0: 41, FOMODEL0: 34;

        then (h . 1) = s1 & (h . 1) = s2 by FINSEQ_1: 40;

        then

        reconsider pp = p as n2 -element Element of (TT * );

        newt = ( <*s2*> ^ (C . pp)) by A3, A2, FOMODEL0: 41;

        hence thesis by FOMODEL1:def 37;

      end;

        suppose t is 0 -termal;

        then

        reconsider t0 = t as 0 -termal string of S;

        reconsider newt = ((l1,l2) -SymbolSubstIn t0) as 0 -termal string of S;

        ( SubTerms newt) = {} & ( SubTerms t0) = {} ;

        hence thesis;

      end;

    end;

    

     Lm39: ( SubTerms ((l1,l2) -SymbolSubstIn phi0)) = ((l1 SubstWith l2) * ( SubTerms phi0))

    proof

      set s = (l1 SubstWith l2), psi0 = ((l1,l2) -SymbolSubstIn phi0), ST1 = ( SubTerms phi0), F = (S -firstChar ), C = (S -multiCat ), ST2 = ( SubTerms psi0), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S);

      reconsider TTT = TT as Subset of (SS * ) by XBOOLE_1: 1;

      

       A1: ( rng ST1) c= TT & ( dom (s | TTT)) = TTT & ( rng (s | TT)) c= TT by RELAT_1:def 19, PARTFUN1:def 2;

      then

      reconsider ss = (s | TT) as Function of TT, TT by FUNCT_2: 2;

      reconsider r1 = (F . phi0), r2 = (F . psi0) as relational Element of S;

      (phi0 . 1) = r1 by FOMODEL0: 6;

      then r1 = (phi0 . 1) & (psi0 . 1) = (phi0 . 1) by FUNCT_4: 105;

      then

       A2: r1 = r2 by FOMODEL0: 6;

      set n1 = |.( ar r1).|, n2 = |.( ar r2).|;

      (s * ST1) = (ss * ST1) by RELAT_1: 165, A1;

      then (s * ST1) is n2 -element FinSequence of TT by FOMODEL0: 26, A2;

      then

      reconsider ST22 = (s * ST1) as n2 -element Element of (TT * );

      reconsider ST11 = ST1 as (SS * ) -valued FinSequence;

      phi0 = ( <*r1*> ^ (C . ST1)) by FOMODEL1:def 38;

      

      then (s . phi0) = ((s . <*r1*>) ^ (s . (C . ST1))) by FOMODEL0: 36

      .= ( <*r1*> ^ (s . (C . ST1))) by FOMODEL0: 35

      .= ( <*r2*> ^ (C . ST22)) by FOMODEL0: 37, A2;

      then psi0 = ( <*r2*> ^ (C . ST22)) by FOMODEL0:def 22;

      hence thesis by FOMODEL1:def 38;

    end;

    

     Lm40: ((((l1,u) ReassignIn I) -TermEval ) | (((( AllSymbolsOf S) \ {l2}) * ) /\ ((S -termsOfMaxDepth ) . m))) = (((((l2,u) ReassignIn I) -TermEval ) * (l1 SubstWith l2)) | (((( AllSymbolsOf S) \ {l2}) * ) /\ ((S -termsOfMaxDepth ) . m)))

    proof

      set I1 = ((l1,u) ReassignIn I), I2 = ((l2,u) ReassignIn I), s = (l1 SubstWith l2), E1 = (I1 -TermEval ), E2 = (I2 -TermEval ), T = (S -termsOfMaxDepth ), TT = ( AllTermsOf S), SS = ( AllSymbolsOf S), F = (S -firstChar ), C = (S -multiCat ), g1 = (l1 .--> ( {} .--> u)), g2 = (l2 .--> ( {} .--> u)), L = ( LettersOf S);

      reconsider SSS = (SS \ {l2}) as non empty Subset of SS;

      set D = (SSS * );

      l1 in {l1} & l2 in {l2} by TARSKI:def 1;

      then l1 in ( dom g1) & l2 in ( dom g2);

      then (I1 . l1) = (g1 . l1) & (I2 . l2) = (g2 . l2) by FUNCT_4: 13;

      then

       A1: (I1 . l1) = ( {} .--> u) & (I2 . l2) = ( {} .--> u) by FUNCOP_1: 72;

      defpred P[ Nat] means (E1 | ((T . $1) /\ D)) = ((E2 * s) | ((T . $1) /\ D));

      

       A2: P[ 0 ]

      proof

        reconsider T0 = (T . 0 ) as non empty Subset of TT by FOMODEL1: 2;

        reconsider T00 = T0 as non empty Subset of (SS * ) by XBOOLE_1: 1;

        reconsider ss = (s | (T . 0 )) as (T . 0 ) -valued Function;

        reconsider X0 = (T0 /\ D) as Subset of T0;

        reconsider X = (T0 /\ D) as Subset of TT by XBOOLE_1: 1;

        (ss | D) is T0 -valued;

        then

        reconsider sss = (s | (T0 /\ D)) as T00 -valued Function by RELAT_1: 71;

        

         A3: ( dom (E2 * sss)) = X & ( dom (E1 | X)) = X by PARTFUN1:def 2;

        ( rng (E2 * sss)) c= U & ( rng (E1 | X)) c= U by RELAT_1:def 19;

        then

        reconsider f1 = (E1 | X), f2 = (E2 * sss) as Function of X, U by FUNCT_2: 2, A3;

        now

          let x be object;

          assume

           A4: x in X;

          then

          reconsider X00 = X0 as non empty Subset of D;

          ( dom sss) = X & ( rng sss) c= T0 by PARTFUN1:def 2, RELAT_1:def 19;

          then

          reconsider ssss = sss as Function of X00, T0 by FUNCT_2: 2;

          reconsider xx = x as Element of X00 by A4;

          reconsider xd = xx as Element of D;

          reconsider t0 = x as 0 -termal string of S by TARSKI:def 3, FOMODEL1:def 33, A4;

          reconsider t00 = t0 as Element of T0 by FOMODEL1:def 33;

          T0 = ( AtomicTermsOf S) by FOMODEL1:def 30;

          then

          reconsider tl = t00 as 1 -element FinSequence of L by FOMODEL0: 12;

          reconsider LL = (L \ {l2}) as non empty Subset of L;

          ( rng tl) c= L & ( rng xd) c= (SS \ {l2}) by RELAT_1:def 19;

          then ( rng xx) c= (L /\ (SS \ {l2})) by XBOOLE_1: 19;

          then ( rng xx) c= ((L null SS) \ {l2}) by XBOOLE_1: 49;

          then

          reconsider xxx = tl as 1 -elementLL -valued FinSequence by RELAT_1:def 19;

          ( {(xxx . 1)} \ LL) = {} ;

          then

          reconsider lx = (xxx . 1) as Element of LL by ZFMISC_1: 60;

           not lx in {l2} by XBOOLE_0:def 5;

          then

           A5: lx <> l2 & not lx in ( dom g2) by TARSKI:def 1;

          

           A6: ( len xxx) = 1 by CARD_1:def 7;

          reconsider newt = ((l1,l2) -SymbolSubstIn t0) as 0 -termal string of S;

          reconsider s1 = (F . t0), s2 = (F . newt) as literal Element of S;

          

           A7: s1 = lx & s2 = (newt . 1) by FOMODEL0: 6;

          (((E2 * ssss) . xx) \+\ (E2 . (ssss . xx))) = {} & ((sss . xx) \+\ (s . xx)) = {} & ((f1 . xx) \+\ (E1 . xx)) = {} ;

          then

           A8: ((E2 * sss) . x) = (E2 . (sss . x)) & (sss . x) = (s . x) & (f1 . x) = (E1 . x) by FOMODEL0: 29;

          

           A9: (f2 . x) = (E2 . newt) by A8, FOMODEL0:def 22

          .= ((I2 . s2) . (E2 * ( SubTerms newt))) by FOMODEL2: 21

          .= ((I2 . s2) . {} );

          

           A10: (f1 . x) = ((I1 . s1) . (E1 * ( SubTerms t0))) by A8, FOMODEL2: 21

          .= ((I1 . s1) . {} );

          per cases ;

            suppose

             A11: lx = l1;

            t0 = <*l1*> by A6, FINSEQ_1: 40, A11;

            then newt = <*l2*> by FOMODEL0: 34;

            hence (f1 . x) = (f2 . x) by A11, A10, A1, A9, A7, FINSEQ_1: 40;

          end;

            suppose lx <> l1;

            then (newt . 1) = lx & not lx in {l1} by FUNCT_4: 105, TARSKI:def 1;

            then s2 = lx & not lx in ( dom g1) by FOMODEL0: 6;

            then (f2 . x) = ((I . lx) . {} ) & (f1 . x) = ((I . lx) . {} ) by A7, A9, A10, FUNCT_4: 11, A5;

            hence (f1 . x) = (f2 . x);

          end;

        end;

        then f1 = f2 by FUNCT_2: 12;

        hence thesis by RELAT_1: 83;

      end;

      

       A12: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        reconsider nn = n, NN = (n + 1) as Element of NAT by ORDINAL1:def 12;

        assume

         A13: P[n];

        reconsider Tnn = (T . nn), TNN = (T . NN) as non empty Subset of TT by FOMODEL1: 2;

        reconsider Xn = (Tnn /\ D), X = (TNN /\ D) as Subset of TT by XBOOLE_1: 1;

        ((s | (T . NN)) | D) is TNN -valued;

        then

        reconsider sX = (s | X) as TT -valued Function by RELAT_1: 71;

        ( dom (s | X)) = X & ( rng sX) c= TT by PARTFUN1:def 2, RELAT_1:def 19;

        then

        reconsider sXX = sX as Function of X, TT by FUNCT_2: 2;

        ((s | (T . nn)) | D) is Tnn -valued;

        then

        reconsider sXn = (s | Xn) as TT -valued Function by RELAT_1: 71;

        

         A14: ( dom (E1 | X)) = X & ( dom (E2 * sX)) = X & ( dom (E2 * sXn)) = Xn by PARTFUN1:def 2;

        ( rng (E1 | X)) c= U & ( rng (E2 * sX)) c= U by RELAT_1:def 19;

        then

        reconsider f1 = (E1 | X), f2 = (E2 * sX) as Function of X, U by FUNCT_2: 2, A14;

        now

          let x be object;

          assume

           A15: x in X;

          then

          reconsider XX = X as non empty Subset of TNN;

          reconsider xxx = x as Element of XX by A15;

          reconsider xx = xxx as Element of D by A15;

          reconsider tN = x as Element of TNN by A15;

          reconsider t = tN as NN -termal string of S by TARSKI:def 3, FOMODEL1:def 33;

          reconsider ttt = t as Element of TT;

          set d = ( Depth t);

          reconsider aux = ( rng xx) as Subset of (SS \ {l2}) by RELAT_1:def 19;

          (aux * ) c= D & ( rng ( SubTerms t)) c= (( rng t) * ) by RELAT_1:def 19;

          then

           A16: ( rng ( SubTerms t)) c= D by XBOOLE_1: 1;

          reconsider tt = t as (nn + 1) -termal string of S;

          reconsider newt = ((l1,l2) -SymbolSubstIn t) as NN -termal string of S;

          

           A17: ( rng ( SubTerms tt)) c= (T . nn) by RELAT_1:def 19;

          

           A18: ( dom (E1 | Xn)) = Xn & ( dom ((E2 * s) | Xn)) = Xn by A14, RELAT_1: 83, PARTFUN1:def 2;

          ((f1 . xxx) \+\ (E1 . xxx)) = {} & (((s | XX) . xxx) \+\ (s . xxx)) = {} & (((E2 * sXX) . xxx) \+\ (E2 . (sXX . xxx))) = {} ;

          then

           A19: (f1 . x) = (E1 . x) & (sX . x) = (s . x) & (f2 . x) = (E2 . (sX . x)) by FOMODEL0: 29;

          per cases ;

            suppose d = 0 ;

            then

            reconsider t0 = t as 0 -termal string of S by FOMODEL1:def 40;

            reconsider l = (F . t0) as literal Element of S;

            

             A20: t0 = ( <*l*> ^ (C . ( SubTerms t0))) by FOMODEL1:def 37

            .= ( <*l*> null {} );

            ( {(xx . 1)} \ SSS) = {} ;

            then (t0 . 1) in SSS by ZFMISC_1: 60;

            then l in SSS by FOMODEL0: 6;

            then not l in ( dom g2) by XBOOLE_0:def 5;

            then

             A21: (I2 . l) = (I . l) by FUNCT_4: 11;

            

             A22: (f1 . t0) = ((I1 . l) . (E1 * ( SubTerms t0))) by FOMODEL2: 21, A19

            .= ((I1 . l) . {} );

            per cases ;

              suppose

               A23: l in ( dom g1);

              l = l1 by A23, TARSKI:def 1;

              then (f1 . t0) = ((I1 . l1) . {} ) & (s . t0) = <*l2*> by A22, FOMODEL0: 35, A20;

              

              then (f2 . t0) = ((I2 . (F . <*l2*>)) . (E2 * ( SubTerms <*l2*>))) by FOMODEL2: 21, A19

              .= ((I2 . ( <*l2*> . 1)) . {} ) by FOMODEL0: 6

              .= ((I2 . l2) . {} ) by FINSEQ_1: 40;

              hence (f2 . x) = (f1 . x) by A23, TARSKI:def 1, A22, A1;

            end;

              suppose

               A24: not l in ( dom g1);

              then (f1 . t0) = ((I . l) . {} ) & not l in {l1} by A22, FUNCT_4: 11;

              then l <> l1 by TARSKI:def 1;

              then (s . t0) = t0 by A20, FOMODEL0: 35;

              

              then (f2 . t0) = ((I2 . l) . (E2 * ( SubTerms t0))) by A19, FOMODEL2: 21

              .= ((I2 . l) . {} );

              hence (f2 . x) = (f1 . x) by A24, A22, FUNCT_4: 11, A21;

            end;

          end;

            suppose d <> 0 ;

            then

             A25: not t is 0 -termal;

            then

            reconsider s1 = (F . t) as non literal ofAtomicFormula Element of S by FOMODEL1: 16;

            (t . 1) = (F . t) & (F . t) is non literal by FOMODEL1: 16, A25, FOMODEL0: 6;

            then (newt . 1) = s1 by FUNCT_4: 105;

            then

            reconsider s2 = (F . newt) as non literal ofAtomicFormula Element of S by FOMODEL0: 6;

            ( not s1 in ( dom g1)) & ( not s2 in ( dom g2)) by TARSKI:def 1;

            then

             A26: (I1 . s1) = (I . s1) & (I2 . s2) = (I . s2) by FUNCT_4: 11;

            s1 <> l1;

            then (t . 1) <> l1 by FOMODEL0: 6;

            

            then (newt . 1) = (t . 1) by FUNCT_4: 105

            .= s1 by FOMODEL0: 6;

            then

             A27: s1 = s2 by FOMODEL0: 6;

            

            thus (f2 . x) = (E2 . newt) by A19, FOMODEL0:def 22

            .= ((I2 . s2) . (E2 * ( SubTerms newt))) by FOMODEL2: 21

            .= ((I2 . s2) . (E2 * (s * ( SubTerms t)))) by Lm38

            .= ((I . s2) . ((E2 * s) * ( SubTerms t))) by A26, RELAT_1: 36

            .= ((I . s2) . (((E2 * s) | ((T . n) /\ D)) * ( SubTerms t))) by RELAT_1: 165, A17, A16, XBOOLE_1: 19, A18

            .= ((I . s2) . (E1 * ( SubTerms t))) by RELAT_1: 165, A17, A16, XBOOLE_1: 19, A18, A13

            .= (f1 . x) by A19, A26, A27, FOMODEL2: 21;

          end;

        end;

        then f1 = f2 by FUNCT_2: 12;

        hence thesis by RELAT_1: 83;

      end;

      for m holds P[m] from NAT_1:sch 2( A2, A12);

      hence thesis;

    end;

    

     Lm41: phi0 is (( AllSymbolsOf S) \ {l2}) -valued implies (((l1,u) ReassignIn I) -AtomicEval phi0) = (((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0))

    proof

      set I1 = ((l1,u) ReassignIn I), I2 = ((l2,u) ReassignIn I), s = (l1 SubstWith l2), E1 = (I1 -TermEval ), E2 = (I2 -TermEval ), T = (S -termsOfMaxDepth ), TT = ( AllTermsOf S), SS = ( AllSymbolsOf S), F = (S -firstChar ), C = (S -multiCat ), g1 = (l1 .--> ( {} .--> u)), g2 = (l2 .--> ( {} .--> u)), L = ( LettersOf S), E = ( TheEqSymbOf S), d = (U -deltaInterpreter ), SSS = (SS \ {l2});

      reconsider SSSS = SSS as non empty Subset of SS;

      reconsider psi0 = ((l1,l2) -SymbolSubstIn phi0) as 0wff string of S;

      reconsider r = (F . phi0), r2 = (F . psi0) as relational Element of S;

      (phi0 . 1) = r by FOMODEL0: 6;

      

      then

       A1: r = (psi0 . 1) by FUNCT_4: 105

      .= r2 by FOMODEL0: 6;

       not r in ( dom g1) & not r in ( dom g2) by TARSKI:def 1;

      then

       A2: (I1 . r) = (I . r) & (I2 . r) = (I . r) by FUNCT_4: 11;

      ( dom E1) = TT & ( dom E2) = TT by FUNCT_2:def 1;

      then

       A3: ( dom (E1 | (SSS * ))) = (TT /\ (SSS * )) & ( dom (s | (SSSS * ))) = (SSSS * ) by PARTFUN1:def 2, RELAT_1: 61;

      reconsider ST1 = ( SubTerms phi0) as Element of (TT * );

      consider mm such that

       A4: ( SubTerms phi0) is Element of ((T . mm) * ) by Lm3;

      reconsider Tm = (T . mm) as non empty Subset of TT by FOMODEL1: 2;

      

       A5: ( dom (E1 | ((SSS * ) /\ Tm))) = ( dom ((E1 | (SSS * )) | Tm)) by RELAT_1: 71

      .= (( dom (E1 | (SSS * ))) /\ Tm) by RELAT_1: 61

      .= ((Tm null TT) /\ (SSS * )) by A3, XBOOLE_1: 16

      .= ((SSS * ) /\ Tm);

      

       A6: ( dom (s | ((SSS * ) /\ Tm))) = ( dom ((s | (SSS * )) | Tm)) by RELAT_1: 71

      .= ((SSS * ) /\ Tm) by A3, RELAT_1: 61;

      assume phi0 is SSS -valued;

      then

      reconsider R = ( rng phi0) as non empty Subset of SSSS by RELAT_1:def 19;

      ( rng ( SubTerms phi0)) c= (R * ) & (R * ) c= (SSS * ) by RELAT_1:def 19;

      then

       A7: ( rng ( SubTerms phi0)) c= (SSS * ) & ( rng ( SubTerms phi0)) c= Tm by RELAT_1:def 19, A4;

      

       A8: (E1 * ( SubTerms phi0)) = ((E1 | ((SSS * ) /\ Tm)) * ( SubTerms phi0)) by A7, XBOOLE_1: 19, A5, RELAT_1: 165

      .= (((E2 * s) | ((SSS * ) /\ Tm)) * ( SubTerms phi0)) by Lm40

      .= ((E2 * (s | ((SSS * ) /\ Tm))) * ( SubTerms phi0)) by RELAT_1: 83

      .= (E2 * ((s | ((SSS * ) /\ Tm)) * ( SubTerms phi0))) by RELAT_1: 36

      .= (E2 * (s * ( SubTerms phi0))) by A7, XBOOLE_1: 19, A6, RELAT_1: 165

      .= (E2 * ( SubTerms psi0)) by Lm39;

      per cases ;

        suppose

         A9: r <> E;

        

        then (I1 -AtomicEval phi0) = ((I2 . r2) . (E2 * ( SubTerms psi0))) by FOMODEL2: 14, A8, A1, A2

        .= (I2 -AtomicEval psi0) by FOMODEL2: 14, A9, A1;

        hence thesis;

      end;

        suppose

         A10: r = E;

        

        then (I1 -AtomicEval phi0) = (d . (E1 * ( SubTerms phi0))) by FOMODEL2: 14

        .= (I2 -AtomicEval psi0) by A10, A1, FOMODEL2: 14, A8;

        hence thesis;

      end;

    end;

    theorem :: FOMODEL3:9

    

     Th9: ( not l2 in ( rng psi)) implies for I be Element of (U -InterpretersOf S) holds (((l1,u1) ReassignIn I) -TruthEval psi) = (((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi))

    proof

      set II = (U -InterpretersOf S), s = (l1 SubstWith l2), SS = ( AllSymbolsOf S), SSS = (SS \ {l2}), TT = ( AllTermsOf S), T = (S -termsOfMaxDepth ), F = (S -firstChar ), N = ( TheNorSymbOf S);

      reconsider SSSS = SSS as non empty Subset of SS;

      defpred P[ Nat] means for I be Element of II, u, phi st phi is $1 -wff & phi is SSS -valued holds (((l1,u) ReassignIn I) -TruthEval phi) = (((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi));

      

       A1: P[ 0 ]

      proof

        let I be Element of II;

        let u, phi;

        set I1 = ((l1,u) ReassignIn I), I2 = ((l2,u) ReassignIn I);

        assume phi is 0 -wff;

        then

        reconsider phi0 = phi as 0wff string of S;

        assume phi is SSS -valued;

        then (I1 -TruthEval phi0) = (I2 -TruthEval ((l1,l2) -SymbolSubstIn phi0)) by Lm41;

        hence thesis;

      end;

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A3: P[n];

        let I be Element of II;

        let u, phi;

        set I1 = ((l1,u) ReassignIn I), I2 = ((l2,u) ReassignIn I);

        assume

         A4: phi is (n + 1) -wff & phi is SSS -valued;

        then

        reconsider phii = phi as (n + 1) -wff string of S;

        reconsider x = phi as non emptySSSS -valued FinSequence by A4;

        ( {(x . 1)} \ SSS) = {} ;

        then (phii . 1) in SSS by ZFMISC_1: 60;

        then (F . phii) in SSS by FOMODEL0: 6;

        then not (F . phii) in {l2} by XBOOLE_0:def 5;

        then

         A5: (F . phii) <> l2 by TARSKI:def 1;

        reconsider psi = ((l1,l2) -SymbolSubstIn phii) as (n + 1) -wff string of S;

        reconsider phi1 = ( head phii) as n -wff string of S;

        reconsider psi1 = ((l1,l2) -SymbolSubstIn phi1) as n -wff string of S;

        per cases ;

          suppose phi is exal & not phi is 0wff;

          then

          reconsider phii as non 0wff exal(n + 1) -wff string of S;

          set l = (F . phii), phi2 = ( tail phii);

          

           A6: phii = (( <*l*> ^ phi1) ^ phi2) by FOMODEL2: 23

          .= ( <*l*> ^ phi1);

          

          then (s . phii) = ((s . <*l*>) ^ (s . phi1)) by FOMODEL0: 36

          .= ((s . <*l*>) ^ psi1) by FOMODEL0:def 22;

          then

           A7: psi = ((s . <*l*>) ^ psi1) by FOMODEL0:def 22;

          x = (( <*l*> ^ phi1) ^ {} ) by A6;

          then

           A8: phi1 is SSSS -valued by FOMODEL0: 44;

          (I1 -TruthEval phii) = 1 iff (I2 -TruthEval psi) = 1

          proof

            per cases ;

              suppose

               A9: l = l1;

              then

               A10: psi = ( <*l2*> ^ psi1) by A7, FOMODEL0: 35;

              hereby

                assume (I1 -TruthEval phii) = 1;

                then

                consider u1 such that

                 A11: (((l,u1) ReassignIn I1) -TruthEval phi1) = 1 by A6, FOMODEL2: 19;

                1 = (((l1,u1) ReassignIn I) -TruthEval phi1) by A11, A9, FOMODEL0: 43

                .= (((l2,u1) ReassignIn I) -TruthEval psi1) by A8, A3

                .= (((l2,u1) ReassignIn I2) -TruthEval psi1) by FOMODEL0: 43;

                hence (I2 -TruthEval psi) = 1 by A10, FOMODEL2: 19;

              end;

              assume (I2 -TruthEval psi) = 1;

              then

              consider u2 such that

               A12: (((l2,u2) ReassignIn I2) -TruthEval psi1) = 1 by A10, FOMODEL2: 19;

              1 = (((l2,u2) ReassignIn I) -TruthEval psi1) by A12, FOMODEL0: 43

              .= (((l1,u2) ReassignIn I) -TruthEval phi1) by A8, A3

              .= (((l,u2) ReassignIn I1) -TruthEval phi1) by A9, FOMODEL0: 43;

              hence (I1 -TruthEval phii) = 1 by A6, FOMODEL2: 19;

            end;

              suppose

               A13: l <> l1;

              then

               A14: psi = ( <*l*> ^ psi1) by A7, FOMODEL0: 35;

              hereby

                assume (I1 -TruthEval phii) = 1;

                then

                consider u1 such that

                 A15: (((l,u1) ReassignIn I1) -TruthEval phi1) = 1 by A6, FOMODEL2: 19;

                1 = (((l1,u) ReassignIn ((l,u1) ReassignIn I)) -TruthEval phi1) by A15, A13, FOMODEL0: 43

                .= (((l2,u) ReassignIn ((l,u1) ReassignIn I)) -TruthEval psi1) by A3, A8

                .= (((l,u1) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1) by A5, FOMODEL0: 43;

                hence (I2 -TruthEval psi) = 1 by A14, FOMODEL2: 19;

              end;

              assume (I2 -TruthEval psi) = 1;

              then

              consider u2 such that

               A16: (((l,u2) ReassignIn I2) -TruthEval psi1) = 1 by A14, FOMODEL2: 19;

              1 = (((l2,u) ReassignIn ((l,u2) ReassignIn I)) -TruthEval psi1) by A5, A16, FOMODEL0: 43

              .= (((l1,u) ReassignIn ((l,u2) ReassignIn I)) -TruthEval phi1) by A3, A8

              .= (((l,u2) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1) by A13, FOMODEL0: 43;

              hence (I1 -TruthEval phii) = 1 by A6, FOMODEL2: 19;

            end;

          end;

          then (I1 -TruthEval phii) = 1 iff not (I2 -TruthEval psi) = 0 by FOMODEL0: 39;

          hence thesis by FOMODEL0: 39;

        end;

          suppose not phi is exal & not phi is 0wff;

          then

          reconsider phii as (n + 1) -wff non exal non 0wff string of S;

          reconsider phi2 = ( tail phii) as n -wff string of S;

          reconsider psi2 = ((l1,l2) -SymbolSubstIn phi2) as n -wff string of S;

          ((F . phii) \+\ N) = {} ;

          then (F . phii) = N by FOMODEL0: 29;

          then

           A17: phii = (( <*N*> ^ phi1) ^ phi2) by FOMODEL2: 23;

          then phi1 is SSS -valued & phi2 is SSS -valued & ((I1 -TruthEval phii) = 1 iff ((I1 -TruthEval phi1) = 0 & (I1 -TruthEval phi2) = 0 )) by A4, FOMODEL0: 44, FOMODEL2: 19;

          then

           A18: ((I1 -TruthEval phii) = 1 iff ((I2 -TruthEval psi1) = 0 & (I2 -TruthEval psi2) = 0 )) by A3;

          

           A19: (s . phii) = psi & (s . phi1) = psi1 & (s . phi2) = psi2 by FOMODEL0:def 22;

          

          then psi = ((s . ( <*N*> ^ phi1)) ^ (s . phi2)) by A17, FOMODEL0: 36

          .= (((s . <*N*>) ^ (s . phi1)) ^ (s . phi2)) by FOMODEL0: 36

          .= (( <*N*> ^ psi1) ^ psi2) by FOMODEL0: 35, A19;

          then (I2 -TruthEval psi) = 1 iff not (I1 -TruthEval phi) = 0 by FOMODEL0: 39, FOMODEL2: 19, A18;

          hence thesis by FOMODEL0: 39;

        end;

          suppose phi is 0 -wff;

          hence thesis by A1, A4;

        end;

      end;

      

       A20: for m holds P[m] from NAT_1:sch 2( A1, A2);

      set m = ( Depth psi);

      assume not l2 in ( rng psi);

      then {l2} misses ( rng psi) & ( rng psi) c= SS by RELAT_1:def 19, ZFMISC_1: 50;

      then

       A21: psi is m -wff & psi is SSS -valued by XBOOLE_1: 86, FOMODEL2:def 31, RELAT_1:def 19;

      let I be Element of II;

      thus thesis by A20, A21;

    end;

    definition

      let S;

      let l, t, n;

      let f be FinSequence-yielding Function;

      let phi;

      :: FOMODEL3:def20

      func (l,t,n,f) Subst2 phi -> FinSequence equals

      : Def20: (( <*( TheNorSymbOf S)*> ^ (f . ( head phi))) ^ (f . ( tail phi))) if ( Depth phi) = (n + 1) & not phi is exal,

( <* the Element of (( LettersOf S) \ ((( rng t) \/ ( rng ( head phi))) \/ {l}))*> ^ (f . ((((S -firstChar ) . phi), the Element of (( LettersOf S) \ ((( rng t) \/ ( rng ( head phi))) \/ {l}))) -SymbolSubstIn ( head phi)))) if ( Depth phi) = (n + 1) & phi is exal & ((S -firstChar ) . phi) <> l

      otherwise (f . phi);

      coherence ;

      consistency ;

    end

    registration

      let S;

      cluster -> FinSequence-yielding for Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S)));

      coherence ;

    end

    

     Lm42: for f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S))) holds ((l,t,n,f) Subst2 phi) is wff string of S

    proof

      set FF = ( AllFormulasOf S), h = ( head phi), d = ( Depth phi), F = (S -firstChar );

      let f be Element of ( Funcs (FF,FF));

      reconsider ff = f as Function of FF, FF;

      set IT = ((l,t,n,f) Subst2 phi), N = ( TheNorSymbOf S), L = ( LettersOf S), X = (L \ ((( rng t) \/ ( rng h)) \/ {l})), ll1 = the Element of X;

      reconsider hh = h, phii = phi as Element of FF by FOMODEL2: 16;

      reconsider newhead = (ff . hh) as wff string of S by TARSKI:def 3;

      reconsider XX = X as non empty Subset of L;

      ll1 is Element of XX;

      then

      reconsider l1 = ll1 as literal Element of S;

      per cases ;

        suppose

         A1: d = (n + 1) & not phi is exal;

        then not phi is 0 -wff;

        then

        reconsider phiii = phi as non 0wff non exal wff string of S by A1;

        reconsider ttt = ( tail phiii) as wff string of S;

        reconsider tt = ttt as Element of FF by FOMODEL2: 16;

        reconsider newtail = (ff . tt) as wff string of S by TARSKI:def 3;

        IT = (( <*N*> ^ newhead) ^ newtail) by A1, Def20;

        hence thesis;

      end;

        suppose

         A2: d = (n + 1) & phi is exal & (F . phi) <> l;

        reconsider phiii = phi as non 0wff exal wff string of S by A2;

        reconsider l = (F . phiii) as literal Element of S;

        reconsider newhead = ((l,l1) -SymbolSubstIn h) as wff string of S;

        reconsider newheadd = newhead as Element of FF by FOMODEL2: 16;

        reconsider newesthead = (ff . newheadd) as wff string of S by TARSKI:def 3;

        IT = ( <*l1*> ^ newesthead) by A2, Def20;

        hence thesis;

      end;

        suppose d <> (n + 1);

        then IT = (ff . phii) by Def20;

        hence thesis by TARSKI:def 3;

      end;

        suppose (F . phi) = l;

        then (F . phi) = l & phi is exal;

        then IT = (ff . phii) by Def20;

        hence thesis by TARSKI:def 3;

      end;

    end;

    definition

      let S;

      let l, t, n;

      let f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S)));

      let phi;

      :: original: Subst2

      redefine

      func (l,t,n,f) Subst2 phi -> wff string of S ;

      coherence by Lm42;

    end

    registration

      let S;

      let l, t, n;

      let f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S)));

      let phi;

      cluster ((l,t,n,f) Subst2 phi) -> wff;

      coherence ;

    end

    definition

      let S;

      let l, t, nn;

      let f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S)));

      let phi;

      :: original: Subst2

      redefine

      func (l,t,nn,f) Subst2 phi -> Element of ( AllFormulasOf S) ;

      coherence

      proof

        ((l,t,nn,f) Subst2 phi) in ( AllFormulasOf S) by FOMODEL2: 16;

        hence thesis;

      end;

    end

    definition

      let S, l, t, n;

      let f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S)));

      set FF = ( AllFormulasOf S), D = ( Funcs (FF,FF));

      :: FOMODEL3:def21

      func (l,t,n,f) Subst3 -> Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S))) means

      : Def21: for phi holds (it . phi) = ((l,t,n,f) Subst2 phi);

      existence

      proof

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        deffunc F( Element of FF) = ((l,t,nn,f) Subst2 $1) qua Element of FF;

        consider g be Function of FF, FF such that

         A1: for x be Element of FF holds (g . x) = F(x) from FUNCT_2:sch 4;

        reconsider gg = g as Element of ( Funcs (FF,FF)) by FUNCT_2: 8;

        take gg;

        now

          let phi;

          reconsider phii = phi as Element of FF by FOMODEL2: 16;

          (g . phii) = F(phii) by A1;

          hence (gg . phi) = ((l,t,nn,f) Subst2 phi);

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of D;

        reconsider IT11 = IT1, IT22 = IT2 as Function of FF, FF;

        assume

         A2: for phi holds (IT1 . phi) = ((l,t,n,f) Subst2 phi);

        assume

         A3: for phi holds (IT2 . phi) = ((l,t,n,f) Subst2 phi);

        now

          let x be object;

          assume x in FF;

          then

          reconsider phi = x as wff string of S;

          (IT1 . phi) = ((l,t,n,f) Subst2 phi) by A2

          .= (IT2 . phi) by A3;

          hence (IT11 . x) = (IT22 . x);

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    definition

      let S, l, t;

      let f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S)));

      set FF = ( AllFormulasOf S), D = ( Funcs (FF,FF));

      deffunc F( Nat, Element of D) = ((l,t,$1,$2) Subst3 );

      :: FOMODEL3:def22

      func (l,t) Subst4 f -> sequence of ( Funcs (( AllFormulasOf S),( AllFormulasOf S))) means

      : Def22: (it . 0 ) = f & for m holds (it . (m + 1)) = ((l,t,m,(it . m)) Subst3 );

      existence

      proof

        consider g be sequence of D such that

         A1: (g . 0 ) = f & for m holds (g . (m + 1)) = F(m,) from NAT_1:sch 12;

        take g;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be sequence of D;

        assume that

         A2: (IT1 . 0 ) = f and

         A3: for m holds (IT1 . (m + 1)) = F(m,) and

         A4: (IT2 . 0 ) = f and

         A5: for m holds (IT2 . (m + 1)) = F(m,);

        IT1 = IT2 from NAT_1:sch 16( A2, A3, A4, A5);

        hence thesis;

      end;

    end

    definition

      let S, l, t;

      set AF = ( AtomicFormulasOf S), TT = ( AllTermsOf S);

      :: FOMODEL3:def23

      func l AtomicSubst t -> Function of ( AtomicFormulasOf S), ( AtomicFormulasOf S) means

      : Def23: for phi0, tt st tt = t holds (it . phi0) = ((l,tt) AtomicSubst phi0);

      existence

      proof

        reconsider tt = t as Element of TT by FOMODEL1:def 32;

        deffunc F( Element of AF) = ((l,tt) AtomicSubst $1);

        consider f such that

         A1: ( dom f) = AF & for x be Element of AF holds (f . x) = F(x) from FUNCT_1:sch 4;

        now

          let x be object;

          assume x in AF;

          then

          reconsider tt = x as Element of AF;

          (f . tt) = F(tt) by A1;

          then

          reconsider y = (f . x) as 0wff string of S;

          y in AF;

          hence (f . x) in AF;

        end;

        then

        reconsider ff = f as Function of AF, AF by A1, FUNCT_2: 3;

        take ff;

        hereby

          let phi0, tt1;

          phi0 in AF;

          then

          reconsider phi = phi0 as Element of AF;

          assume tt1 = t;

          then tt1 = tt & (f . phi) = ((l,tt) AtomicSubst phi) by A1;

          hence (ff . phi0) = ((l,tt1) AtomicSubst phi0);

        end;

      end;

      uniqueness

      proof

        reconsider tt = t as Element of TT by FOMODEL1:def 32;

        let IT1,IT2 be Function of AF, AF;

        assume that

         A2: for phi0, tt st tt = t holds (IT1 . phi0) = ((l,tt) AtomicSubst phi0) and

         A3: for phi0, tt st tt = t holds (IT2 . phi0) = ((l,tt) AtomicSubst phi0);

        now

          let x be Element of AF;

          consider w such that

           A4: x = w & w is 0wff;

          reconsider phi0 = w as 0wff string of S by A4;

          (IT1 . phi0) = ((l,tt) AtomicSubst phi0) by A2

          .= (IT2 . phi0) by A3;

          hence (IT1 . x) = (IT2 . x) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let S, l, t;

      :: FOMODEL3:def24

      func l Subst1 t -> Function equals (( id ( AllFormulasOf S)) +* (l AtomicSubst t));

      coherence ;

    end

    

     Lm43: (l Subst1 t) in ( Funcs (( AllFormulasOf S),( AllFormulasOf S)))

    proof

      set FF = ( AllFormulasOf S), g = (l AtomicSubst t), AF = ( AtomicFormulasOf S), E = the Element of FF, f = ( id FF), IT = (f +* g), SS = ( AllSymbolsOf S);

      reconsider FFF = FF as Subset of (SS * ) by XBOOLE_1: 1;

      (AF \ FF) = {} ;

      then

      reconsider AFF = AF as Subset of FF by XBOOLE_1: 37;

      ( dom f) = FF & ( dom g) = AFF by FUNCT_2:def 1;

      then

       A1: ( dom IT) = (FF null AFF) by FUNCT_4:def 1;

      reconsider gg = g as AFF -valued Function;

      reconsider ff = f as FF -valued Function;

      IT = IT & ( dom IT) = FF & ( rng IT) c= FF by RELAT_1:def 19, A1;

      hence thesis by FUNCT_2:def 2;

    end;

    definition

      let S, l, t;

      :: original: Subst1

      redefine

      func l Subst1 t -> Element of ( Funcs (( AllFormulasOf S),(( AllSymbolsOf S) * ))) ;

      coherence

      proof

        set FF = ( AllFormulasOf S), SS = ( AllSymbolsOf S), IT = (l Subst1 t);

        FF c= (SS * ) by XBOOLE_1: 1;

        then IT in ( Funcs (FF,FF)) & ( Funcs (FF,FF)) c= ( Funcs (FF,(SS * ))) by Lm43, FUNCT_5: 56;

        hence thesis;

      end;

    end

    definition

      let S, l, t;

      :: original: Subst1

      redefine

      func l Subst1 t -> Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S))) ;

      coherence by Lm43;

    end

    definition

      let S, l, t, phi;

      :: FOMODEL3:def25

      func (l,t) SubstIn phi -> wff string of S equals ((((l,t) Subst4 (l Subst1 t)) . ( Depth phi)) . phi);

      coherence

      proof

        set FF = ( AllFormulasOf S), D = ( Funcs (FF,FF));

        reconsider d = ( Depth phi) as Element of NAT by ORDINAL1:def 12;

        reconsider F = ((l,t) Subst4 (l Subst1 t)) as sequence of D;

        (F . d) is Element of D;

        then

        reconsider f = (F . d) as Function of FF, FF;

        reconsider phii = phi as Element of FF by FOMODEL2: 16;

        (f . phii) is wff string of S by TARSKI:def 3;

        hence thesis;

      end;

    end

    registration

      let S, l, t, phi;

      cluster ((l,t) SubstIn phi) -> wff;

      coherence ;

    end

    

     Lm44: for f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S))) holds ((((l,t) Subst4 f) . (m + 1)) . phi) = ((l,t,m,(((l,t) Subst4 f) . m)) Subst2 phi)

    proof

      set FF = ( AllFormulasOf S), D = ( Funcs (FF,FF));

      let f be Element of D;

      reconsider mm = m as Element of NAT by ORDINAL1:def 12;

      set f4 = ((l,t) Subst4 f), f3 = ((l,t,m,(f4 . mm)) Subst3 );

      ((f4 . (mm + 1)) . phi) = (f3 . phi) by Def22

      .= ((l,t,m,(f4 . mm)) Subst2 phi) by Def21;

      hence thesis;

    end;

    

     Lm45: for f be Element of ( Funcs (( AllFormulasOf S),( AllFormulasOf S))) holds ((((l,t) Subst4 f) . (( Depth phi) + m)) . phi) = ((((l,t) Subst4 f) . ( Depth phi)) . phi) & (((S -firstChar ) . phi) = l implies ((((l,t) Subst4 (l Subst1 t)) . ( Depth phi)) . phi) = phi)

    proof

      set TT = ( AllTermsOf S), FF = ( AllFormulasOf S), F = (S -firstChar );

      let f be Element of ( Funcs (FF,FF));

      reconsider tt = t as Element of TT by FOMODEL1:def 32;

      set f0 = (l Subst1 t), f4 = ((l,t) Subst4 f0), N = ( TheNorSymbOf S), L = ( LettersOf S), h = ( head phi), d = ( Depth phi), d1 = ( Depth h), AF = ( AtomicFormulasOf S), f5 = ((l,t) Subst4 f);

      defpred P[ Nat] means ((f5 . (( Depth phi) + $1)) . phi) = ((f5 . ( Depth phi)) . phi) & ((F . phi) = l implies ((f4 . $1) . phi) = phi);

      

       A1: P[ 0 ]

      proof

        thus ((f5 . (( Depth phi) + 0 )) . phi) = ((f5 . ( Depth phi)) . phi);

        assume

         A2: (F . phi) = l;

        then

        reconsider phii = phi as non 0wff wff string of S;

        reconsider phiii = phii as Element of FF by FOMODEL2: 16;

        ((F . phi) \+\ N) <> {} by A2, FOMODEL0: 29;

        then

        reconsider phii as exal non 0wff wff string of S;

        

         A3: ((( id FF) . phiii) \+\ phiii) = {} ;

         not phii in ( dom (l AtomicSubst t));

        

        then

         A4: (f0 . phii) = (( id FF) . phii) by FUNCT_4: 11

        .= phii by A3;

        reconsider tt = ( tail phii) as empty set;

        thus thesis by Def22, A4;

      end;

      

       A5: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A6: P[n];

        then d <> (d + (n + 1)) & P[n];

        then

         A7: d <> ((d + n) + 1) & P[n];

        

        thus ((f5 . (d + (n + 1))) . phi) = ((f5 . ((d + n) + 1)) . phi)

        .= ((l,t,(d + n),(f5 . (d + n))) Subst2 phi) by Lm44

        .= ((f5 . d) . phi) by A7, Def20;

        assume

         A8: (F . phi) = l;

        then ((F . phi) \+\ N) <> {} & not phi is 0 -wff by FOMODEL0: 29;

        then phi is non 0wff & not phi is non exal non 0wff;

        then

        reconsider phii = phi as non 0wff exal wff string of S;

        

        thus ((f4 . (n + 1)) . phi) = ((l,t,n,(f4 . n)) Subst2 phii) by Lm44

        .= phi by A6, A8, Def20;

      end;

      for n holds P[n] from NAT_1:sch 2( A1, A5);

      hence thesis;

    end;

    

     Lm46: phi is m -wff implies ((l,t) SubstIn phi) = ((((l,t) Subst4 (l Subst1 t)) . m) . phi)

    proof

      set d = ( Depth phi), FF = ( AllFormulasOf S);

      reconsider f = (l Subst1 t) as Element of ( Funcs (FF,FF));

      assume phi is m -wff;

      then

      reconsider k = (m - d) as Nat;

      ((((l,t) Subst4 f) . (d + k)) . phi) = ((l,t) SubstIn phi) by Lm45;

      hence thesis;

    end;

    registration

      let S, l, tt, phi0;

      identify (l,tt) AtomicSubst phi0 with (l,tt) SubstIn phi0;

      compatibility

      proof

        set LH = ((l,tt) SubstIn phi0), RH = ((l,tt) AtomicSubst phi0), f1 = (l Subst1 tt), f4 = ((l,tt) Subst4 f1), f0 = (l AtomicSubst tt), AF = ( AtomicFormulasOf S);

        phi0 in AF & ( dom f0) = AF by FUNCT_2:def 1;

        then

        reconsider phi00 = phi0 as Element of ( dom f0);

        

        thus LH = (f1 . phi00) by Def22

        .= (f0 . phi00) by FUNCT_4: 13

        .= RH by Def23;

      end;

      identify (l,tt) SubstIn phi0 with (l,tt) AtomicSubst phi0;

      compatibility ;

    end

    theorem :: FOMODEL3:10

    

     Th10: ( Depth ((l,tt) SubstIn psi)) = ( Depth psi) & for I be Element of (U -InterpretersOf S) holds (I -TruthEval ((l,tt) SubstIn psi)) = (((l,((I -TermEval ) . tt)) ReassignIn I) -TruthEval psi)

    proof

      set II = (U -InterpretersOf S), TT = ( AllTermsOf S), AF = ( AtomicFormulasOf S), F = (S -firstChar ), L = ( LettersOf S);

      set f0 = (l AtomicSubst tt), f1 = (l Subst1 tt), f4 = ((l,tt) Subst4 f1), FF = ( AllFormulasOf S), N = ( TheNorSymbOf S);

      defpred P[ Nat] means for phi st ( Depth phi) <= $1 holds (( Depth ((l,tt) SubstIn phi)) = ( Depth phi) & for I be Element of II holds (I -TruthEval ((l,tt) SubstIn phi)) = (((l,((I -TermEval ) . tt)) ReassignIn I) -TruthEval phi));

      (tt null {} ) is ( {} \/ ( rng tt)) -valued FinSequence;

      then tt is FinSequence of ( rng tt) by FOMODEL0: 26;

      then

      reconsider ttt = tt as Element of (( rng tt) * );

      

       A1: P[ 0 ]

      proof

        let phi;

        set d = ( Depth phi), IT = ((l,tt) SubstIn phi);

        assume

         A2: d <= 0 ;

        reconsider phii = phi as 0wff string of S by A2;

        ( Depth ((l,tt) SubstIn phii)) = 0 ;

        hence ( Depth IT) = d;

        let I be Element of II;

        set u = ((I -TermEval ) . tt), J = ((l,u) ReassignIn I);

        (I -TruthEval ((l,tt) AtomicSubst phii)) = (J -TruthEval phii) by Th8;

        hence thesis;

      end;

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        let phi;

        reconsider X = (L \ ((( rng tt) \/ ( rng ( head phi))) \/ {l})) as infinite Subset of L;

        reconsider XX = X as non empty Subset of L;

        set ll2 = the Element of X;

        reconsider l2 = ll2 as literal Element of S by TARSKI:def 3;

        assume

         C0: ( Depth phi) <= (n + 1);

         not l2 in ((( rng tt) \/ ( rng ( head phi))) \/ {l}) by XBOOLE_0:def 5;

        then not l2 in (( rng tt) \/ ( rng ( head phi))) & not l2 in {l} by XBOOLE_0:def 3;

        then

         A5: l2 <> l & not l2 in ( rng tt) & not l2 in ( rng ( head phi)) by XBOOLE_0:def 3, TARSKI:def 1;

        per cases ;

          suppose phi is exal;

          then

          reconsider phii = phi as non 0wff exal wff string of S;

          consider m such that

           A6: ( Depth phii) = (m + 1) by NAT_1: 6;

          reconsider mm = m as Element of NAT by ORDINAL1:def 12;

          

           D1: m <= n by XREAL_1: 8, C0, A6;

          reconsider phii as non 0wff exal(m + 1) -wff string of S by A6, FOMODEL2:def 31;

          set IT = ((l,tt) SubstIn phii), d = ( Depth phii);

          reconsider l1 = (F . phii) as literal Element of S;

          reconsider phi1 = ( head phii) as Element of FF by FOMODEL2: 16;

          set d1 = ( Depth phi1);

          reconsider phi2 = ( tail phii) as empty set;

          reconsider psi = ((l1,l2) -SymbolSubstIn phi) as (m + 1) -wff string of S;

          reconsider psi1 = ((l1,l2) -SymbolSubstIn ( head phii)) as m -wff string of S;

          (( Depth psi1) \+\ d1) = {} ;

          then

           A7: ( Depth psi1) = ( Depth phi1) by FOMODEL0: 29;

          reconsider Phi1 = ((l,tt) SubstIn psi1) as wff string of S;

          

           A8: phii = (( <*l1*> ^ phi1) ^ phi2) by FOMODEL2: 23

          .= ( <*l1*> ^ phi1);

          d1 <= m by FOMODEL2:def 31;

          then

           A9: d1 <= n by XXREAL_0: 2, D1;

          then

           A10: ( Depth Phi1) = ( Depth ( head phii)) by A4, A7;

          reconsider m1 = (m - d1) as Nat;

          reconsider new1 = ((l,tt) SubstIn phi1) as wff string of S;

          set d11 = ( Depth new1);

          

           A11: IT = ((l,tt,m,(f4 . mm)) Subst2 phii) by A6, Lm44;

          per cases ;

            suppose l1 <> l;

            

            then

             A12: IT = ( <*l2*> ^ ((f4 . mm) . ((l1,l2) -SymbolSubstIn phi1))) by A6, Def20, A11

            .= ( <*l2*> ^ ((l,tt) SubstIn psi1)) by Lm46;

            

            then ( Depth IT) = (( Depth phi1) + 1) by A10, FOMODEL2: 17

            .= ( Depth phi) by A8, FOMODEL2: 17;

            hence ( Depth ((l,tt) SubstIn phi)) = ( Depth phi);

            let I be Element of II;

            set tu = ((I -TermEval ) . tt), It = ((l,tu) ReassignIn I);

            (I -TruthEval IT) = 1 iff (((l,tu) ReassignIn I) -TruthEval phii) = 1

            proof

              hereby

                assume (I -TruthEval IT) = 1;

                then

                consider u such that

                 A13: (((l2,u) ReassignIn I) -TruthEval Phi1) = 1 by A12, FOMODEL2: 19;

                set I2 = ((l2,u) ReassignIn I);

                1 = (((l,((I2 -TermEval ) . tt)) ReassignIn I2) -TruthEval psi1) by A13, A7, A9, A4

                .= (((l,tu) ReassignIn I2) -TruthEval psi1) by A5, FOMODEL2: 25

                .= (((l2,u) ReassignIn ((l,tu) ReassignIn I)) -TruthEval psi1) by A5, FOMODEL0: 43

                .= (((l1,u) ReassignIn ((l,tu) ReassignIn I)) -TruthEval ( head phii)) by A5, Th9;

                hence 1 = (((l,tu) ReassignIn I) -TruthEval phii) by A8, FOMODEL2: 19;

              end;

              assume (((l,tu) ReassignIn I) -TruthEval phii) = 1;

              then

              consider u1 such that

               A14: (((l1,u1) ReassignIn ((l,tu) ReassignIn I)) -TruthEval ( head phii)) = 1 by A8, FOMODEL2: 19;

              1 = (((l2,u1) ReassignIn ((l,tu) ReassignIn I)) -TruthEval psi1) by A14, Th9, A5

              .= (((l,tu) ReassignIn ((l2,u1) ReassignIn I)) -TruthEval psi1) by FOMODEL0: 43, A5

              .= (((l,((((l2,u1) ReassignIn I) -TermEval ) . tt)) ReassignIn ((l2,u1) ReassignIn I)) -TruthEval psi1) by FOMODEL2: 25, A5

              .= (((l2,u1) ReassignIn I) -TruthEval Phi1) by A7, A9, A4;

              hence (I -TruthEval IT) = 1 by A12, FOMODEL2: 19;

            end;

            then (I -TruthEval IT) = 1 iff not (((l,tu) ReassignIn I) -TruthEval phii) = 0 by FOMODEL0: 39;

            hence thesis by FOMODEL0: 39;

          end;

            suppose

             A15: l1 = l;

            then

             A16: phi = IT by Lm45;

            thus ( Depth ((l,tt) SubstIn phi)) = ( Depth phi) by A15, Lm45;

            let I be Element of II;

            set tu = ((I -TermEval ) . tt), It = ((l,tu) ReassignIn I);

            (It -TruthEval phii) = 1 iff (I -TruthEval phii) = 1

            proof

              hereby

                assume (It -TruthEval phii) = 1;

                then

                consider u such that

                 A17: (((l1,u) ReassignIn It) -TruthEval phi1) = 1 by A8, FOMODEL2: 19;

                1 = (((l1,u) ReassignIn I) -TruthEval phi1) by A17, A15, FOMODEL0: 43;

                hence (I -TruthEval phii) = 1 by A8, FOMODEL2: 19;

              end;

              assume (I -TruthEval phii) = 1;

              then

              consider u1 such that

               A18: (((l1,u1) ReassignIn I) -TruthEval phi1) = 1 by A8, FOMODEL2: 19;

              (((l1,u1) ReassignIn It) -TruthEval phi1) = 1 by A15, A18, FOMODEL0: 43;

              hence (It -TruthEval phii) = 1 by A8, FOMODEL2: 19;

            end;

            then (It -TruthEval phi) = 1 iff not (I -TruthEval phi) = 0 by FOMODEL0: 39;

            hence thesis by A16, FOMODEL0: 39;

          end;

        end;

          suppose not phi is exal & not phi is 0wff;

          then

          reconsider phii = phi as non 0wff non exal wff string of S;

          set IT = ((l,tt) SubstIn phii), d = ( Depth phii);

          consider m such that

           A19: d = (m + 1) by NAT_1: 6;

          

           W1: ((m + 1) + ( - 1)) <= ((n + 1) - 1) by XREAL_1: 8, C0, A19;

          reconsider mm = m as Element of NAT by ORDINAL1:def 12;

          reconsider phii as non 0wff non exal(m + 1) -wff string of S by A19, FOMODEL2:def 31;

          reconsider phi1 = ( head phii), phi2 = ( tail phii) as Element of FF by FOMODEL2: 16;

          set d1 = ( Depth phi1), d2 = ( Depth phi2);

          ((F . phii) \+\ N) = {} & phii = (( <*(F . phii)*> ^ phi1) ^ phi2) by FOMODEL2: 23;

          then

           A20: phii = (( <*N*> ^ phi1) ^ phi2) by FOMODEL0: 29;

          

           D2: d1 <= m & d2 <= m by FOMODEL2:def 31;

          reconsider m1 = (m - d1), m2 = (m - d2) as Nat;

          reconsider new1 = ((l,tt) SubstIn phi1), new2 = ((l,tt) SubstIn phi2) as wff string of S;

          set d11 = ( Depth new1), d22 = ( Depth new2);

          

           A21: d1 <= n & d2 <= n by W1, D2, XXREAL_0: 2;

          

           A22: IT = ((l,tt,m,(f4 . mm)) Subst2 phii) by A19, Lm44

          .= (( <*N*> ^ ((f4 . (d1 + m1)) . phi1)) ^ ((f4 . (d2 + m2)) . phi2)) by Def20, A19

          .= (( <*N*> ^ new1) ^ ((f4 . (d2 + m2)) . phi2)) by Lm45

          .= (( <*N*> ^ new1) ^ new2) by Lm45;

          

          then ( Depth IT) = (1 + ( max (d11,d22))) by FOMODEL2: 17

          .= (1 + ( max (d1,d22))) by A21, A4

          .= (1 + ( max (d1,d2))) by A21, A4

          .= d by FOMODEL2: 17, A20;

          hence ( Depth ((l,tt) SubstIn phi)) = ( Depth phi);

          let I be Element of II;

          set TE = (I -TermEval ), u = (TE . tt), J = ((l,u) ReassignIn I), LH = (I -TruthEval IT), RH = (J -TruthEval phii);

          (I -TruthEval new1) = (J -TruthEval phi1) & (I -TruthEval new2) = (J -TruthEval phi2) by A21, A4;

          then (J -TruthEval phii) = 1 iff ((I -TruthEval new1) = 0 & (I -TruthEval new2) = 0 ) by A20, FOMODEL2: 19;

          then LH = 1 iff not RH = 0 by FOMODEL2: 19, A22, FOMODEL0: 39;

          hence thesis by FOMODEL0: 39;

        end;

          suppose phi is 0wff;

          hence thesis by A1;

        end;

      end;

      

       A23: for m holds P[m] from NAT_1:sch 2( A1, A3);

      set m = ( Depth psi);

      thus ( Depth ((l,tt) SubstIn psi)) = ( Depth psi) by A23;

      let I be Element of II;

      thus thesis by A23;

    end;

    registration

      let m, S, l, t;

      let phi be m -wff string of S;

      cluster ((l,t) SubstIn phi) -> m -wff;

      coherence

      proof

        set d = ( Depth phi), TT = ( AllTermsOf S);

        reconsider tt = t as Element of TT by FOMODEL1:def 32;

        set psi = ((l,tt) SubstIn phi);

        reconsider k = (m - d) as Nat;

        ( Depth psi) = d by Th10;

        then

        reconsider psii = psi as d -wff string of S by FOMODEL2:def 31;

        psii is (d + ( 0 * k)) -wff;

        then psii is (d + k) -wff;

        hence thesis;

      end;

    end

    

     Lm47: for I1 be Element of (U -InterpretersOf S1), I2 be Element of (U -InterpretersOf S2) st (I1 | X) = (I2 | X) & (the adicity of S1 | X) = (the adicity of S2 | X) holds ((I1 -TermEval ) | (X * )) c= ((I2 -TermEval ) | (X * ))

    proof

      set T1 = (S1 -termsOfMaxDepth ), O1 = ( OwnSymbolsOf S1), TT1 = ( AllTermsOf S1), SS1 = ( AllSymbolsOf S1), L1 = ( LettersOf S1), F1 = (S1 -firstChar ), C1 = (S1 -multiCat ), AT1 = ( AtomicTermsOf S1), II1 = (U -InterpretersOf S1), a1 = the adicity of S1, strings1 = ((SS1 * ) \ { {} });

      set T2 = (S2 -termsOfMaxDepth ), O2 = ( OwnSymbolsOf S2), TT2 = ( AllTermsOf S2), SS2 = ( AllSymbolsOf S2), L2 = ( LettersOf S2), F2 = (S2 -firstChar ), C2 = (S2 -multiCat ), AT2 = ( AtomicTermsOf S2), II2 = (U -InterpretersOf S2), a2 = the adicity of S2, strings2 = ((SS2 * ) \ { {} });

      let I1 be Element of II1, I2 be Element of II2;

      

       A1: ( dom I1) = O1 & ( dom I2) = O2 by PARTFUN1:def 2;

      set E1 = (I1 -TermEval ), E2 = (I2 -TermEval ), I11 = (I1 | X), I22 = (I2 | X);

      assume

       A2: I11 = I22;

      then

       A3: ( dom E1) = TT1 & ( dom E2) = TT2 & I11 = I22 by FUNCT_2:def 1;

      

       A4: (X /\ ( dom I1)) = ( dom I22) by RELAT_1: 61, A2

      .= (X /\ ( dom I2)) by RELAT_1: 61;

      defpred P[ Nat] means (E1 | ((X * ) /\ (T1 . $1))) c= (E2 | ((X * ) /\ (T2 . $1)));

      deffunc F( set) = the set of all <*x*> where x be Element of $1;

      

       A5: P[ 0 ]

      proof

        

         A6: (T2 . 0 ) c= TT2 & (T1 . 0 ) c= TT1 by FOMODEL1: 2;

        reconsider D1 = ((X * ) /\ (T1 . 0 )) as Subset of TT1 by A6, XBOOLE_1: 1;

        reconsider D2 = ((X * ) /\ (T2 . 0 )) as Subset of TT2 by A6, XBOOLE_1: 1;

        set f1 = (E1 | D1), f2 = (E2 | D2);

        

         A7: ( dom f1) = D1 & ( dom f2) = D2 by PARTFUN1:def 2;

        now

          let x;

          assume

           A8: x in ( dom f1);

          then

           A9: x in ((X * ) /\ AT1) by A7, FOMODEL1:def 30;

          then

           A10: x in (1 -tuples_on (X /\ L1)) by FOMODEL0: 2;

          then

          reconsider Y1 = (X /\ L1) as non empty set;

          Y1 <> {} ;

          then

          reconsider XX = X as non empty set;

          reconsider xx = x as Element of (X * ) by A8, A7;

          x in F(Y1) by FINSEQ_2: 96, A10;

          then

          consider y1 be Element of Y1 such that

           A11: x = <*y1*>;

          y1 in Y1;

          then

          reconsider l1 = y1 as literal Element of S1;

          l1 in X & l1 in O1 by XBOOLE_0:def 4, FOMODEL1:def 19;

          then l1 in (X /\ O2) by A4, A1, XBOOLE_0:def 4;

          then

          reconsider s2 = l1 as own Element of S2;

          reconsider s22 = s2, l11 = l1 as Element of XX by XBOOLE_0:def 4;

          (((I2 | XX) . s22) \+\ (I2 . s22)) = {} & (((I1 | XX) . l11) \+\ (I1 . l11)) = {} ;

          then (I22 . s2) = (I2 . s2) & (I11 . l1) = (I1 . l1) by FOMODEL0: 29;

          

          then ( 0 -tuples_on U) = ( dom (I2 . s2)) by A2, FUNCT_2:def 1

          .= ( |.( ar s2).| -tuples_on U) by FUNCT_2:def 1;

          then not s2 is relational & not s2 is operational;

          then

          reconsider l2 = s2 as literal Element of S2;

          x in AT1 by A9;

          then x in (T1 . 0 ) by FOMODEL1:def 30;

          then

          reconsider t1 = x as 0 -termal string of S1 by FOMODEL1:def 33;

          reconsider D11 = D1 as non empty Subset of TT1 by A8;

          reconsider x1 = t1 as Element of D11 by A8;

          

           A12: l11 in XX & l2 in L2 by FOMODEL1:def 14;

          then

          reconsider Y2 = (XX /\ L2) as non empty set by XBOOLE_0:def 4;

          reconsider ll2 = l2 as Element of Y2 by A12, XBOOLE_0:def 4;

           <*ll2*> in F(Y2);

          then <*ll2*> in (1 -tuples_on Y2) by FINSEQ_2: 96;

          then

           A13: x in ((X * ) /\ AT2) by FOMODEL0: 2, A11;

          reconsider D22 = D2 as non empty Subset of TT2 by FOMODEL1:def 30, A13;

          reconsider x2 = x as Element of D22 by A13, FOMODEL1:def 30;

          

           A14: (t1 . 1) = y1 by A11, FINSEQ_1: 40;

          then

          reconsider y11 = (t1 . 1) as Element of XX by XBOOLE_0:def 4;

          (((I1 | XX) . y11) \+\ (I1 . y11)) = {} & (((I2 | XX) . y11) \+\ (I2 . y11)) = {} & (((E2 | D22) . x2) \+\ (E2 . x2)) = {} ;

          then

           A15: (I11 . y11) = (I1 . y11) & (I22 . y11) = (I2 . y11) & (E2 . x2) = ((E2 | D22) . x2) by FOMODEL0: 29;

          (((E1 | D11) . x1) \+\ (E1 . x1)) = {} ;

          

          then (f1 . x) = (E1 . t1) by FOMODEL0: 29

          .= ((I1 . (F1 . t1)) . (E1 * ( SubTerms t1))) by FOMODEL2: 21

          .= ((I2 . l2) . {} ) by FOMODEL0: 6, A14, A2, A15

          .= ((I2 . ( <*l2*> . 1)) . {} ) by FINSEQ_1: 40

          .= ((I2 . (F2 . <*l2*>)) . (E2 * ( SubTerms <*l2*>))) by FOMODEL0: 6

          .= (f2 . x) by FOMODEL2: 21, A11, A15;

          hence x in ( dom f2) & (f2 . x) = (f1 . x) by A7, A13, FOMODEL1:def 30;

        end;

        hence thesis by FOMODEL0: 51;

      end;

      assume

       A16: (a1 | X) = (a2 | X);

      

       A17: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A18: P[n];

        reconsider nn = n, NN = (n + 1) as Element of NAT by ORDINAL1:def 12;

        

         A19: (T2 . NN) c= TT2 & (T1 . NN) c= TT1 & (T1 . nn) c= TT1 & (T2 . nn) c= TT2 by FOMODEL1: 2;

        reconsider D1 = ((X * ) /\ (T1 . NN)), d1 = ((X * ) /\ (T1 . nn)) as Subset of TT1 by A19, XBOOLE_1: 1;

        reconsider D2 = ((X * ) /\ (T2 . NN)), d2 = ((X * ) /\ (T2 . nn)) as Subset of TT2 by A19, XBOOLE_1: 1;

        set f1 = (E1 | D1), f2 = (E2 | D2);

        

         A20: ( dom f1) = D1 & ( dom f2) = D2 & ( dom (E1 | d1)) = d1 & ( dom (E2 | d2)) = d2 by PARTFUN1:def 2;

        then

         A21: d1 c= d2 by A18, GRFUNC_1: 2;

        reconsider d12 = d1 as Subset of d2 by A18, GRFUNC_1: 2, A20;

        reconsider d21 = d12 as Subset of TT2 by XBOOLE_1: 1;

        now

          let y;

          assume

           A22: y in ( dom f1);

          then

          reconsider D11 = D1 as non empty set;

          reconsider y1 = y as Element of D11 by A22;

          y1 in (T1 . NN) by XBOOLE_0:def 4;

          then

          reconsider t1 = y1 as (nn + 1) -termal string of S1 by FOMODEL1:def 33;

          reconsider o1 = (F1 . t1) as termal Element of S1;

          set m1 = |.( ar o1).|;

          

           A23: t1 in (X * ) & t1 is non empty by TARSKI:def 3;

          then

          reconsider XX = X as non empty set;

          

           A24: y1 in (XX * ) by TARSKI:def 3;

          ( {(t1 . 1)} \ XX) = {} by A24;

          then

           A25: (t1 . 1) in XX & o1 = (t1 . 1) by ZFMISC_1: 60, FOMODEL0: 6;

          then o1 in XX & o1 in O1 by FOMODEL1:def 19;

          then o1 in (XX /\ O2) by A4, A1, XBOOLE_0:def 4;

          then

          reconsider o2 = o1 as own Element of S2;

          reconsider o22 = o2 as ofAtomicFormula Element of S2;

          reconsider ox = o1 as Element of XX by A25;

          ((a1 . ox) \+\ ((a1 | XX) . ox)) = {} & ((a2 . ox) \+\ ((a2 | XX) . ox)) = {} ;

          then

           A26: (a1 . o1) = ((a1 | X) . o1) & (a2 . o2) = ((a2 | X) . o2) by FOMODEL0: 29;

          ( ar o1) = ( ar o22) by A26, A16;

          then not o22 is relational;

          then

          reconsider o2 as termal Element of S2;

          set m2 = |.( ar o2).|;

          

           A27: ((I1 . ox) \+\ ((I1 | XX) . ox)) = {} & ((I2 . ox) \+\ ((I2 | XX) . ox)) = {} ;

          

          then

           A28: (I1 . ox) = ((I1 | XX) . o1) by FOMODEL0: 29

          .= (I2 . ox) by A27, FOMODEL0: 29, A2;

          set st1 = ( SubTerms t1);

          reconsider B = ( rng t1) as non empty Subset of XX by A24, RELAT_1:def 19;

          ( rng st1) c= (( rng t1) * ) & (B * ) c= (XX * ) by RELAT_1:def 19;

          then

           A29: ( rng st1) c= (XX * ) by XBOOLE_1: 1;

          

           A30: ( rng st1) c= (T1 . n) by RELAT_1:def 19;

          then ( rng st1) c= d1 by A29, XBOOLE_1: 19;

          then

           A31: ( rng st1) c= ((SS1 * ) \ { {} }) & ( rng st1) c= d2 by XBOOLE_1: 1, A21;

          then

           A32: ( rng st1) c= ((SS1 * ) \ { {} }) & ( rng st1) c= ((SS2 * ) \ { {} }) by XBOOLE_1: 1;

          st1 is (T2 . nn) -valued by A31, XBOOLE_1: 1, RELAT_1:def 19;

          then st1 is m2 -element FinSequence of (T2 . nn) by FOMODEL0: 26, A16, A26;

          then

          reconsider st2 = st1 as m2 -element Element of ((T2 . nn) * );

          reconsider T2n = (T2 . nn) as non empty Subset of TT2 by FOMODEL1: 2;

          st2 in (T2n * );

          then

          reconsider st22 = st2 as m2 -element Element of (TT2 * );

          reconsider t2 = (o2 -compound st2) as (nn + 1) -termal string of S2;

          per cases ;

            suppose t1 is 0 -termal;

            then

            reconsider t11 = t1 as 0 -termal string of S1;

            

             A33: t11 in (X * ) & t11 in (T1 . 0 ) by FOMODEL1:def 33, TARSKI:def 3;

            then

             A34: t11 in ((XX * ) /\ (T1 . 0 )) by XBOOLE_0:def 4;

            

             A35: (T2 . 0 ) c= TT2 & (T1 . 0 ) c= TT1 by FOMODEL1: 2;

            reconsider A1 = ((X * ) /\ (T1 . 0 )) as Subset of TT1 by A35, XBOOLE_1: 1;

            reconsider A2 = ((X * ) /\ (T2 . 0 )) as Subset of TT2 by A35, XBOOLE_1: 1;

            set g1 = (E1 | A1), g2 = (E2 | A2);

            

             A36: ( dom g1) = A1 & ( dom g2) = A2 by PARTFUN1:def 2;

            then

             A37: A1 c= A2 by A5, GRFUNC_1: 2;

            then t11 in A2 & t11 in A1 by A34;

            then

            reconsider t2 = t11 as 0 -termal string of S2 by FOMODEL1:def 33;

            t2 is ( 0 + ( 0 * NN)) -termal;

            then t2 is ( 0 + NN) -termal;

            then

             A38: t2 in (XX * ) & t2 in (T2 . NN) by TARSKI:def 3;

            thus y in ( dom f2) by A20, XBOOLE_0:def 4, A38;

            reconsider D22 = D2 as non empty set by XBOOLE_0:def 4, A38;

            reconsider A11 = A1, A22 = A2 as non empty set by A36, A5, A33, XBOOLE_0:def 4;

            reconsider t111 = t11 as Element of A11 by A33, XBOOLE_0:def 4;

            reconsider t02 = t11 as Element of A22 by A37, A34;

            reconsider t20 = t2 as Element of D22 by A38, XBOOLE_0:def 4;

            (((E1 | D11) . y1) \+\ (E1 . y1)) = {} & (((E1 | ((X * ) /\ (T1 . 0 ))) . t111) \+\ (E1 . t111)) = {} & (((E2 | A2) . t02) \+\ (E2 . t02)) = {} & (((E2 | D22) . t20) \+\ (E2 . t20)) = {} ;

            then

             A39: (f1 . y) = (E1 . y) & ((E1 | ((X * ) /\ (T1 . 0 ))) . y) = (E1 . y) & ((E2 | ((X * ) /\ (T2 . 0 ))) . y) = (E2 . y) & (f2 . y) = (E2 . y) by FOMODEL0: 29;

            thus (f1 . y) = (f2 . y) by A39, A5, A36, GRFUNC_1: 2, A34;

          end;

            suppose not t1 is 0 -termal;

            then o1 is operational by FOMODEL1: 16;

            then

            consider n1 be Nat such that

             A40: m1 = (n1 + 1) by NAT_1: 6;

            reconsider nn1 = n1 as Element of NAT by ORDINAL1:def 12;

            reconsider st11 = st1 as (nn1 + 1) -element Element of (TT1 * ) by A40;

            

             A41: not st11 is ( {} * ) -valued;

            st11 is (SS2 * ) -valued by XBOOLE_1: 1, A32, RELAT_1:def 19;

            then (C2 . st11) <> {} by FOMODEL0: 52, A41;

            then

             A42: (C1 . st1) = (C2 . st1) by FOMODEL0: 52;

            

             A43: t1 = t2 by FOMODEL1:def 37, A42;

            then t1 in (X * ) & t1 in (T2 . NN) by FOMODEL1:def 33, TARSKI:def 3;

            hence y in ( dom f2) by A20, XBOOLE_0:def 4;

            

             A44: t2 in (T2 . NN) & t2 in (X * ) by FOMODEL1:def 37, A42, A23, FOMODEL1:def 33;

            reconsider D22 = D2 as non empty set by A44, XBOOLE_0:def 4;

            reconsider tt2 = t2 as Element of D22 by A44, XBOOLE_0:def 4;

            

             A45: (F2 . t2) = (t2 . 1) by FOMODEL0: 6

            .= o2 by FINSEQ_1: 41;

            then

             A46: st22 = ( SubTerms t2) by FOMODEL1:def 37;

            

             A47: (E1 | d1) = ((E2 | d2) | d1) by A18, GRFUNC_1: 34, A20

            .= (E2 | (d12 null d2)) by RELAT_1: 71;

            (((E1 | D11) . y1) \+\ (E1 . y1)) = {} & (((E2 | D22) . tt2) \+\ (E2 . tt2)) = {} ;

            then

             A48: ((E1 | D1) . y1) = (E1 . y1) & ((E2 | D2) . t2) = (E2 . t2) by FOMODEL0: 29;

            

            hence (f1 . y) = ((I1 . o1) . (E1 * st1)) by FOMODEL2: 21

            .= ((I1 . o1) . ((E1 | d1) * st1)) by RELAT_1: 165, A20, A30, A29, XBOOLE_1: 19

            .= ((I1 . o1) . (E2 * st1)) by RELAT_1: 165, A20, A30, A29, XBOOLE_1: 19, A47

            .= (f2 . y) by A43, A48, FOMODEL2: 21, A45, A46, A28;

          end;

        end;

        hence thesis by FOMODEL0: 51;

      end;

      

       A49: for n holds P[n] from NAT_1:sch 2( A5, A17);

      now

        set g1 = (E1 | (X * )), g2 = (E2 | (X * ));

        

         A50: ( dom g1) = ((X * ) /\ TT1) & ( dom g2) = ((X * ) /\ TT2) by RELAT_1: 61, A3;

        let x;

        assume

         A51: x in ( dom g1);

        then x in ((X * ) /\ TT1) by RELAT_1: 61, A3;

        then

        reconsider t1 = x as termal string of S1;

        set m1 = ( Depth t1);

        reconsider mm1 = m1 as Element of NAT by ORDINAL1:def 12;

        reconsider t11 = t1 as m1 -termal string of S1 by FOMODEL1:def 40;

        

         A52: t11 in (T1 . m1) & x in (X * ) by A51, FOMODEL1:def 33;

        then

         A53: x in ((X * ) /\ (T1 . m1)) & (T1 . mm1) c= TT1 & (T2 . mm1) c= TT2 by XBOOLE_0:def 4, FOMODEL1: 2;

        then

        reconsider D1 = ((X * ) /\ (T1 . m1)) as non empty Subset of TT1 by XBOOLE_1: 1;

        reconsider D2 = ((X * ) /\ (T2 . m1)) as Subset of TT2 by XBOOLE_1: 1, A53;

        reconsider t111 = t1 as Element of D1 by A52, XBOOLE_0:def 4;

        set f1 = (E1 | D1), f2 = (E2 | D2);

        

         A54: ( dom (E1 | D1)) = D1 & ( dom (E2 | D2)) = D2 by PARTFUN1:def 2;

        x in ( dom f1) & f1 c= f2 by A49, A53, PARTFUN1:def 2;

        then

         A55: x in ( dom f2) & (f1 . x) = (f2 . x) by FOMODEL0: 51;

        then

         A56: x in ((X * ) /\ TT2) & x in D2 by XBOOLE_0:def 4, A54;

        hence x in ( dom g2) by RELAT_1: 61, A3;

        

        thus (g1 . x) = (E1 . t111) by A51, FUNCT_1: 47

        .= (f1 . t111) by A54, FUNCT_1: 47

        .= (E2 . t111) by A55, FUNCT_1: 49

        .= (g2 . x) by A56, A50, FUNCT_1: 47;

      end;

      hence thesis by FOMODEL0: 51;

    end;

    theorem :: FOMODEL3:11

    

     Th11: for I1 be Element of (U -InterpretersOf S1), I2 be Element of (U -InterpretersOf S2) st (I1 | X) = (I2 | X) & (the adicity of S1 | X) = (the adicity of S2 | X) holds ((I1 -TermEval ) | (X * )) = ((I2 -TermEval ) | (X * )) by Lm47;

    

     Lm48: for phi1 be 0wff string of S1, I1 be Element of (U -InterpretersOf S1), I2 be Element of (U -InterpretersOf S2) st (I1 | (( rng phi1) /\ ( OwnSymbolsOf S1))) = (I2 | (( rng phi1) /\ ( OwnSymbolsOf S1))) & (the adicity of S1 | (( rng phi1) /\ ( OwnSymbolsOf S1))) = (the adicity of S2 | (( rng phi1) /\ ( OwnSymbolsOf S1))) & ( TheEqSymbOf S1) = ( TheEqSymbOf S2) holds ex phi2 be 0wff string of S2 st (phi2 = phi1 & (I2 -AtomicEval phi2) = (I1 -AtomicEval phi1))

    proof

      set II1 = (U -InterpretersOf S1), II2 = (U -InterpretersOf S2), a2 = the adicity of S2, F2 = (S2 -firstChar ), E1 = ( TheEqSymbOf S1), E2 = ( TheEqSymbOf S2), TT1 = ( AllTermsOf S1), TT2 = ( AllTermsOf S2), O1 = ( OwnSymbolsOf S1), O2 = ( OwnSymbolsOf S2), C2 = (S2 -multiCat ), F1 = (S1 -firstChar ), TS1 = ( TermSymbolsOf S1), TS2 = ( TermSymbolsOf S2), a1 = the adicity of S1, C1 = (S1 -multiCat ), AS1 = ( AtomicFormulaSymbolsOf S1), AS2 = ( AtomicFormulaSymbolsOf S2), d = (U -deltaInterpreter ), RR1 = ( RelSymbolsOf S1);

      reconsider TS1 = ( TermSymbolsOf S1) as non empty Subset of O1 by FOMODEL1: 1;

      reconsider TS2 = ( TermSymbolsOf S2) as non empty Subset of O2 by FOMODEL1: 1;

      let phi1 be 0wff string of S1;

      let I1 be Element of II1, I2 be Element of II2;

      set TE1 = (I1 -TermEval ), TE2 = (I2 -TermEval ), X = (( rng phi1) /\ O1);

      assume

       A1: (I1 | X) = (I2 | X) & (a1 | X) = (a2 | X) & E1 = E2;

      then

       A2: (TE1 | (X * )) = (TE2 | (X * )) by Th11;

      

      then

       A3: ( dom (TE1 | (X * ))) = ((X * ) /\ ( dom TE2)) by RELAT_1: 61

      .= ((X * ) /\ TT2) by FUNCT_2:def 1;

      

      then

       A4: ((X * ) /\ TT2) = ((X * ) /\ ( dom TE1)) by RELAT_1: 61

      .= ((X * ) /\ TT1) by FUNCT_2:def 1;

      reconsider r1 = (F1 . phi1) as relational Element of S1;

      set m = |.( ar r1).|;

      set Y1 = (X \/ {E1}), Y2 = (X \/ {E2});

      ( {((phi1 null {} ) . 1)} \ (( rng phi1) \/ {} )) = {} ;

      then (phi1 . 1) in ( rng phi1) by ZFMISC_1: 60;

      then

       A5: r1 in ( rng phi1) by FOMODEL0: 6;

      r1 in {E1} or not r1 in (RR1 \ O1) by FOMODEL1: 1;

      then

       A6: r1 in {E1} or not r1 in RR1 or r1 in O1 by XBOOLE_0:def 5;

      then r1 in {E1} or r1 in X by A5, FOMODEL1:def 17, XBOOLE_0:def 4;

      then

       A7: r1 in Y1 by XBOOLE_0:def 3;

      reconsider t1 = ( SubTerms phi1) as (m + 0 ) -element FinSequence of TT1 by FOMODEL0: 26;

      t1 is (TS1 * ) -valued;

      then t1 in (m -tuples_on (O1 * )) & t1 in (m -tuples_on (( rng phi1) * )) by FOMODEL0: 16;

      then t1 in ((m -tuples_on (( rng phi1) * )) /\ (m -tuples_on (O1 * ))) by XBOOLE_0:def 4;

      then t1 in (m -tuples_on ((( rng phi1) * ) /\ (O1 * ))) by FOMODEL0: 3;

      then t1 in (m -tuples_on (X * )) by FOMODEL0: 55;

      then

       A8: t1 is (X * ) -valued & ( rng t1) c= TT1 by FOMODEL0: 12, RELAT_1:def 19;

      then

       A9: ( rng t1) c= (X * ) & ( rng t1) c= TT1 by RELAT_1:def 19;

      then

       A10: ( rng t1) c= ((X * ) /\ TT1) by XBOOLE_1: 19;

      ( rng t1) c= ((X * ) /\ TT2) by XBOOLE_1: 19, A9, A4;

      then

      reconsider X2 = ((X * ) /\ TT2) as non empty Subset of TT2;

      reconsider X1 = ((X * ) /\ TT1) as non empty Subset of TT1 by A10;

      t1 is m -elementX2 -valued FinSequence by RELAT_1:def 19, A9, A4, XBOOLE_1: 19;

      then

      reconsider t2 = t1 as m -element FinSequence of X2 by FOMODEL0: 26;

      t2 is Element of (X2 * );

      then

      reconsider tt2 = t2 as m -element Element of (TT2 * );

      reconsider E11 = E1 as Element of AS1 by FOMODEL1:def 20;

      reconsider EE1 = {E11} as non empty Subset of AS1;

      reconsider E22 = E2 as Element of AS2 by FOMODEL1:def 20;

      reconsider EE2 = {E22} as non empty Subset of AS2;

      set Y1 = (X \/ EE1), Y2 = (X \/ EE2), f1 = (a1 | EE1), f2 = (a2 | EE2);

      

       A11: ( dom f1) = EE1 & ( dom f2) = EE2 by PARTFUN1:def 2;

      now

        let x be object;

        assume

         A12: x in ( dom f1);

        then x = E1 & (f1 . x) = (a1 . x) by FUNCT_1: 47, TARSKI:def 1;

        then (f1 . x) = ( - 2) & (a2 . x) = ( - 2) by FOMODEL1:def 23, A1;

        hence (f1 . x) = (f2 . x) by A11, A1, A12, FUNCT_1: 47;

      end;

      then f1 = f2 by FUNCT_1: 2, A11, A1;

      then ((a2 | X) +* f2) = (a1 | Y1) by A1, FUNCT_4: 78;

      then

       A13: Y1 = Y2 & (a1 | Y1) = (a2 | Y2) by FUNCT_4: 78, A1;

      

       A14: ( ar r1) = ((a1 | Y1) . r1) by FUNCT_1: 49, A7

      .= (a2 . r1) by A7, A13, FUNCT_1: 49;

      then r1 in ( dom a2) by FUNCT_1:def 2;

      then r1 in AS2;

      then

      reconsider r2 = r1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;

      

       A15: ( ar r1) = ( ar r2) by A14;

      then

      reconsider r2 as relational Element of S2;

      reconsider phi2 = (r2 -compound tt2) as 0wff string of S2 by A15;

      take phi2;

      

      thus phi1 = ( <*r1*> ^ (C1 . t1)) by FOMODEL1:def 38

      .= phi2 by FOMODEL0: 52;

      

       A16: (F2 . phi2) = (phi2 . 1) by FOMODEL0: 6

      .= r2 by FINSEQ_1: 41;

      then

      reconsider tt22 = tt2 as |.( ar (F2 . phi2)).| -element Element of (TT2 * ) by A14;

      

       A17: tt22 = ( SubTerms phi2) by FOMODEL1:def 38, A16;

      

       A18: (TE1 * t1) = ((TE1 | (X * )) * t1) by RELAT_1: 165, XBOOLE_1: 19, A9, A4, A3

      .= (TE2 * ( SubTerms phi2)) by A17, A2, A8, RELAT_1:def 19, A3, RELAT_1: 165;

      per cases ;

        suppose

         A19: r1 <> E1;

        then

         A20: r1 in X by A6, A5, FOMODEL1:def 17, XBOOLE_0:def 4, TARSKI:def 1;

        

        then (I1 . r1) = ((I1 | X) . r1) by FUNCT_1: 49

        .= (I2 . r2) by FUNCT_1: 49, A1, A20;

        then ((I1 -AtomicEval phi1) = ((I1 . r1) . (TE1 * t1)) & (I2 -AtomicEval phi2) = ((I1 . r1) . (TE2 * ( SubTerms phi2)))) by A1, A19, A16, FOMODEL2: 14;

        hence (I1 -AtomicEval phi1) = (I2 -AtomicEval phi2) by A18;

      end;

        suppose r1 = E1;

        then ((I1 -AtomicEval phi1) = (d . (TE1 * t1)) & (I2 -AtomicEval phi2) = (d . (TE2 * ( SubTerms phi2)))) by A1, A16, FOMODEL2: 14;

        hence (I1 -AtomicEval phi1) = (I2 -AtomicEval phi2) by A18;

      end;

    end;

    theorem :: FOMODEL3:12

    

     Th12: ( TheNorSymbOf S1) = ( TheNorSymbOf S2) & ( TheEqSymbOf S1) = ( TheEqSymbOf S2) & (the adicity of S1 | ( OwnSymbolsOf S1)) = (the adicity of S2 | ( OwnSymbolsOf S1)) implies for I1 be Element of (U -InterpretersOf S1), I2 be Element of (U -InterpretersOf S2), phi1 be wff string of S1 st (I1 | ( OwnSymbolsOf S1)) = (I2 | ( OwnSymbolsOf S1)) holds ex phi2 be wff string of S2 st (phi2 = phi1 & (I2 -TruthEval phi2) = (I1 -TruthEval phi1))

    proof

      set II1 = (U -InterpretersOf S1), II2 = (U -InterpretersOf S2), N1 = ( TheNorSymbOf S1), N2 = ( TheNorSymbOf S2), F1 = (S1 -firstChar ), F2 = (S2 -firstChar ), a1 = the adicity of S1, a2 = the adicity of S2, O1 = ( OwnSymbolsOf S1), O2 = ( OwnSymbolsOf S2), d = (U -deltaInterpreter ), E1 = ( TheEqSymbOf S1), E2 = ( TheEqSymbOf S2), AS1 = ( AtomicFormulaSymbolsOf S1), AS2 = ( AtomicFormulaSymbolsOf S2);

      assume

       A1: N1 = N2;

      assume

       A2: E1 = E2 & (a1 | O1) = (a2 | O1);

      defpred P[ Nat] means for I1 be Element of II1, I2 be Element of II2, phi1 be $1 -wff string of S1 st (I1 | O1) = (I2 | O1) holds ex phi2 be $1 -wff string of S2 st (phi1 = phi2 & (I1 -TruthEval phi1) = (I2 -TruthEval phi2));

      

       A3: P[ 0 ]

      proof

        let I1 be Element of II1, I2 be Element of II2, phi1 be 0 -wff string of S1;

        set TE1 = (I1 -TermEval ), TE2 = (I2 -TermEval ), X = ( rng phi1);

        reconsider XX = (X /\ O1) as Subset of O1;

        reconsider r1 = (F1 . phi1) as relational Element of S1;

        

         A4: (a1 | XX) = ((a1 | O1) | X) by RELAT_1: 71

        .= (a2 | XX) by A2, RELAT_1: 71;

        assume (I1 | O1) = (I2 | O1);

        then ((I2 | O1) | X) = (I1 | XX) by RELAT_1: 71;

        then (I1 | XX) = (I2 | XX) by RELAT_1: 71;

        then

        consider phi2 be 0wff string of S2 such that

         A5: phi2 = phi1 & (I2 -AtomicEval phi2) = (I1 -AtomicEval phi1) by A4, Lm48, A2;

        reconsider phi2 as 0 -wff string of S2;

        take phi2;

        set st1 = ( SubTerms phi1), st2 = ( SubTerms phi2);

        reconsider r2 = (F2 . phi2) as relational Element of S2;

        thus thesis by A5;

      end;

      

       A6: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A7: P[n];

        let I1 be Element of II1, I2 be Element of II2, phi1 be (n + 1) -wff string of S1;

        set X = ( rng phi1);

        assume

         A8: (I1 | O1) = (I2 | O1);

        reconsider h1 = ( head phi1) as n -wff string of S1;

        set t = ( tail phi1), s1 = (F1 . phi1);

        consider h2 be n -wff string of S2 such that

         A9: h1 = h2 & (I1 -TruthEval h1) = (I2 -TruthEval h2) by A7, A8;

        per cases ;

          suppose phi1 is exal;

          then

          reconsider phi11 = phi1 as exal(n + 1) -wff string of S1;

          reconsider l1 = (F1 . phi11) as literal Element of S1;

          

           A10: (I1 . l1) = (I2 . l1) by A8, FOMODEL1:def 19, FUNCT_1: 49;

          l1 in ( dom I2) by A10, FUNCT_1:def 2;

          then l1 in O2;

          then

          reconsider l2 = l1 as own Element of S2;

          ( |.( ar l2).| -tuples_on U) = ( dom (I2 . l2)) by PARTFUN1:def 2

          .= ( 0 -tuples_on U) by A10, FUNCT_2:def 1;

          then not l2 is relational & not l2 is operational;

          then

          reconsider l2 as literal Element of S2;

          reconsider phi2 = ( <*l2*> ^ h2) as (n + 1) -wff exal string of S2;

          take phi2;

          

           A11: phi1 = (( <*l1*> ^ h1) ^ ( tail phi11)) by FOMODEL2: 23

          .= ( <*l1*> ^ h1);

          hence phi1 = phi2 by A9;

          (I1 -TruthEval phi11) = 1 iff (I2 -TruthEval phi2) = 1

          proof

            hereby

              assume (I1 -TruthEval phi11) = 1;

              then

              consider u such that

               A12: (((l1,u) ReassignIn I1) -TruthEval h1) = 1 by FOMODEL2: 19, A11;

              reconsider I11 = ((l1,u) ReassignIn I1) as Element of II1;

              reconsider I22 = ((l2,u) ReassignIn I2) as Element of II2;

              (I11 | O1) = ((I1 | O1) +* ((l1 .--> ( {} .--> u)) | O1)) by FUNCT_4: 71

              .= (I22 | O1) by A8, FUNCT_4: 71;

              then

              consider h22 be n -wff string of S2 such that

               A13: h22 = h1 & (I11 -TruthEval h1) = (I22 -TruthEval h22) by A7;

              thus (I2 -TruthEval phi2) = 1 by FOMODEL2: 19, A13, A9, A12;

            end;

            assume (I2 -TruthEval phi2) = 1;

            then

            consider u2 such that

             A14: (((l2,u2) ReassignIn I2) -TruthEval h2) = 1 by FOMODEL2: 19;

            reconsider I11 = ((l1,u2) ReassignIn I1) as Element of II1;

            reconsider I22 = ((l2,u2) ReassignIn I2) as Element of II2;

            (I11 | O1) = ((I1 | O1) +* ((l1 .--> ( {} .--> u2)) | O1)) by FUNCT_4: 71

            .= (I22 | O1) by A8, FUNCT_4: 71;

            then

            consider h222 be n -wff string of S2 such that

             A15: h222 = h1 & (I11 -TruthEval h1) = (I22 -TruthEval h222) by A7;

            thus (I1 -TruthEval phi11) = 1 by FOMODEL2: 19, A11, A14, A15, A9;

          end;

          then (I1 -TruthEval phi1) = 1 iff not (I2 -TruthEval phi2) = 0 by FOMODEL0: 39;

          hence (I1 -TruthEval phi1) = (I2 -TruthEval phi2) by FOMODEL0: 39;

        end;

          suppose not phi1 is 0wff & not phi1 is exal;

          then

          reconsider phi11 = phi1 as non 0wff non exal(n + 1) -wff string of S1;

          reconsider t1 = ( tail phi11) as n -wff string of S1;

          consider t2 be n -wff string of S2 such that

           A16: t1 = t2 & (I1 -TruthEval t1) = (I2 -TruthEval t2) by A7, A8;

          reconsider phi2 = (( <*N2*> ^ h2) ^ t2) as (n + 1) -wff non exal non 0wff string of S2;

          take phi2;

          ((F1 . phi11) \+\ N1) = {} & ((F2 . phi2) \+\ N2) = {} ;

          then

           A17: (F1 . phi1) = N1 & (F2 . phi2) = N2 & phi11 = (( <*(F1 . phi11)*> ^ h1) ^ t1) & h2 = ( head phi2) & t2 = ( tail phi2) by FOMODEL2: 23, FOMODEL0: 29;

          hence phi1 = phi2 by A16, A9, A1;

          set b1 = (I1 -TruthEval h1), c1 = (I1 -TruthEval t1), b2 = (I2 -TruthEval h2), c2 = (I2 -TruthEval t2), A1 = (I1 -TruthEval phi11), A2 = (I2 -TruthEval phi2);

          (A1 \+\ ((I1 -TruthEval ( head phi11)) 'nor' (I1 -TruthEval ( tail phi11)))) = {} & (A2 \+\ ((I2 -TruthEval ( head phi2)) 'nor' (I2 -TruthEval ( tail phi2)))) = {} ;

          then A1 = (b1 'nor' c1) & A2 = (b2 'nor' c2) by A17, FOMODEL0: 29;

          hence thesis by A9, A16;

        end;

          suppose phi1 is 0wff;

          then

          consider phi2 be 0 -wff string of S2 such that

           A18: phi1 = phi2 & (I1 -TruthEval phi1) = (I2 -TruthEval phi2) by A3, A8;

          phi2 is ( 0 + ( 0 * (n + 1))) -wff;

          then phi2 is ( 0 + (n + 1)) -wff;

          then

          reconsider phi22 = phi2 as (n + 1) -wff string of S2;

          take phi22;

          thus thesis by A18;

        end;

      end;

      

       A19: for n holds P[n] from NAT_1:sch 2( A3, A6);

      let I1 be Element of II1, I2 be Element of II2, phi1 be wff string of S1;

      set d = ( Depth phi1);

      reconsider phi11 = (phi1 null 0 ) as (d + 0 ) -wff string of S1;

      assume (I1 | O1) = (I2 | O1);

      then ex phi2 be d -wff string of S2 st (phi2 = phi11 & (I2 -TruthEval phi2) = (I1 -TruthEval phi11)) by A19;

      hence thesis;

    end;

    

     Lm49: for I1 be Element of (U -InterpretersOf S1), I2 be Element of (U -InterpretersOf S2) st S2 is S1 -extending & X c= ( AllFormulasOf S1) & (I1 | ( OwnSymbolsOf S1)) = (I2 | ( OwnSymbolsOf S1)) holds (X is I1 -satisfied iff X is I2 -satisfied)

    proof

      set II1 = (U -InterpretersOf S1), II2 = (U -InterpretersOf S2), a1 = the adicity of S1, a2 = the adicity of S2, O1 = ( OwnSymbolsOf S1), E1 = ( TheEqSymbOf S1), E2 = ( TheEqSymbOf S2), N1 = ( TheNorSymbOf S1), N2 = ( TheNorSymbOf S2), FF1 = ( AllFormulasOf S1), AS1 = ( AtomicFormulaSymbolsOf S1);

      ( dom a1) = AS1 & O1 c= AS1 by FUNCT_2:def 1, FOMODEL1: 1;

      then

      reconsider O11 = O1 as Subset of ( dom a1);

      let I1 be Element of II1, I2 be Element of II2;

      assume

       A1: S2 is S1 -extending;

      

      then (a1 | O1) = ((a2 | ( dom a1)) | O1) by GRFUNC_1: 34

      .= (a2 | (O11 null ( dom a1))) by RELAT_1: 71;

      then

       A2: (a1 | O1) = (a2 | O1) & N1 = N2 & E1 = E2 by A1;

      assume

       A3: X c= FF1 & (I1 | O1) = (I2 | O1);

      hereby

        assume

         A4: X is I1 -satisfied;

        now

          let phi2 be wff string of S2;

          assume

           A5: phi2 in X;

          then phi2 in FF1 by A3;

          then

          reconsider phi1 = phi2 as wff string of S1;

          consider phi22 be wff string of S2 such that

           A6: phi1 = phi22 & (I1 -TruthEval phi1) = (I2 -TruthEval phi22) by Th12, A2, A3;

          thus (I2 -TruthEval phi2) = 1 by A6, A5, A4;

        end;

        hence X is I2 -satisfied;

      end;

      assume

       A7: X is I2 -satisfied;

      now

        let phi1 be wff string of S1;

        assume

         A8: phi1 in X;

        consider phi2 be wff string of S2 such that

         A9: phi1 = phi2 & (I1 -TruthEval phi1) = (I2 -TruthEval phi2) by Th12, A2, A3;

        thus (I1 -TruthEval phi1) = 1 by A9, A8, A7;

      end;

      hence thesis;

    end;

    theorem :: FOMODEL3:13

    

     Th13: for I1,I2 be Element of (U -InterpretersOf S) st (I1 | (( rng phi) /\ ( OwnSymbolsOf S))) = (I2 | (( rng phi) /\ ( OwnSymbolsOf S))) holds (I1 -TruthEval phi) = (I2 -TruthEval phi)

    proof

      set O = ( OwnSymbolsOf S), II = (U -InterpretersOf S), a = the adicity of S, E = ( TheEqSymbOf S), F = (S -firstChar ), C = (S -multiCat );

      defpred P[ Nat] means for I1,I2 be Element of II, phi be $1 -wff string of S st (I1 | (( rng phi) /\ O)) = (I2 | (( rng phi) /\ O)) holds (I1 -TruthEval phi) = (I2 -TruthEval phi);

      

       A1: P[ 0 ]

      proof

        let I1,I2 be Element of II;

        let phi be 0 -wff string of S;

        reconsider phi1 = phi as 0wff string of S;

        assume (I1 | (( rng phi) /\ O)) = (I2 | (( rng phi) /\ O));

        then (I1 | (( rng phi1) /\ O)) = (I2 | (( rng phi1) /\ O)) & (a | (( rng phi1) /\ O)) = (a | (( rng phi1) /\ O)) & E = E;

        then

        consider phi2 be 0wff string of S such that

         A2: phi2 = phi1 & (I2 -AtomicEval phi2) = (I1 -AtomicEval phi1) by Lm48;

        thus thesis by A2;

      end;

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        let I1,I2 be Element of II;

        let phi be (n + 1) -wff string of S;

        assume

         A5: (I1 | (( rng phi) /\ O)) = (I2 | (( rng phi) /\ O));

        per cases ;

          suppose not phi is 0wff & not phi is exal;

          then

          reconsider phii = phi as non 0wff non exal(n + 1) -wff string of S;

          set X = (( rng phii) /\ O), s = (F . phii);

          reconsider h = ( head phii), t = ( tail phii) as n -wff string of S;

          phii = (( <*s*> ^ h) ^ t) by FOMODEL2: 23

          .= ( <*s*> ^ (h ^ t)) by FINSEQ_1: 32;

          then ( rng (h ^ t)) c= ( rng phii) & ( rng t) c= ( rng (h ^ t)) & ( rng h) c= ( rng (h ^ t)) by FINSEQ_1: 29, FINSEQ_1: 30;

          then ( rng h) c= ( rng phii) & ( rng t) c= ( rng phii) by XBOOLE_1: 1;

          then

          reconsider rh = (( rng h) /\ O), rt = (( rng t) /\ O) as Subset of X by XBOOLE_1: 26;

          set v1 = (I1 -TruthEval phii), v2 = (I2 -TruthEval phii), h1 = (I1 -TruthEval h), h2 = (I2 -TruthEval h), t1 = (I1 -TruthEval t), t2 = (I2 -TruthEval t);

          

           A6: (I1 | rh) = (I1 | (rh null X))

          .= ((I1 | X) | rh) by RELAT_1: 71

          .= (I2 | (rh null X)) by A5, RELAT_1: 71;

          (I1 | rt) = (I1 | (rt null X))

          .= ((I1 | X) | rt) by RELAT_1: 71

          .= (I2 | (rt null X)) by A5, RELAT_1: 71;

          then

           A7: t1 = t2 by A4;

          (v1 \+\ (h1 'nor' t1)) = {} & (v2 \+\ (h2 'nor' t2)) = {} ;

          then v1 = (h1 'nor' t1) & v2 = (h2 'nor' t2) by FOMODEL0: 29;

          hence thesis by A4, A6, A7;

        end;

          suppose phi is exal & not phi is 0wff;

          then

          reconsider phii = phi as exal wff string of S;

          set l = (F . phii);

          reconsider h = ( head phii) as n -wff string of S;

          

           A8: phii = (( <*l*> ^ h) ^ ( tail phii)) by FOMODEL2: 23

          .= ( <*l*> ^ h);

          then

          reconsider rh = ( rng h) as Subset of ( rng phii) by FINSEQ_1: 30;

          now

            hereby

              assume (I1 -TruthEval phii) = 1;

              then

              consider u such that

               A9: (((l,u) ReassignIn I1) -TruthEval h) = 1 by A8, FOMODEL2: 19;

              set f = (l .--> ( {} .--> u));

              reconsider I1u = ((l,u) ReassignIn I1), I2u = ((l,u) ReassignIn I2) as Element of II;

              (I1u | (( rng h) /\ O)) = ((I1 | ((rh null ( rng phii)) /\ O)) +* (f | (rh /\ O))) by FUNCT_4: 71

              .= ((I1 | (rh /\ (( rng phii) /\ O))) +* (f | (rh /\ O))) by XBOOLE_1: 16

              .= (((I1 | (( rng phii) /\ O)) | rh) +* (f | (rh /\ O))) by RELAT_1: 71

              .= ((I2 | ((( rng phii) /\ O) /\ rh)) +* (f | (rh /\ O))) by RELAT_1: 71, A5

              .= ((I2 | ((( rng phii) /\ rh) /\ O)) +* (f | (rh /\ O))) by XBOOLE_1: 16

              .= (I2u | (( rng h) /\ O)) by FUNCT_4: 71;

              then (I2u -TruthEval h) = 1 by A9, A4;

              hence (I2 -TruthEval phii) = 1 by A8, FOMODEL2: 19;

            end;

            assume (I2 -TruthEval phii) = 1;

            then

            consider u such that

             A10: (((l,u) ReassignIn I2) -TruthEval h) = 1 by A8, FOMODEL2: 19;

            set f = (l .--> ( {} .--> u));

            reconsider I1u = ((l,u) ReassignIn I1), I2u = ((l,u) ReassignIn I2) as Element of II;

            (I1u | (( rng h) /\ O)) = ((I1 | ((rh null ( rng phii)) /\ O)) +* (f | (rh /\ O))) by FUNCT_4: 71

            .= ((I1 | (rh /\ (( rng phii) /\ O))) +* (f | (rh /\ O))) by XBOOLE_1: 16

            .= (((I1 | (( rng phii) /\ O)) | rh) +* (f | (rh /\ O))) by RELAT_1: 71

            .= ((I2 | ((( rng phii) /\ O) /\ rh)) +* (f | (rh /\ O))) by RELAT_1: 71, A5

            .= ((I2 | ((( rng phii) /\ rh) /\ O)) +* (f | (rh /\ O))) by XBOOLE_1: 16

            .= (I2u | (( rng h) /\ O)) by FUNCT_4: 71;

            then (I1u -TruthEval h) = 1 by A10, A4;

            hence (I1 -TruthEval phii) = 1 by A8, FOMODEL2: 19;

          end;

          then (I1 -TruthEval phii) = 1 iff not (I2 -TruthEval phii) = 0 by FOMODEL0: 39;

          hence thesis by FOMODEL0: 39;

        end;

          suppose phi is 0wff;

          hence thesis by A1, A5;

        end;

      end;

      

       A11: for n holds P[n] from NAT_1:sch 2( A1, A3);

      let I1,I2 be Element of II;

      set d = ( Depth phi);

      (phi null 0 ) is (d + 0 ) -wff;

      then

      reconsider phii = phi as d -wff string of S;

      assume (I1 | (( rng phi) /\ O)) = (I2 | (( rng phi) /\ O));

      then (I1 | (( rng phii) /\ O)) = (I2 | (( rng phii) /\ O));

      hence thesis by A11;

    end;

    theorem :: FOMODEL3:14

    for I be Element of (U -InterpretersOf S) st l is X -absent & X is I -satisfied holds X is ((l,u) ReassignIn I) -satisfied

    proof

      set II = (U -InterpretersOf S);

      let I be Element of II;

      set O = ( OwnSymbolsOf S), I2 = ((l,u) ReassignIn I), f2 = (l .--> ( {} .--> u));

      assume

       A1: l is X -absent & X is I -satisfied;

      now

        let phi;

        reconsider no = (( rng phi) /\ O) as Subset of ( rng phi);

        assume

         A2: phi in X;

        then

        reconsider Phi = {phi} as Subset of X by ZFMISC_1: 31;

        

         A3: (I -TruthEval phi) = 1 by A1, A2;

        l is (X /\ Phi) -absent by A1;

        then not l in no by FOMODEL2: 28;

        then {l} misses no by ZFMISC_1: 50;

        then ( dom f2) misses no;

        then ((I | no) +* (f2 | no)) = ((I | no) null {} ) by RELAT_1: 66;

        then (I2 | no) = (I | no) by FUNCT_4: 71;

        hence (I2 -TruthEval phi) = 1 by A3, Th13;

      end;

      hence thesis;

    end;

    theorem :: FOMODEL3:15

    for E be Equivalence_Relation of U, i be E -respecting Element of (U -InterpretersOf S) holds ((l,((E -class ) . u)) ReassignIn (i quotient E)) = (((l,u) ReassignIn i) quotient E)

    proof

      set II = (U -InterpretersOf S);

      let E be Equivalence_Relation of U;

      let i be E -respecting Element of II;

      set x = u;

      set O = ( OwnSymbolsOf S), UU = ( Class E), III = (UU -InterpretersOf S);

      reconsider X = ((E -class ) . x) as Element of UU;

      reconsider I = (i quotient E) as Element of III;

      reconsider j = ((l,x) ReassignIn i) as Element of II;

      reconsider Jj = ((l,X) ReassignIn I qua Element of III) as Element of III;

      reconsider jJ = (j quotient E) as Function;

      

       A1: ( dom Jj) = O & ( dom jJ) = O by Def17, PARTFUN1:def 2;

      set jJ = (j qua Element of II quotient E), g = (l .--> ( { {} } --> x)), h = ( { {} } --> x), G = (l .--> ( { {} } --> X));

      reconsider n = |.( ar l).| as Nat;

      

       A2: { {} } = ( 0 -tuples_on U) & ( id { {} }) is Equivalence_Relation of { {} } by FOMODEL0: 10;

      then

      reconsider Enn = ( id { {} }) as Equivalence_Relation of ( 0 -tuples_on U);

      set En = (n -placesOf E), nE = (n -tuple2Class E);

      

       A3: ( dom g) = {l} & ( dom G) = {l} & l in ( dom g) & l in ( dom G) by TARSKI:def 1;

      

       A4: En = Enn & ( dom (E -class )) = U & ( dom ( { {} } --> ((E -class ) . x))) = { {} } & ( dom h) = { {} } & (( id { {} }) \+\ ( {} .--> {} )) = {} by Lm30, FUNCT_2:def 1;

      then

       A5: En = Enn & x in ( dom (E -class )) & {} in ( dom ( { {} } --> ((E -class ) . x))) & ( id { {} }) = ( {} .--> {} ) by TARSKI:def 1, FOMODEL0: 29;

       {} in ( dom h) by TARSKI:def 1;

      then

      reconsider hh = h as Enn, E -respecting Function by Lm22;

      reconsider hhh = hh as En, E -respecting Function of (n -tuples_on U), U by A2, A4;

      now

        let s be object;

        assume s in O;

        then

        reconsider ss = s as own Element of S;

        per cases ;

          suppose

           A6: s in ( dom G);

          

           A7: s = l by A6, TARSKI:def 1;

          

          then

           A8: (jJ . s) = ((j . l) quotient E) by Def18

          .= ((n -tuple2Class E) * ((j . l) quotient ((n -placesOf E),E))) by Def15

          .= (nE * ((g . l) quotient (En,E))) by A3, FUNCT_4: 13

          .= (nE * (h quotient (En,E)) qua Relation) by FUNCOP_1: 72

          .= ((n -placesOf ((E -class ) qua Relation of U, ( Class E) ~ )) * ((E -class ) * hhh)) by Lm21

          .= (( id { {} }) qua Relation * ((E -class ) * hhh)) by Lm30

          .= (( { {} } --> ((E -class ) . x)) * ( { {} } --> {} )) by FUNCOP_1: 17, A5

          .= ( { {} } --> (( {} .--> ((E -class ) . x)) . {} )) by FUNCOP_1: 17, A5

          .= ( { {} } --> X) by FUNCOP_1: 72;

          (Jj . s) = (G . l) by A6, A7, FUNCT_4: 13

          .= ( { {} } --> X) by FUNCOP_1: 72;

          hence (Jj . s) = (jJ . s) by A8;

        end;

          suppose

           A9: not s in ( dom G);

          

          then (Jj . s) = (I . s) by FUNCT_4: 11

          .= ((i . ss) quotient E) by Def18

          .= ((j . ss) quotient E) by A9, FUNCT_4: 11

          .= (jJ . ss) by Def18;

          hence (Jj . s) = (jJ . s);

        end;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: FOMODEL3:16

    (( TheEqSymbOf S1) = ( TheEqSymbOf S2) & ( TheNorSymbOf S1) = ( TheNorSymbOf S2)) implies for I1 be Element of (U -InterpretersOf S1), I2 be Element of (U -InterpretersOf S2), phi1 be wff string of S1 st ((the adicity of S1 | (( rng phi1) /\ ( OwnSymbolsOf S1))) = (the adicity of S2 | (( rng phi1) /\ ( OwnSymbolsOf S1))) & (I1 | (( rng phi1) /\ ( OwnSymbolsOf S1))) = (I2 | (( rng phi1) /\ ( OwnSymbolsOf S1)))) holds ex phi2 be wff string of S2 st phi1 = phi2

    proof

      set O1 = ( OwnSymbolsOf S1), O2 = ( OwnSymbolsOf S2), a1 = the adicity of S1, a2 = the adicity of S2, E1 = ( TheEqSymbOf S1), E2 = ( TheEqSymbOf S2), F1 = (S1 -firstChar ), F2 = (S2 -firstChar ), AS1 = ( AtomicFormulaSymbolsOf S1), AS2 = ( AtomicFormulaSymbolsOf S2), N1 = ( TheNorSymbOf S1), N2 = ( TheNorSymbOf S2), II1 = (U -InterpretersOf S1), II2 = (U -InterpretersOf S2);

      assume

       A1: E1 = E2 & N1 = N2;

      defpred P[ Nat] means for I1 be Element of II1, I2 be Element of II2, phi1 be $1 -wff string of S1 st (a1 | (( rng phi1) /\ O1)) = (a2 | (( rng phi1) /\ O1)) & (I1 | (( rng phi1) /\ O1)) = (I2 | (( rng phi1) /\ O1)) holds ex phi2 be $1 -wff string of S2 st phi1 = phi2;

      

       A2: P[ 0 ]

      proof

        let I1 be Element of II1, I2 be Element of II2;

        let phi1 be 0 -wff string of S1;

        reconsider phi11 = phi1 as 0wff string of S1;

        set x1 = ( rng phi1), x11 = (x1 /\ O1);

        assume (a1 | x11) = (a2 | x11) & (I1 | x11) = (I2 | x11);

        then

        consider phi2 be 0wff string of S2 such that

         A3: phi11 = phi2 & (I1 -AtomicEval phi11) = (I2 -AtomicEval phi2) by Lm48, A1;

        thus thesis by A3;

      end;

      

       A4: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        set N = (n + 1);

        assume

         A5: P[n];

        let I1 be Element of II1, I2 be Element of II2;

        let phi1 be N -wff string of S1;

        set x1 = ( rng phi1), x11 = (x1 /\ O1);

        assume

         A6: (a1 | x11) = (a2 | x11) & (I1 | x11) = (I2 | x11);

        per cases ;

          suppose phi1 is 0wff;

          then

          reconsider phi11 = phi1 as 0 -wff string of S1;

          consider phi2 be 0 -wff string of S2 such that

           A7: phi11 = phi2 by A2, A6;

          phi2 is ( 0 + ( 0 * N)) -wff;

          then phi2 is ( 0 + N) -wff;

          then

          reconsider phi22 = phi2 as N -wff string of S2;

          take phi22;

          thus thesis by A7;

        end;

          suppose not phi1 is 0wff;

          then

          reconsider phi11 = phi1 as non 0wffN -wff string of S1;

          reconsider h1 = ( head phi11) as n -wff string of S1;

          set t11 = ( tail phi11), l11 = (F1 . phi11);

          

           A8: phi11 = (( <*l11*> ^ h1) ^ t11) by FOMODEL2: 23;

          then ( rng h1) c= ( rng ( <*l11*> ^ h1)) & ( rng ( <*l11*> ^ h1)) c= x1 by FINSEQ_1: 30, FINSEQ_1: 29;

          then

          reconsider y1 = ( rng h1) as non empty Subset of x1 by XBOOLE_1: 1;

          reconsider y11 = (y1 /\ O1) as Subset of x11 by XBOOLE_1: 26;

          

           A9: (I1 | (y11 null x11)) = ((I1 | x11) | y11) by RELAT_1: 71

          .= (I2 | (y11 null x11)) by RELAT_1: 71, A6;

          (a1 | (y11 null x11)) = ((a1 | x11) | y11) by RELAT_1: 71

          .= (a2 | (y11 null x11)) by RELAT_1: 71, A6;

          then

          consider h2 be n -wff string of S2 such that

           A10: h1 = h2 by A5, A9;

          per cases ;

            suppose phi11 is exal;

            then

            reconsider phi11 as exal non 0wffN -wff string of S1;

            reconsider l1 = (F1 . phi11) as literal Element of S1;

            (phi1 null {} ) is (x1 \/ {} ) -valued;

            then ( {(phi1 . 1)} \ x1) = {} ;

            then (phi1 . 1) in x1 by ZFMISC_1: 60;

            then l1 in x1 & l1 in O1 & ( dom a1) = AS1 by FOMODEL0: 6, FOMODEL1:def 19, FUNCT_2:def 1;

            then

             A11: l1 in x11 & ( dom (a1 | x11)) = (AS1 /\ x11) & l1 in AS1 by RELAT_1: 61, XBOOLE_0:def 4, FOMODEL1:def 20;

            then l1 in ( dom (a2 | x11)) & ( dom (a2 | x11)) = (x11 /\ ( dom a2)) by XBOOLE_0:def 4, RELAT_1: 61, A6;

            then l1 in ( dom a2) & ( dom a2) = AS2 by FUNCT_2:def 1;

            then

            reconsider l2 = l1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;

            l2 in O2 by A1, FOMODEL1: 15;

            then

            reconsider l2 as own Element of S2;

            ( ar l1) = ((a1 | x11) . l1) by A11, FUNCT_1: 49

            .= ( ar l2) by A6, A11, FUNCT_1: 49;

            then not l2 is low-compounding;

            then

            reconsider l2 as literal Element of S2;

            take phi2 = ( <*l2*> ^ h2);

            phi11 = (( <*l2*> ^ h1) ^ ( tail phi11)) by FOMODEL2: 23;

            hence phi1 = phi2 by A10;

            reconsider l2 as literal Element of S2;

          end;

            suppose not phi11 is exal;

            then

            reconsider phi11 as non exal non 0wffN -wff string of S1;

            reconsider t1 = ( tail phi11) as n -wff string of S1;

            reconsider z1 = ( rng t1) as non empty Subset of x1 by A8, FINSEQ_1: 30;

            reconsider z11 = (z1 /\ O1) as Subset of x11 by XBOOLE_1: 26;

            

             A12: (I1 | (z11 null x11)) = ((I2 | x11) | z11) by A6, RELAT_1: 71

            .= (I2 | (z11 null x11)) by RELAT_1: 71;

            (a1 | (z11 null x11)) = ((a1 | x11) | z11) by RELAT_1: 71

            .= (a2 | (z11 null x11)) by RELAT_1: 71, A6;

            then

            consider t2 be n -wff string of S2 such that

             A13: t1 = t2 by A5, A12;

            take phi2 = (( <*N2*> ^ h2) ^ t2);

            ((F1 . phi11) \+\ N1) = {} ;

            hence phi1 = phi2 by A1, A10, A13, A8, FOMODEL0: 29;

          end;

        end;

      end;

      

       A14: for n holds P[n] from NAT_1:sch 2( A2, A4);

      let I1 be Element of II1, I2 be Element of II2, phi1 be wff string of S1;

      set d = ( Depth phi1);

      (phi1 null 0 ) is (d + 0 ) -wff;

      then

      reconsider phi11 = phi1 as d -wff string of S1;

      set x1 = ( rng phi1), x11 = (x1 /\ O1);

      assume (a1 | x11) = (a2 | x11) & (I1 | x11) = (I2 | x11);

      then

      consider phi2 be d -wff string of S2 such that

       A15: phi2 = phi11 by A14;

      take phi2;

      thus thesis by A15;

    end;

    theorem :: FOMODEL3:17

    for I1 be Element of (U -InterpretersOf S1), I2 be Element of (U -InterpretersOf S2) st S2 is S1 -extending & X c= ( AllFormulasOf S1) & (I1 | ( OwnSymbolsOf S1)) = (I2 | ( OwnSymbolsOf S1)) holds (X is I1 -satisfied iff X is I2 -satisfied) by Lm49;

    

     Lm50: for R be total reflexive Relation of U, f be Function of X, U st x in X holds f is { [x, x]}, R -respecting

    proof

      let R be total reflexive Relation of U;

      let f be Function of X, U;

      reconsider E = { [x, x]} as Relation;

      assume

       A1: x in X;

      then

      reconsider XX = X as non empty set;

      reconsider ff = f as Function of XX, U;

      now

        let x1,x2 be set;

        assume [x1, x2] in E;

        then

         A2: [x1, x2] = [x, x] by TARSKI:def 1;

        then

         A3: x1 = x & x2 = x by XTUPLE_0: 1;

        reconsider x11 = x1, x22 = x2 as Element of XX by A1, A2, XTUPLE_0: 1;

        (ff . x11) in U & (ff . x22) in U & (ff . x11) = (ff . x22) by A3;

        hence [(f . x1), (f . x2)] in R by EQREL_1: 5;

      end;

      hence thesis;

    end;

    

     Lm51: for E be total reflexive Relation of U, f be Interpreter of l, U holds f is E -respecting

    proof

      let E be total reflexive Relation of U;

      reconsider m = |.( ar l).| as zero Nat;

      let f be Interpreter of l, U;

      (m -tuples_on U) = { {} } by FOMODEL0: 10;

      then

      reconsider ff = f as Function of { {} }, U by FOMODEL2:def 2;

       {} in { {} } by TARSKI:def 1;

      then ff is { [ {} , {} ]}, E -respecting by Lm50;

      then f is (m -placesOf E), E -respecting;

      hence thesis by Def10;

    end;

    theorem :: FOMODEL3:18

    for E be total reflexive Relation of U, f be Interpreter of l, U holds f is E -respecting by Lm51;