fomodel0.miz



    begin

    reserve A,B,C,Y,x,y,z for set,

U,D for non empty set,

X for non empty Subset of D,

d,d1,d2 for Element of D;

    reserve P,Q,R for Relation,

g for Function,

p,q for FinSequence;

    reserve f for BinOp of D,

i,m,n for Nat;

    definition

      let X be set;

      let f be Function;

      :: FOMODEL0:def1

      attr f is X -one-to-one means (f | X) is one-to-one;

    end

    definition

      let D, f;

      let X be set;

      :: FOMODEL0:def2

      attr X is f -unambiguous means f is [:X, D:] -one-to-one;

    end

    definition

      let D;

      let X be set;

      :: FOMODEL0:def3

      attr X is D -prefix means X is (D -concatenation ) -unambiguous;

    end

    definition

      let f be Function-yielding Function, g be Function;

      :: FOMODEL0:def4

      func ^^^f,g__ -> Function means ( dom it ) = (( dom f) /\ ( dom g)) & for x be set st x in ( dom it ) holds (it . x) = ((f . x) . (g . x));

      existence

      proof

        set A = (( dom f) /\ ( dom g));

        deffunc F( object) = ((f . $1) . (g . $1));

        consider h be Function such that

         A1: ( dom h) = A & for x be object st x in A holds (h . x) = F(x) from FUNCT_1:sch 3;

        take h;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set A = (( dom f) /\ ( dom g));

        let IT1,IT2 be Function;

        assume

         A2: ( dom IT1) = A & for x be set st x in ( dom IT1) holds (IT1 . x) = ((f . x) . (g . x));

        assume

         A3: ( dom IT2) = A & for x be set st x in ( dom IT2) holds (IT2 . x) = ((f . x) . (g . x));

        now

          let x be object;

          assume

           A4: x in ( dom IT1);

          

          thus (IT1 . x) = ((f . x) . (g . x)) by A2, A4

          .= (IT2 . x) by A2, A3, A4;

        end;

        hence thesis by FUNCT_1: 2, A2, A3;

      end;

    end

    definition

      let D be set;

      :: FOMODEL0:def5

      func D -pr1 -> BinOp of D equals ( pr1 (D,D));

      coherence ;

    end

    

     Lm1: g is Y -valued & g is FinSequence-like implies g is FinSequence of Y by FINSEQ_1:def 4;

    

     Lm2: Y c= ( Funcs (A,B)) implies ( union Y) c= [:A, B:]

    proof

      set AB = [:A, B:], F = ( Funcs (A,B)), X = Y;

      assume X c= F;

      then X c= F & F c= ( bool AB) by FRAENKEL: 2;

      then

      reconsider XX = X as Subset of ( bool AB) by XBOOLE_1: 1;

      ( union XX) is Subset of AB;

      hence thesis;

    end;

    

     Lm3: for X be set, f be Function holds (f is X -one-to-one iff (for x,y be set st x in (( dom f) /\ X) & y in (( dom f) /\ X) & (f . x) = (f . y) holds x = y))

    proof

      let X be set, f be Function;

      set g = (f | X);

      thus f is X -one-to-one implies (for x,y be set st x in (( dom f) /\ X) & y in (( dom f) /\ X) & (f . x) = (f . y) holds x = y)

      proof

        assume f is X -one-to-one;

        then

         A1: g is one-to-one;

        let x,y be set;

        assume x in (( dom f) /\ X);

        then

         A2: x in ( dom g) by RELAT_1: 61;

        assume y in (( dom f) /\ X);

        then

         A3: y in ( dom g) by RELAT_1: 61;

        assume (f . x) = (f . y);

        then (g . x) = (f . x) & (g . y) = (f . y) & (f . x) = (f . y) by A2, A3, FUNCT_1: 47;

        hence x = y by A1, FUNCT_1:def 4, A2, A3;

      end;

      assume

       A4: for x,y be set st x in (( dom f) /\ X) & y in (( dom f) /\ X) & (f . x) = (f . y) holds x = y;

      now

        let x,y be object;

        assume

         A5: x in ( dom g) & y in ( dom g) & (g . x) = (g . y);

        then (g . x) = (f . x) & (g . y) = (f . y) & (g . x) = (g . y) by FUNCT_1: 47;

        then x in (( dom f) /\ X) & y in (( dom f) /\ X) & (f . x) = (f . y) by A5, RELAT_1: 61;

        hence x = y by A4;

      end;

      then g is one-to-one by FUNCT_1:def 4;

      hence thesis;

    end;

    

     Lm4: A c= B & f is B -one-to-one implies f is A -one-to-one

    proof

      assume A c= B & f is B -one-to-one;

      then (f | B) is one-to-one & (f | A) = ((f | B) | A) by FUNCT_1: 51;

      hence thesis by FUNCT_1: 52;

    end;

    

     Lm5: (m -tuples_on A) meets (n -tuples_on B) implies m = n

    proof

      assume (m -tuples_on A) meets (n -tuples_on B);

      then ((m -tuples_on A) /\ (n -tuples_on B)) is non empty;

      then

      consider p be object such that

       A1: p in ((m -tuples_on A) /\ (n -tuples_on B));

      

       A2: p in (m -tuples_on A) & p in (n -tuples_on B) by XBOOLE_0:def 4, A1;

      reconsider pA = p as m -element FinSequence by FINSEQ_2: 141, A2;

      reconsider pB = p as n -element FinSequence by FINSEQ_2: 141, A2;

      m = ( len pA) by CARD_1:def 7

      .= ( len pB)

      .= n by CARD_1:def 7;

      hence thesis;

    end;

    

     Lm6: for D be set holds ( 0 -tuples_on D) = { {} }

    proof

      let D be set;

      

      thus ( 0 -tuples_on D) = {( <*> D)} by FINSEQ_2: 94

      .= { {} };

    end;

    

     Lm7: for i be Nat, Y be set holds (i -tuples_on Y) = ( Funcs (( Seg i),Y))

    proof

      let i be Nat, Y be set;

      per cases ;

        suppose

         A1: Y is empty;

        per cases ;

          suppose i is zero;

          then i is zero & ( Seg i) = {} ;

          then ( Funcs (( Seg i),Y)) = { {} } & (i -tuples_on Y) = { {} } by FUNCT_5: 57, Lm6;

          hence thesis;

        end;

          suppose i is non zero;

          then ( Funcs (( Seg i),Y)) = {} & (i -tuples_on Y) = {} by FINSEQ_3: 119, A1;

          hence thesis;

        end;

      end;

        suppose Y is non empty;

        then

        reconsider YY = Y as non empty set;

        thus thesis by FINSEQ_2: 93;

      end;

    end;

    

     Lm8: ((m -tuples_on A) /\ (B * )) c= (m -tuples_on B)

    proof

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

      set L = ((m -tuples_on A) /\ (B * )), R = (m -tuples_on B);

      let x be object;

      assume x in L;

      then

       A1: x in (m -tuples_on A) & x in (B * ) by XBOOLE_0:def 4;

      then

       A2: x is m -element FinSequence & x is FinSequence of B by FINSEQ_2: 141, FINSEQ_1:def 11;

      reconsider xx = x as FinSequence of B by A1, FINSEQ_1:def 11;

      ( len xx) = m by A2, CARD_1:def 7;

      then xx = xx & ( dom xx) = ( Seg m) & ( rng xx) c= B by FINSEQ_1:def 3;

      then xx in ( Funcs (( Seg m),B)) by FUNCT_2:def 2;

      hence x in R by Lm7;

    end;

    theorem :: FOMODEL0:1

    

     Th1: ((m -tuples_on A) /\ (B * )) = ((m -tuples_on A) /\ (m -tuples_on B))

    proof

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

      set L = ((m -tuples_on A) /\ (B * )), R = ((m -tuples_on A) /\ (m -tuples_on B));

      ((m -tuples_on A) /\ L) c= R by XBOOLE_1: 26, Lm8;

      then

       A1: (((m -tuples_on A) /\ (m -tuples_on A)) /\ (B * )) c= R by XBOOLE_1: 16;

      now

        let x be object;

        assume

         A2: x in (m -tuples_on B);

        then

        reconsider xx = x as m -element FinSequence by FINSEQ_2: 141;

        xx in (mm -tuples_on B) by A2;

        then ( len xx) = mm & ( rng xx) c= B by FINSEQ_2: 132;

        then x is FinSequence of B by FINSEQ_1:def 4;

        hence x in (B * ) by FINSEQ_1:def 11;

      end;

      then R c= L by XBOOLE_1: 26, TARSKI:def 3;

      hence thesis by A1;

    end;

    

     Lm9: (( Funcs (A,B)) /\ ( Funcs (A,C))) = ( Funcs (A,(B /\ C)))

    proof

      set L = (( Funcs (A,B)) /\ ( Funcs (A,C))), R = ( Funcs (A,(B /\ C)));

      now

        let f be object;

        assume f in L;

        then

         A1: f in ( Funcs (A,B)) & f in ( Funcs (A,C)) by XBOOLE_0:def 4;

        consider f1 be Function such that

         A2: f1 = f & ( dom f1) = A & ( rng f1) c= B by FUNCT_2:def 2, A1;

        consider f2 be Function such that

         A3: f2 = f & ( dom f2) = A & ( rng f2) c= C by FUNCT_2:def 2, A1;

        f1 = f & ( dom f1) = A & ( rng f1) c= (B /\ C) by XBOOLE_1: 19, A2, A3;

        hence f in ( Funcs (A,(B /\ C))) by FUNCT_2:def 2;

      end;

      then

       A4: L c= R;

      R c= ( Funcs (A,B)) & R c= ( Funcs (A,C)) by XBOOLE_1: 17, FUNCT_5: 56;

      then R c= L by XBOOLE_1: 19;

      hence thesis by A4;

    end;

    theorem :: FOMODEL0:2

    

     Th2: ((m -tuples_on A) /\ (B * )) = (m -tuples_on (A /\ B))

    proof

      (m -tuples_on (A /\ B)) = ( Funcs (( Seg m),(A /\ B))) by Lm7

      .= (( Funcs (( Seg m),A)) /\ ( Funcs (( Seg m),B))) by Lm9

      .= ((m -tuples_on A) /\ ( Funcs (( Seg m),B))) by Lm7

      .= ((m -tuples_on A) /\ (m -tuples_on B)) by Lm7

      .= ((m -tuples_on A) /\ (B * )) by Th1;

      hence thesis;

    end;

    theorem :: FOMODEL0:3

    

     Th3: (m -tuples_on (A /\ B)) = ((m -tuples_on A) /\ (m -tuples_on B))

    proof

      (m -tuples_on (A /\ B)) = ((m -tuples_on A) /\ (B * )) by Th2

      .= ((m -tuples_on A) /\ (m -tuples_on B)) by Th1;

      hence thesis;

    end;

    

     Lm10: for x,y be FinSequence of D holds ((D -concatenation ) . (x,y)) = (x ^ y)

    proof

      let x,y be FinSequence of D;

      reconsider x2 = x, y2 = y as Element of (D * ) by FINSEQ_1:def 11;

      reconsider x1 = x2, y1 = y2 as Element of (D *+^ ) by MONOID_0:def 34;

      

       A1: (D -concatenation ) = the multF of (D *+^ ) by MONOID_0:def 36;

      (x1 ^ y1) = (x1 * y1) by MONOID_0:def 34

      .= ((D -concatenation ) . (x1,y1)) by A1, ALGSTR_0:def 18;

      hence thesis;

    end;

    theorem :: FOMODEL0:4

    

     Th4: for x,y be FinSequence st x is U -valued & y is U -valued holds ((U -concatenation ) . (x,y)) = (x ^ y)

    proof

      let x,y be FinSequence;

      set f = (U -concatenation );

      assume x is U -valued & y is U -valued;

      then

      reconsider xx = x, yy = y as FinSequence of U by Lm1;

      (f . (xx,yy)) = (xx ^ yy) by Lm10;

      hence thesis;

    end;

    theorem :: FOMODEL0:5

    

     Th5: for x be set holds (x is non empty FinSequence of D iff x in ((D * ) \ { {} }))

    proof

      let x be set;

      thus x is non empty FinSequence of D implies x in ((D * ) \ { {} })

      proof

        assume x is non empty FinSequence of D;

        then not x in { {} } & x in (D * ) by FINSEQ_1:def 11, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 5;

      end;

      assume x in ((D * ) \ { {} });

      then x in (D * ) & not x in { {} } by XBOOLE_0:def 5;

      hence thesis by FINSEQ_1:def 11, TARSKI:def 1;

    end;

    

     Lm11: B is f -unambiguous & A c= B implies A is f -unambiguous

    proof

      assume

       A0: B is f -unambiguous & A c= B;

      then [:A, D:] c= [:B, D:] by ZFMISC_1: 95;

      then f is [:A, D:] -one-to-one by A0, Lm4;

      hence thesis;

    end;

    

     Lm12: {} is f -unambiguous

    proof

      reconsider A = [: {} , D:] as empty set;

      f is A -one-to-one;

      hence thesis;

    end;

    

     Lm13: for f,g be FinSequence holds ( dom <:f, g:>) = ( Seg ( min (( len f),( len g))))

    proof

      let f,g be FinSequence;

      set m = ( len f), n = ( len g), l = ( min (m,n));

      

      thus ( dom <:f, g:>) = (( dom f) /\ ( dom g)) by FUNCT_3:def 7

      .= (( Seg m) /\ ( dom g)) by FINSEQ_1:def 3

      .= (( Seg m) /\ ( Seg n)) by FINSEQ_1:def 3

      .= ( Seg l) by FINSEQ_2: 2;

    end;

    registration

      let D be non empty set;

      cluster (D -pr1 ) -> associative;

      coherence

      proof

        now

          let a,b,c be Element of D;

          ((D -pr1 ) . (a,((D -pr1 ) . (b,c)))) = a & ((D -pr1 ) . (((D -pr1 ) . (a,b)),c)) = ((D -pr1 ) . (a,c)) by FUNCT_3:def 4;

          hence ((D -pr1 ) . (a,((D -pr1 ) . (b,c)))) = ((D -pr1 ) . (((D -pr1 ) . (a,b)),c)) by FUNCT_3:def 4;

        end;

        hence thesis;

      end;

    end

    registration

      let D be set;

      cluster associative for BinOp of D;

      existence

      proof

        per cases ;

          suppose D is non empty;

          then

          reconsider DD = D as non empty set;

          set f = (DD -pr1 );

          reconsider ff = f as BinOp of D;

          take ff;

          thus thesis;

        end;

          suppose D is empty;

          then

          reconsider DD = D as empty set;

          set f = the BinOp of {} ;

          f is associative & f is BinOp of DD;

          hence thesis;

        end;

      end;

    end

    definition

      let X be set, Y be Subset of X;

      :: original: *

      redefine

      func Y * -> non empty Subset of (X * ) ;

      coherence by FINSEQ_1: 62;

    end

    registration

      let D be non empty set;

      cluster (D -concatenation ) -> associative;

      coherence by MONOID_0: 67;

    end

    registration

      let D be non empty set;

      cluster ((D * ) \ { {} }) -> non empty;

      coherence

      proof

        set x = the Element of D;

         <*x*> in (D * ) & not <*x*> in { {} } by TARSKI:def 1, FINSEQ_1:def 11;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    registration

      let D be non empty set, m be Nat;

      cluster m -element for Element of (D * );

      existence

      proof

        set p = the m -element FinSequence of D;

        reconsider pp = p as Element of (D * ) by FINSEQ_1:def 11;

        take pp;

        thus thesis;

      end;

    end

    definition

      let X be set;

      let f be Function;

      :: original: -one-to-one

      redefine

      :: FOMODEL0:def6

      attr f is X -one-to-one means

      : Def6: (for x,y be set st x in (X /\ ( dom f)) & y in (X /\ ( dom f)) & (f . x) = (f . y) holds x = y);

      compatibility by Lm3;

    end

    registration

      let D, f;

      cluster f -unambiguous for set;

      existence

      proof

        take {} ;

        thus thesis by Lm12;

      end;

    end

    registration

      let f be Function, x be set;

      cluster (f | {x}) -> one-to-one;

      coherence

      proof

        set g = (f | {x});

        per cases ;

          suppose x in ( dom f);

          then g = (x .--> (f . x)) by FUNCT_7: 6;

          hence thesis;

        end;

          suppose not x in ( dom f);

          then

          reconsider gg = g as empty Function by RELAT_1: 152, ZFMISC_1: 50;

          gg is one-to-one;

          hence thesis;

        end;

      end;

    end

    registration

      let e be empty set;

      identify {e} with e * ;

      compatibility by FUNCT_7: 17;

      identify e * with {e};

      compatibility ;

    end

    registration

      cluster empty -> empty-membered for set;

      coherence ;

      let e be empty set;

      cluster {e} -> empty-membered;

      coherence

      proof

         not ex x be non empty set st x in {e} by TARSKI:def 1;

        hence thesis by SETFAM_1:def 10;

      end;

    end

    registration

      let U;

      let m1 be non zero Nat;

      cluster (m1 -tuples_on U) -> with_non-empty_elements;

      coherence

      proof

         not {} is Element of (m1 -tuples_on U);

        hence thesis by SETFAM_1:def 8;

      end;

    end

    registration

      let X be empty-membered set;

      cluster -> empty-membered for Subset of X;

      coherence

      proof

        let Y be Subset of X;

         not ex x be non empty set st x in Y by SETFAM_1:def 10;

        hence thesis by SETFAM_1:def 10;

      end;

    end

    registration

      let A;

      let m0 be zero number;

      cluster (m0 -tuples_on A) -> empty-membered;

      coherence by Lm6;

    end

    registration

      let e be empty set;

      let m1 be non zero Nat;

      cluster (m1 -tuples_on e) -> empty;

      coherence by FINSEQ_3: 119;

    end

    registration

      let D, f;

      let e be empty set;

      cluster (e /\ f) -> f -unambiguous;

      coherence by Lm12;

    end

    registration

      let U;

      let e be empty set;

      cluster (e /\ U) -> U -prefix;

      coherence

      proof

        set f = (U -concatenation );

        (e /\ f) is f -unambiguous;

        hence thesis;

      end;

    end

    registration

      let U;

      cluster U -prefix for set;

      existence

      proof

        take ( {} /\ U);

        thus thesis;

      end;

    end

    definition

      let D, f;

      let x be FinSequence of D;

      :: FOMODEL0:def7

      func MultPlace (f,x) -> Function means

      : Def7: ( dom it ) = NAT & (it . 0 ) = (x . 1) & for n be Nat holds (it . (n + 1)) = (f . ((it . n),(x . (n + 2))));

      existence

      proof

        deffunc F( Nat, set) = (f . ($2,(x . ($1 + 2))));

        consider f1 be Function such that

         A1: ( dom f1) = NAT & (f1 . 0 ) = (x . 1) & for n be Nat holds (f1 . (n + 1)) = F(n,.) from NAT_1:sch 11;

        take f1;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function;

        assume

         A2: ( dom IT1) = NAT & (IT1 . 0 ) = (x . 1) & for n be Nat holds (IT1 . (n + 1)) = (f . ((IT1 . n),(x . (n + 2))));

        assume

         A3: ( dom IT2) = NAT & (IT2 . 0 ) = (x . 1) & for n be Nat holds (IT2 . (n + 1)) = (f . ((IT2 . n),(x . (n + 2))));

        deffunc RecFun( Nat, set) = (f . ($2,(x . ($1 + 2))));

        

         A4: ( dom IT1) = NAT by A2;

        

         A5: (IT1 . 0 ) = (x . 1) by A2;

        

         A6: for n be Nat holds (IT1 . (n + 1)) = RecFun(n,.) by A2;

        

         A7: ( dom IT2) = NAT by A3;

        

         A8: (IT2 . 0 ) = (x . 1) by A3;

        

         A9: for n be Nat holds (IT2 . (n + 1)) = RecFun(n,.) by A3;

        thus thesis from NAT_1:sch 15( A4, A5, A6, A7, A8, A9);

      end;

    end

    

     Lm14: for x be FinSequence of D holds for m be Nat holds ((m + 1) <= ( len x) implies (( MultPlace (f,x)) . m) in D) & for n be Nat st n >= (m + 1) holds (( MultPlace (f,(x | n))) . m) = (( MultPlace (f,x)) . m)

    proof

      let x be FinSequence of D;

      defpred Q[ Nat] means ($1 + 1) <= ( len x) implies (( MultPlace (f,x)) . $1) in D;

      

       A1: Q[ 0 ]

      proof

        assume ( 0 + 1) <= ( len x);

        then 1 in ( Seg ( len x));

        then 1 in ( dom x) by FINSEQ_1:def 3;

        then (x . 1) in ( rng x) & ( rng x) c= D by FUNCT_1:def 3;

        then (x . 1) in D & (( MultPlace (f,x)) . 0 ) = (x . 1) by Def7;

        hence thesis;

      end;

      

       A2: for m be Nat st Q[m] holds Q[(m + 1)]

      proof

        let m be Nat;

        assume

         A3: Q[m];

        assume

         A4: ((m + 1) + 1) <= ( len x);

        then (m + 2) <= ( len x) & 1 <= (m + 2) by NAT_1: 12;

        then (m + 2) in ( Seg ( len x));

        then (m + 2) in ( dom x) by FINSEQ_1:def 3;

        then

         A5: (x . (m + 2)) in ( rng x) & ( rng x) c= D by FUNCT_1:def 3;

        

         A6: ((m + 1) <= (m + 2) implies (m + 1) <= ( len x)) by A4, XXREAL_0: 2;

         [(( MultPlace (f,x)) . m), (x . (m + 2))] in [:D, D:] by A6, A3, XREAL_1: 8, A5, ZFMISC_1:def 2;

        then (f . ((( MultPlace (f,x)) . m),(x . (m + 2)))) in D by FUNCT_2: 5;

        hence thesis by Def7;

      end;

      defpred P[ Nat] means for n be Nat st n >= ($1 + 1) holds (( MultPlace (f,(x | n))) . $1) = (( MultPlace (f,x)) . $1);

      

       A7: P[ 0 ]

      proof

        let n be Nat;

        assume

         A8: n >= ( 0 + 1);

        (( MultPlace (f,(x | n))) . 0 ) = ((x | n) . 1) by Def7

        .= (x . 1) by FINSEQ_3: 112, A8

        .= (( MultPlace (f,x)) . 0 ) by Def7;

        hence thesis;

      end;

      

       A9: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A10: P[m];

        let n be Nat;

        assume

         A11: n >= ((m + 1) + 1);

        then

         A12: (m + 2) >= (m + 1) & n >= (m + 2) by XREAL_1: 8;

        (( MultPlace (f,(x | n))) . (m + 1)) = (f . ((( MultPlace (f,(x | n))) . m),((x | n) . (m + 2)))) by Def7

        .= (f . ((( MultPlace (f,x)) . m),((x | n) . (m + 2)))) by A10, XXREAL_0: 2, A12

        .= (f . ((( MultPlace (f,x)) . m),(x . (m + 2)))) by A11, FINSEQ_3: 112

        .= (( MultPlace (f,x)) . (m + 1)) by Def7;

        hence thesis;

      end;

      defpred R[ Nat] means P[$1] & Q[$1];

      

       A13: R[ 0 ] by A7, A1;

      

       A14: for m be Nat st R[m] holds R[(m + 1)] by A9, A2;

      for m be Nat holds R[m] from NAT_1:sch 2( A13, A14);

      hence thesis;

    end;

    definition

      let D, f;

      let x be Element of ((D * ) \ { {} });

      :: FOMODEL0:def8

      func MultPlace (f,x) -> Function equals ( MultPlace (f,x qua Element of (D * )));

      coherence ;

    end

    definition

      let D, f;

      :: FOMODEL0:def9

      func MultPlace (f) -> Function of ((D * ) \ { {} }), D means

      : Def9: for x be Element of ((D * ) \ { {} }) holds (it . x) = (( MultPlace (f,x)) . (( len x) - 1));

      existence

      proof

        defpred P[ Element of ((D * ) \ { {} }), Element of D] means $2 = (( MultPlace (f,$1)) . (( len $1) - 1));

        

         A1: for x be Element of ((D * ) \ { {} }) holds ex y be Element of D st P[x, y]

        proof

          let x be Element of ((D * ) \ { {} });

          reconsider x1 = x as Element of (D * );

           not x1 in { {} } by XBOOLE_0:def 5;

          then x1 <> {} by TARSKI:def 1;

          then ( len x1) >= 1 by FINSEQ_1: 20;

          then (( len x1) - 1) in NAT by INT_1: 3, XREAL_1: 48;

          then

          reconsider m = (( len x1) - 1) as Nat;

          

           A2: (m + 1) <= ( len x1);

          reconsider y = (( MultPlace (f,x1)) . m) as Element of D by Lm14, A2;

          take y;

          thus thesis;

        end;

        consider g be Function of ((D * ) \ { {} }), D such that

         A3: for x be Element of ((D * ) \ { {} }) holds P[x, (g . x)] from FUNCT_2:sch 3( A1);

        take g;

        thus thesis by A3;

      end;

      uniqueness

      proof

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

        

         A4: ( dom IT1) = ((D * ) \ { {} }) & ( dom IT2) = ((D * ) \ { {} }) by FUNCT_2:def 1;

        assume

         A5: for x be Element of ((D * ) \ { {} }) holds (IT1 . x) = (( MultPlace (f,x)) . (( len x) - 1));

        assume

         A6: for x be Element of ((D * ) \ { {} }) holds (IT2 . x) = (( MultPlace (f,x)) . (( len x) - 1));

        now

          let x be object;

          assume x in ( dom IT1);

          then

          reconsider xx = x as Element of ((D * ) \ { {} });

          (IT1 . x) = (( MultPlace (f,xx)) . (( len xx) - 1)) by A5

          .= (IT2 . x) by A6;

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

        end;

        hence thesis by FUNCT_1: 2, A4;

      end;

    end

    

     Lm15: for x be non empty FinSequence of D, y be Element of D holds (( MultPlace f) . <*y*>) = y & (( MultPlace f) . (x ^ <*y*>)) = (f . ((( MultPlace f) . x),y))

    proof

      set F = ( MultPlace f);

      let x be non empty FinSequence of D, y be Element of D;

      consider k be Nat such that

       A1: (k + 1) = ( len x) by NAT_1: 6;

      reconsider x0 = x as Element of ((D * ) \ { {} }) by Th5;

      reconsider x1 = (x ^ <*y*>) as non empty FinSequence of D;

      1 in ( Seg 1);

      then 1 in ( dom <*y*>) by FINSEQ_1:def 8;

      

      then

       A2: (x1 . (( len x) + 1)) = ( <*y*> . 1) by FINSEQ_1:def 7

      .= y by FINSEQ_1: 40;

      

       A3: (x1 | ( len x)) = (x | ( len x)) by FINSEQ_5: 22

      .= x by FINSEQ_3: 49;

      

       A4: ( len <*y*>) = 1 by FINSEQ_1: 40;

      then

       A5: ( len x1) = (( len x) + 1) by FINSEQ_1: 22;

      reconsider y1 = <*y*> as non empty FinSequence of D;

      reconsider y2 = y1 as Element of ((D * ) \ { {} }) by Th5;

      (( len y2) - 1) = 0 by A4;

      

      then (F . y2) = (( MultPlace (f,y2)) . 0 ) by Def9

      .= (y2 . 1) by Def7

      .= y by FINSEQ_1:def 8;

      hence (F . <*y*>) = y;

      reconsider x2 = x1 as Element of ((D * ) \ { {} }) by Th5;

      (F . x2) = (( MultPlace (f,x2)) . (( len x2) - 1)) by Def9

      .= (f . ((( MultPlace (f,x2)) . k),(x2 . (k + 2)))) by Def7, A1, A5

      .= (f . ((( MultPlace (f,x0)) . (( len x) - 1)),(x2 . (( len x) + 1)))) by A3, A1, Lm14

      .= (f . ((F . x0),y)) by A2, Def9;

      hence thesis;

    end;

    

     Lm16: for X be set holds (f is [:X, D:] -one-to-one iff (for x,y,d1,d2 be set st x in (X /\ D) & y in (X /\ D) & d1 in D & d2 in D & (f . (x,d1)) = (f . (y,d2)) holds (x = y & d1 = d2)))

    proof

      

       A1: ( dom f) = [:D, D:] by FUNCT_2:def 1;

      let X be set;

      thus f is [:X, D:] -one-to-one implies (for x,y,d1,d2 be set st x in (X /\ D) & y in (X /\ D) & d1 in D & d2 in D & (f . (x,d1)) = (f . (y,d2)) holds (x = y & d1 = d2))

      proof

        assume

         A2: f is [:X, D:] -one-to-one;

        let x,y,d1,d2 be set;

        assume

         A3: x in (X /\ D) & y in (X /\ D) & d1 in D & d2 in D & (f . (x,d1)) = (f . (y,d2));

        then [x, d1] in [:(X /\ D), (D /\ D):] & [y, d2] in [:(X /\ D), (D /\ D):] by ZFMISC_1:def 2;

        then

         A4: [x, d1] in ( [:X, D:] /\ [:D, D:]) & [y, d2] in ( [:X, D:] /\ [:D, D:]) by ZFMISC_1: 100;

         [x, d1] = [y, d2] by A1, A2, A4, A3;

        hence x = y & d1 = d2 by XTUPLE_0: 1;

      end;

      assume

       A5: for x,y,d1,d2 be set st x in (X /\ D) & y in (X /\ D) & d1 in D & d2 in D & (f . (x,d1)) = (f . (y,d2)) holds x = y & d1 = d2;

      now

        let x,y be set;

        assume

         A6: x in ( [:X, D:] /\ ( dom f)) & y in ( [:X, D:] /\ ( dom f)) & (f . x) = (f . y);

        then

         A7: x in [:(X /\ D), (D /\ D):] & y in [:(X /\ D), (D /\ D):] & (f . x) = (f . y) by ZFMISC_1: 100, A1;

        then

        consider x1,d1 be object such that

         A8: x1 in (X /\ D) & d1 in D & x = [x1, d1] by ZFMISC_1:def 2;

        consider x2,d2 be object such that

         A9: x2 in (X /\ D) & d2 in D & y = [x2, d2] by ZFMISC_1:def 2, A7;

        x1 in (X /\ D) & x2 in (X /\ D) & d1 in D & d2 in D & (f . (x1,d1)) = (f . (x2,d2)) by A8, A9, A6;

        then x1 = x2 & d1 = d2 by A5;

        hence x = y by A8, A9;

      end;

      hence f is [:X, D:] -one-to-one;

    end;

    definition

      let D, f;

      let X be set;

      :: original: -unambiguous

      redefine

      :: FOMODEL0:def10

      attr X is f -unambiguous means

      : Def10: for x,y,d1,d2 be set st x in (X /\ D) & y in (X /\ D) & d1 in D & d2 in D & (f . (x,d1)) = (f . (y,d2)) holds (x = y & d1 = d2);

      compatibility by Lm16;

    end

    

     Lm17: f is associative implies for d be Element of D holds (for m be Nat, x be Element of ((m + 1) -tuples_on D) holds (( MultPlace f) . ( <*d*> ^ x)) = (f . (d,(( MultPlace f) . x))))

    proof

      set F = ( MultPlace f);

      assume

       A1: f is associative;

      let d be Element of D;

      defpred P[ Nat] means for x be Element of (($1 + 1) -tuples_on D) holds (F . ( <*d*> ^ x)) = (f . (d,(F . x)));

      

       A2: P[ 0 ]

      proof

        let x be Element of (( 0 + 1) -tuples_on D);

        consider xx be Element of D such that

         A3: x = <*xx*> by FINSEQ_2: 97;

        (F . ( <*d*> ^ x)) = (f . ((F . <*d*>),xx)) by Lm15, A3

        .= (f . (d,xx)) by Lm15

        .= (f . (d,(F . x))) by Lm15, A3;

        hence thesis;

      end;

      

       A4: for m be Nat holds ( P[m] implies P[(m + 1)])

      proof

        let m be Nat;

        assume

         A5: P[m];

        let x be Element of (((m + 1) + 1) -tuples_on D);

        ((m + 1) + 0 ) <= ((m + 1) + 1) & ( len x) = ((m + 1) + 1) by CARD_1:def 7, XREAL_1: 8;

        then ( len (x | (m + 1))) = (m + 1) by FINSEQ_1: 59;

        then

        reconsider xx = (x | (m + 1)) as Element of ((m + 1) -tuples_on D) by FINSEQ_2: 92;

        reconsider xxx = xx as non empty FinSequence of D;

        reconsider y = (x /. ( len x)) as Element of D;

        reconsider XX = (F . xxx) as Element of D by FUNCT_2: 5, Th5;

        

         A6: ((m + 1) + 1) = ( len x) by CARD_1:def 7;

        

        then (F . ( <*d*> ^ x)) = (F . ( <*d*> ^ ((x | (m + 1)) ^ <*y*>))) by FINSEQ_5: 21

        .= (F . (( <*d*> ^ xx) ^ <*y*>)) by FINSEQ_1: 32

        .= (f . ((F . ( <*d*> ^ xx)),y)) by Lm15

        .= (f . ((f . (d,(F . xx))),y)) by A5

        .= (f . (d,(f . (XX,y)))) by A1

        .= (f . (d,(F . (xxx ^ <*y*>)))) by Lm15

        .= (f . (d,(F . x))) by FINSEQ_5: 21, A6;

        hence thesis;

      end;

      thus for m be Nat holds P[m] from NAT_1:sch 2( A2, A4);

    end;

    

     Lm18: (f is associative & X is f -unambiguous) implies (( MultPlace f) .: ((m + 1) -tuples_on X)) is f -unambiguous

    proof

      set F = ( MultPlace f);

      assume

       A1: f is associative;

      assume

       A2: X is f -unambiguous;

      defpred P[ Nat] means (F .: (($1 + 1) -tuples_on X)) is f -unambiguous;

      

       A3: P[ 0 ]

      proof

        set Z = (( 0 + 1) -tuples_on X);

        set Y = (F .: Z);

        for x,y,d1,d2 be set st x in (Y /\ D) & y in (Y /\ D) & d1 in D & d2 in D & (f . (x,d1)) = (f . (y,d2)) holds x = y & d1 = d2

        proof

          let x,y,d1,d2 be set;

          assume x in (Y /\ D);

          then x in Y by XBOOLE_0:def 4;

          then

          consider uu be object such that

           A4: uu in ( dom F) & [uu, x] in F & uu in Z by RELAT_1: 110;

          assume y in (Y /\ D);

          then y in Y by XBOOLE_0:def 4;

          then

          consider vv be object such that

           A5: vv in ( dom F) & [vv, y] in F & vv in Z by RELAT_1: 110;

          assume d1 in D;

          then

          reconsider d11 = d1 as Element of D;

          assume d2 in D;

          then

          reconsider d22 = d2 as Element of D;

          reconsider u = uu as Element of (1 -tuples_on X) by A4;

          reconsider v = vv as Element of (1 -tuples_on X) by A5;

          assume (f . (x,d1)) = (f . (y,d2));

          then

           A6: (f . (x,d1)) = (f . (y,d2)) & (F . u) = x & (F . v) = y by A4, A5, FUNCT_1:def 2;

          consider ee be Element of X such that

           A7: u = <*ee*> by FINSEQ_2: 97;

          consider ff be Element of X such that

           A8: v = <*ff*> by FINSEQ_2: 97;

          reconsider eee = ee, fff = ff as Element of D;

          (f . ((F . <*eee*>),d1)) = (f . ((F . <*fff*>),d2)) & (F . <*eee*>) = eee & (F . <*fff*>) = fff by A6, A7, A8, Lm15;

          then ee in (X /\ D) & ff in (X /\ D) & d11 in D & d22 in D & (f . (ee,d11)) = (f . (ff,d22)) by XBOOLE_0:def 4;

          hence thesis by A6, A7, A8, A2;

        end;

        hence thesis by Def10;

      end;

      

       A9: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A10: P[m];

        set Z = (((m + 1) + 1) -tuples_on X);

        set Y = (F .: Z);

        for x,y,d1,d2 be set st x in (Y /\ D) & y in (Y /\ D) & d1 in D & d2 in D & (f . (x,d1)) = (f . (y,d2)) holds x = y & d1 = d2

        proof

          let x,y,d1,d2 be set;

          assume x in (Y /\ D);

          then x in Y by XBOOLE_0:def 4;

          then

          consider uu be object such that

           A11: uu in ( dom F) & [uu, x] in F & uu in Z by RELAT_1: 110;

          assume y in (Y /\ D);

          then y in Y by XBOOLE_0:def 4;

          then

          consider vv be object such that

           A12: vv in ( dom F) & [vv, y] in F & vv in Z by RELAT_1: 110;

          assume d1 in D;

          then

          reconsider d11 = d1 as Element of D;

          assume d2 in D;

          then

          reconsider d22 = d2 as Element of D;

          reconsider u = uu as Element of (((m + 1) + 1) -tuples_on X) by A11;

          reconsider v = vv as Element of (((m + 1) + 1) -tuples_on X) by A12;

          ( len u) = ((m + 1) + 1) & ( len v) = ((m + 1) + 1) & (m + 1) <= ((m + 1) + 1) by CARD_1:def 7, NAT_1: 11;

          then

           A13: u = ((u | (m + 1)) ^ <*(u /. ( len u))*>) & v = ((v | (m + 1)) ^ <*(v /. ( len v))*>) & ( len (u | (m + 1))) = (m + 1) & ( len (v | (m + 1))) = (m + 1) by FINSEQ_5: 21, FINSEQ_1: 59;

          then

          reconsider u1 = (u | (m + 1)), v1 = (v | (m + 1)) as Tuple of (m + 1), X by CARD_1:def 7;

          ( rng u1) c= D & ( rng v1) c= D by XBOOLE_1: 1;

          then

          reconsider u2 = u1, v2 = v1 as non empty FinSequence of D by FINSEQ_1:def 4;

          reconsider u3 = u2, v3 = v2 as Element of ((D * ) \ { {} }) by Th5;

          reconsider u4 = u2, v4 = v3 as Element of ((m + 1) -tuples_on X) by FINSEQ_2: 131;

          reconsider ul = (u /. ( len u)), vl = (v /. ( len v)) as Element of D by TARSKI:def 3;

          

           A14: ul in (X /\ D) & vl in (X /\ D) by XBOOLE_0:def 4;

          

           A15: (F . (u2 ^ <*ul*>)) = (f . ((F . u2),ul)) & (F . (v2 ^ <*vl*>)) = (f . ((F . v2),vl)) by Lm15;

          

           A16: (f . ((f . ((F . u3),ul)),d11)) = (f . ((F . u3),(f . (ul,d11)))) & (f . ((f . ((F . v3),vl)),d22)) = (f . ((F . v3),(f . (vl,d22)))) by A1;

          assume (f . (x,d1)) = (f . (y,d2));

          then

           A17: (f . (x,d1)) = (f . (y,d2)) & (F . u) = x & (F . v) = y by A11, A12, FUNCT_1:def 2;

          ( dom F) = ((D * ) \ { {} }) by FUNCT_2:def 1;

          then u3 in ( dom F) & v3 in ( dom F) & u4 in ((m + 1) -tuples_on X) & v4 in ((m + 1) -tuples_on X);

          then (F . u4) in (F .: ((m + 1) -tuples_on X)) & (F . v4) in (F .: ((m + 1) -tuples_on X)) & (f . (ul,d11)) in D & (f . (vl,d22)) in D by FUNCT_1:def 6;

          then (F . u4) in ((F .: ((m + 1) -tuples_on X)) /\ D) & (F . v4) in ((F .: ((m + 1) -tuples_on X)) /\ D) & (f . (ul,d11)) in D & (f . (vl,d22)) in D by XBOOLE_0:def 4;

          then

           A18: (F . u3) = (F . v3) & (f . (ul,d11)) = (f . (vl,d22)) by A17, A13, A15, A16, A10, Def10;

          thus x = y & d1 = d2 by A18, A2, A14, A17, A13, A15;

        end;

        hence thesis by Def10;

      end;

      for m be Nat holds P[m] from NAT_1:sch 2( A3, A9);

      hence thesis;

    end;

    

     Lm19: f is associative & Y is f -unambiguous implies (( MultPlace f) .: ((m + 1) -tuples_on Y)) is f -unambiguous

    proof

      set F = ( MultPlace f);

      

       A1: ( dom F) = ((D * ) \ { {} }) by FUNCT_2:def 1;

      assume f is associative & Y is f -unambiguous;

      then

       A2: f is associative & (Y /\ D) is f -unambiguous by XBOOLE_1: 17, Lm11;

      

       A3: (F .: ((m + 1) -tuples_on Y)) = (F .: (((D * ) \ { {} }) /\ ((m + 1) -tuples_on Y))) by A1, RELAT_1: 112

      .= (F .: (((D * ) /\ ((m + 1) -tuples_on Y)) \ { {} })) by XBOOLE_1: 49

      .= (F .: (((m + 1) -tuples_on (Y /\ D)) \ { {} })) by Th2

      .= (F .: (((m + 1) -tuples_on (Y /\ D)) \ ( 0 -tuples_on Y))) by Lm6

      .= (F .: ((m + 1) -tuples_on (Y /\ D))) by Lm5, XBOOLE_1: 83;

      per cases ;

        suppose (Y /\ D) <> {} ;

        then

        reconsider YY = (Y /\ D) as non empty Subset of D by XBOOLE_1: 17;

        (F .: ((m + 1) -tuples_on Y)) = (F .: ((m + 1) -tuples_on YY)) by A3;

        hence thesis by Lm18, A2;

      end;

        suppose (Y /\ D) = {} ;

        then (F .: ((m + 1) -tuples_on Y)) = {} by A3;

        hence thesis;

      end;

    end;

    

     Lm20: (f is associative & X is f -unambiguous) implies ( MultPlace f) is ((m + 1) -tuples_on X) -one-to-one

    proof

      set F = ( MultPlace f);

      

       A1: ( dom F) = ((D * ) \ { {} }) by FUNCT_2:def 1;

      defpred P[ Nat] means F is (($1 + 1) -tuples_on X) -one-to-one;

      assume

       A2: f is associative & X is f -unambiguous;

      

       A3: P[ 0 ]

      proof

        now

          let x,y be set;

          assume

           A4: x in ((( 0 + 1) -tuples_on X) /\ ( dom F)) & y in ((( 0 + 1) -tuples_on X) /\ ( dom F)) & (F . x) = (F . y);

          then

           A5: x is Element of (1 -tuples_on X) & y is Element of (1 -tuples_on X) & (F . x) = (F . y) by XBOOLE_0:def 4;

          consider u be Element of X such that

           A6: x = <*u*> by FINSEQ_2: 97, A5;

          consider v be Element of X such that

           A7: y = <*v*> by FINSEQ_2: 97, A5;

          reconsider uu = u, vv = v as Element of D;

          uu = (F . y) by A4, A6, Lm15

          .= vv by A7, Lm15;

          hence x = y by A6, A7;

        end;

        hence F is (( 0 + 1) -tuples_on X) -one-to-one;

      end;

      

       A8: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A9: P[m];

        set goal = (((m + 1) + 1) -tuples_on X);

        now

          let x,y be set;

          assume

           A10: x in (goal /\ ( dom F)) & y in (goal /\ ( dom F)) & (F . x) = (F . y);

          reconsider xx = x, yy = y as Element of (((m + 1) + 1) -tuples_on X) by XBOOLE_0:def 4, A10;

          ( len xx) = ((m + 1) + 1) & ( len yy) = ((m + 1) + 1) & ((m + 1) + 0 ) <= ((m + 1) + 1) by CARD_1:def 7, NAT_1: 11;

          then ( len (xx | (m + 1))) = (m + 1) & ( len (yy | (m + 1))) = (m + 1) by FINSEQ_1: 59;

          then

          reconsider x1 = (xx | (m + 1)), y1 = (yy | (m + 1)) as Element of ((m + 1) -tuples_on X) by FINSEQ_2: 92;

          reconsider x11 = x1, y11 = y1 as non empty FinSequence of X;

          ( rng x11) c= D & ( rng y11) c= D by XBOOLE_1: 1;

          then

          reconsider x111 = x11, y111 = y11 as non empty FinSequence of D by FINSEQ_1:def 4;

          reconsider xl = (xx /. ( len xx)), yl = (yy /. ( len yy)) as Element of D by TARSKI:def 3;

          

           A11: (F . (x111 ^ <*xl*>)) = (f . ((F . x111),xl)) & (F . (y111 ^ <*yl*>)) = (f . ((F . y111),yl)) by Lm15;

          ( len xx) = ((m + 1) + 1) & ( len yy) = ((m + 1) + 1) by CARD_1:def 7;

          then

           A12: xx = (x1 ^ <*xl*>) & yy = (y1 ^ <*yl*>) by FINSEQ_5: 21;

          

           A13: x111 in ( dom F) & x1 in ((m + 1) -tuples_on X) & y111 in ( dom F) & y1 in ((m + 1) -tuples_on X) by Th5, A1;

          then (F . x1) in (F .: ((m + 1) -tuples_on X)) & (F . x111) in D & (F . y1) in (F .: ((m + 1) -tuples_on X)) & (F . y111) in D by PARTFUN1: 4, FUNCT_1:def 6;

          then

           A14: (F . x1) in ((F .: ((m + 1) -tuples_on X)) /\ D) & (F . y1) in ((F .: ((m + 1) -tuples_on X)) /\ D) & xl in D & yl in D & (f . ((F . x1),xl)) = (f . ((F . y1),yl)) by XBOOLE_0:def 4, A12, A11, A10;

          (F .: ((m + 1) -tuples_on X)) is f -unambiguous by A2, Lm18;

          then

           A15: (F . x1) = (F . y1) & xl = yl by A14;

          x1 in (((m + 1) -tuples_on X) /\ ( dom F)) & y1 in (((m + 1) -tuples_on X) /\ ( dom F)) by A13, XBOOLE_0:def 4;

          hence x = y by A15, A9, Def6, A12;

        end;

        hence F is goal -one-to-one;

      end;

      for m be Nat holds P[m] from NAT_1:sch 2( A3, A8);

      hence thesis;

    end;

    

     Lm21: (f is associative & Y is f -unambiguous) implies ( MultPlace f) is ((m + 1) -tuples_on Y) -one-to-one

    proof

      assume

       A1: f is associative & Y is f -unambiguous;

      set F = ( MultPlace f);

      

       A2: (F | ((m + 1) -tuples_on Y)) = ((F | ((D * ) \ { {} })) | ((m + 1) -tuples_on Y))

      .= (F | (((D * ) \ { {} }) /\ ((m + 1) -tuples_on Y))) by RELAT_1: 71

      .= (F | (((D * ) /\ ((m + 1) -tuples_on Y)) \ { {} })) by XBOOLE_1: 49

      .= (F | ((D * ) /\ (((m + 1) -tuples_on Y) \ { {} }))) by XBOOLE_1: 49

      .= (F | ((D * ) /\ (((m + 1) -tuples_on Y) \ ( 0 -tuples_on Y)))) by Lm6

      .= (F | ((D * ) /\ ((m + 1) -tuples_on Y))) by XBOOLE_1: 83, Lm5

      .= (F | ((m + 1) -tuples_on (Y /\ D))) by Th2;

      

       A3: (Y /\ D) is f -unambiguous by Lm11, A1, XBOOLE_1: 17;

      per cases ;

        suppose (D /\ Y) <> {} ;

        then

        reconsider X = (D /\ Y) as non empty Subset of D by XBOOLE_1: 17;

        F is ((m + 1) -tuples_on X) -one-to-one by Lm20, A3, A1;

        then (F | ((m + 1) -tuples_on Y)) is one-to-one by A2;

        hence thesis;

      end;

        suppose (D /\ Y) = {} ;

        hence thesis by A2;

      end;

    end;

    definition

      let D;

      :: FOMODEL0:def11

      func D -firstChar -> Function of ((D * ) \ { {} }), D equals ( MultPlace (D -pr1 ));

      coherence ;

    end

    

     Lm22: for w be non empty FinSequence of D holds ((D -firstChar ) . w) = (w . 1)

    proof

      let w be non empty FinSequence of D;

      consider d be Element of D, df1 be FinSequence of D such that

       A1: d = (w . 1) & w = ( <*d*> ^ df1) by FINSEQ_3: 102;

      set f = (D -pr1 ), F = ( MultPlace f);

      per cases ;

        suppose ( len w) <= 1;

        then ( len w) <= 0 or ( len w) = ( 0 + 1) by NAT_1: 8;

        then w = <*d*> by A1, FINSEQ_1: 40;

        hence thesis by Lm15, A1;

      end;

        suppose

         A2: ( len w) > 1;

        ( len w) = (( len <*d*>) + ( len df1)) by A1, FINSEQ_1: 22

        .= (1 + ( len df1)) by FINSEQ_1: 40;

        then ( len df1) <> 0 by A2;

        then

        consider k be Nat such that

         A3: ( len df1) = (k + 1) by NAT_1: 6;

        reconsider df11 = df1 as Element of ((k + 1) -tuples_on D) by A3, FINSEQ_2: 133;

        reconsider df111 = df11 as Element of ((D * ) \ { {} }) by Th5;

        (F . w) = (( pr1 (D,D)) . (d,(( MultPlace f) . df111))) by A1, Lm17

        .= (w . 1) by FUNCT_3:def 4, A1;

        hence thesis;

      end;

    end;

    theorem :: FOMODEL0:6

    

     Th6: for p be FinSequence st p is U -valued & p is non empty holds ((U -firstChar ) . p) = (p . 1)

    proof

      let p be FinSequence;

      assume p is U -valued & p is non empty;

      then

      reconsider pp = p as non empty FinSequence of U by Lm1;

      ((U -firstChar ) . pp) = (pp . 1) by Lm22;

      hence thesis;

    end;

    definition

      let D;

      :: FOMODEL0:def12

      func D -multiCat -> Function equals (( {} .--> {} ) +* ( MultPlace (D -concatenation )));

      coherence ;

    end

    definition

      let D;

      :: original: -multiCat

      redefine

      func D -multiCat -> Function of ((D * ) * ), (D * ) ;

      coherence

      proof

        

         A1: { {} } c= ((D * ) * ) & { {} } c= (D * ) by ZFMISC_1: 31, FINSEQ_1: 49;

        then

         A2: ( { {} } \/ ((D * ) * )) = ((D * ) * ) & ( { {} } \/ (D * )) = (D * ) by XBOOLE_1: 12;

        set f = ( {} .--> {} );

        set g = ( MultPlace (D -concatenation ));

        

         A3: ( dom f) = { {} } & ( rng f) c= { {} } by FUNCOP_1: 13;

        

         A4: ( dom g) = (((D * ) * ) \ { {} }) & ( rng g) c= (D * ) by FUNCT_2:def 1;

        (( dom f) \/ ( dom g)) = ( { {} } \/ ((D * ) * )) by XBOOLE_1: 39, A4;

        then

         A5: (( dom f) \/ ( dom g)) = ((D * ) * ) by A1, XBOOLE_1: 12;

        (( rng f) \/ ( rng g)) c= (D * ) & ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by A2, A3, XBOOLE_1: 13, FUNCT_4: 17;

        then ( dom (D -multiCat )) = ((D * ) * ) & ( rng (D -multiCat )) c= (D * ) by FUNCT_4:def 1, A5;

        hence thesis by RELSET_1: 4, FUNCT_2: 67;

      end;

    end

    

     Lm23: ((D -multiCat ) | (((D * ) * ) \ { {} })) = ( MultPlace (D -concatenation ))

    proof

      set f = (D -concatenation );

      set F = ( MultPlace f);

      ( dom F) = (((D * ) * ) \ { {} }) by FUNCT_2:def 1;

      hence thesis;

    end;

    

     Lm24: ((D -multiCat ) | (Y \ { {} })) = (( MultPlace (D -concatenation )) | Y)

    proof

      set F = (D -multiCat );

      (F | (Y \ { {} })) = ((F | ((D * ) * )) | (Y \ { {} }))

      .= (F | (((D * ) * ) /\ (Y \ { {} }))) by RELAT_1: 71

      .= (F | ((((D * ) * ) /\ Y) \ { {} })) by XBOOLE_1: 49

      .= ((D -multiCat ) | (Y /\ (((D * ) * ) \ { {} }))) by XBOOLE_1: 49

      .= (((D -multiCat ) | (((D * ) * ) \ { {} })) | Y) by RELAT_1: 71

      .= (( MultPlace (D -concatenation )) | Y) by Lm23;

      hence thesis;

    end;

    

     Lm25: ( {} .--> {} ) tolerates ( MultPlace (D -concatenation ))

    proof

      set f = ( {} .--> {} );

      set g = ( MultPlace (D -concatenation ));

      ( dom f) = { {} } & ( dom g) = (((D * ) * ) \ { {} }) by FUNCT_2:def 1;

      then for x be object st x in (( dom g) /\ ( dom f)) holds (f . x) = (g . x) by XBOOLE_1: 79, XBOOLE_0:def 7;

      hence thesis by PARTFUN1:def 4;

    end;

    registration

      let D;

      let e be empty set;

      cluster ((D -multiCat ) . e) -> empty;

      coherence

      proof

        set g = ( MultPlace (D -concatenation )), f = ( {} .--> {} );

         {} in ( dom f) by TARSKI:def 1;

        then

         A1: {} in ( dom f) & {} in (( dom g) \/ ( dom f)) by XBOOLE_0:def 3;

        (D -multiCat ) = (g +* f) by Lm25, FUNCT_4: 34;

        then e = {} & ((D -multiCat ) . {} ) = (f . {} ) by A1, FUNCT_4:def 1;

        hence thesis;

      end;

    end

    registration

      let D;

      cluster -> D -prefix for Subset of (1 -tuples_on D);

      coherence

      proof

        set f = (D -concatenation ), D1 = (1 -tuples_on D);

        let X be Subset of D1;

        now

          let x1,x2,d1,d2 be set;

          assume

           A1: x1 in (X /\ (D * )) & x2 in (X /\ (D * )) & d1 in (D * ) & d2 in (D * );

          then

          reconsider x11 = x1, x22 = x2 as Element of D1;

          reconsider x111 = x11, x222 = x22 as 1 -element FinSequence;

          reconsider x1111 = x11, x2222 = x22 as Element of (D * ) by FINSEQ_2: 142, TARSKI:def 3;

          reconsider xx1 = x1111, xx2 = x2222, dd1 = d1, dd2 = d2 as FinSequence of D by FINSEQ_1:def 11, A1;

          ( len xx1) = 1 & ( len xx2) = 1 by CARD_1:def 7;

          then

           A2: xx1 = <*(xx1 . 1)*> & xx2 = <*(xx2 . 1)*> by FINSEQ_1: 40;

          

           A3: (f . (x1,d1)) = (xx1 ^ dd1) & (f . (x2,d2)) = (xx2 ^ dd2) by Lm10;

          assume

           A4: (f . (x1,d1)) = (f . (x2,d2));

          

           A5: (xx1 . 1) = ((xx1 ^ dd1) . 1) by A2, FINSEQ_1: 41

          .= (xx2 . 1) by A2, A4, A3, FINSEQ_1: 41;

          thus x1 = x2 & d1 = d2 by FINSEQ_1: 33, A5, A2, A4, A3;

        end;

        hence thesis by Def10;

      end;

    end

    theorem :: FOMODEL0:7

    

     Th7: A is D -prefix implies ((D -multiCat ) .: (m -tuples_on A)) is D -prefix

    proof

      reconsider f = (D -concatenation ) as BinOp of (D * );

      set F = (D -multiCat ), Y = (F .: (m -tuples_on A));

       {} in ((D * ) * ) by FINSEQ_1: 49;

      then

       A1: {} in ( dom F) by FUNCT_2:def 1;

      per cases ;

        suppose m = 0 ;

        

        then

         A2: Y = (F .: {( <*> A)}) by FINSEQ_2: 94

        .= ( Im (F, {} ))

        .= {(F . {} )} by FUNCT_1: 59, A1

        .= { {} };

        for x,y,d1,d2 be set st x in (Y /\ (D * )) & y in (Y /\ (D * )) & d1 in (D * ) & d2 in (D * ) & (f . (x,d1)) = (f . (y,d2)) holds (x = y & d1 = d2)

        proof

          let x,y,d1,d2 be set;

          assume

           A3: x in (Y /\ (D * )) & y in (Y /\ (D * )) & d1 in (D * ) & d2 in (D * ) & (f . (x,d1)) = (f . (y,d2));

          then x in Y & x in (D * ) & y in Y & y in (D * ) by XBOOLE_0:def 4;

          then

           A4: x = {} & y = {} by TARSKI:def 1, A2;

          reconsider xx = x as Element of (D * ) by A3;

          reconsider yy = y as Element of (D * ) by A3;

          reconsider d11 = d1 as Element of (D * ) by A3;

          reconsider d22 = d2 as Element of (D * ) by A3;

          d11 = (xx ^ d11) by A4, FINSEQ_1: 34

          .= (f . (yy,d22)) by Lm10, A3

          .= ( {} ^ d22) by A4, Lm10

          .= d22 by FINSEQ_1: 34;

          hence x = y & d1 = d2 by A4;

        end;

        hence thesis by Def10;

      end;

        suppose m <> 0 ;

        then

        consider k be Nat such that

         A5: m = (k + 1) by NAT_1: 6;

        set B = ((k + 1) -tuples_on A);

        B misses ( 0 -tuples_on A) by Lm5;

        then B misses { {} } by Lm6;

        then

         A6: (B \ { {} }) = B by XBOOLE_1: 83;

        assume A is D -prefix;

        then

         A7: (( MultPlace f) .: B) is f -unambiguous by Lm19;

        (F .: B) = ((F | (B \ { {} })) .: (B \ { {} })) by RELAT_1: 129, A6

        .= ((( MultPlace f) | B) .: B) by A6, Lm24

        .= (( MultPlace f) .: B) by RELAT_1: 129;

        hence thesis by A5, A7;

      end;

    end;

    theorem :: FOMODEL0:8

    A is D -prefix implies (D -multiCat ) is (m -tuples_on A) -one-to-one

    proof

      set f = (D -concatenation ), F = (D -multiCat ), Z = (m -tuples_on A);

      assume

       A1: A is D -prefix;

      per cases ;

        suppose m = 0 ;

        

        then Z = ( Funcs (( Seg 0 ),A)) by Lm7

        .= { {} } by FUNCT_5: 57;

        then (F | Z) is one-to-one;

        hence thesis;

      end;

        suppose m <> 0 ;

        then

        consider k be Nat such that

         A2: m = (k + 1) by NAT_1: 6;

        reconsider kk = (k + 1) as Element of NAT by ORDINAL1:def 12;

        set ZZ = (kk -tuples_on A);

        ( MultPlace f) is ZZ -one-to-one by A1, Lm21;

        then

         A3: (( MultPlace f) | ZZ) is one-to-one;

        ( len {} ) = 0 ;

        then not {} in ZZ by FINSEQ_2: 132;

        then { {} } misses ZZ by ZFMISC_1: 50;

        then (ZZ \ { {} }) = ZZ by XBOOLE_1: 83;

        then (F | Z) is one-to-one by Lm24, A3, A2;

        hence thesis;

      end;

    end;

    theorem :: FOMODEL0:9

    ((m + 1) -tuples_on Y) c= ((Y * ) \ { {} })

    proof

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

      

       A1: ( 0 -tuples_on Y) misses (K -tuples_on Y) by Lm5;

      (K -tuples_on Y) c= ((Y * ) \ ( 0 -tuples_on Y)) by FINSEQ_2: 134, XBOOLE_1: 86, A1;

      hence thesis by Lm6;

    end;

    theorem :: FOMODEL0:10

    m is zero implies (m -tuples_on Y) = { {} } by Lm6;

    theorem :: FOMODEL0:11

    (i -tuples_on Y) = ( Funcs (( Seg i),Y)) by Lm7;

    theorem :: FOMODEL0:12

    x in (m -tuples_on A) implies x is FinSequence of A

    proof

      assume

       A1: x in (m -tuples_on A);

      then

      reconsider p = x as m -element FinSequence by FINSEQ_2: 141;

      p in ( Funcs (( Seg m),A)) by A1, Lm7;

      then

      consider f be Function such that

       A2: p = f & ( dom f) = ( Seg m) & ( rng f) c= A by FUNCT_2:def 2;

      thus x is FinSequence of A by A2, FINSEQ_1:def 4;

    end;

    definition

      let A,X be set;

      :: original: chi

      redefine

      func chi (A,X) -> Function of X, BOOLEAN ;

      coherence

      proof

        ( chi (A,X)) is Function of X, { {} , 1} & { {} , 1} = BOOLEAN ;

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:13

    (( MultPlace f) . <*d*>) = d & for x be non empty FinSequence of D holds (( MultPlace f) . (x ^ <*d*>)) = (f . ((( MultPlace f) . x),d)) by Lm15;

    theorem :: FOMODEL0:14

    

     Th14: for d be non empty Element of ((D * ) * ) holds ((D -multiCat ) . d) = (( MultPlace (D -concatenation )) . d)

    proof

      let d be non empty Element of ((D * ) * );

      set f = (D -concatenation ), F = (D -multiCat );

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

      then d in (((D * ) * ) \ { {} }) by XBOOLE_0:def 5;

      

      hence (F . d) = ((F | (((D * ) * ) \ { {} })) . d) by FUNCT_1: 49

      .= (( MultPlace f) . d) by Lm23;

    end;

    theorem :: FOMODEL0:15

    for d1,d2 be Element of (D * ) holds ((D -multiCat ) . <*d1, d2*>) = (d1 ^ d2)

    proof

      let d1,d2 be Element of (D * );

      set F = (D -multiCat ), f = (D -concatenation ), d = <*d1, d2*>;

      reconsider dd = ( <*d1*> ^ <*d2*>) as non empty Element of ((D * ) * );

      

       A1: (F . dd) = (( MultPlace f) . dd) by Th14;

      

      thus (F . d) = (f . ((( MultPlace f) . <*d1*>),d2)) by Lm15, A1

      .= (f . (d1,d2)) by Lm15

      .= (d1 ^ d2) by Lm10;

    end;

    registration

      let f,g be FinSequence;

      cluster <:f, g:> -> FinSequence-like;

      coherence

      proof

        set m = ( len f), n = ( len g), l = ( min (m,n));

        

         A1: l is Nat by TARSKI: 1;

        ( dom <:f, g:>) = ( Seg l) by Lm13;

        hence thesis by A1;

      end;

    end

    registration

      let m;

      let f,g be m -element FinSequence;

      cluster <:f, g:> -> m -element;

      coherence

      proof

        set l = ( min (( len f),( len g)));

        

         A1: ( len f) = m & ( len g) = m by CARD_1:def 7;

        reconsider h = <:f, g:> as FinSequence;

        reconsider ll = l as Element of NAT by ORDINAL1:def 12;

        ( dom h) = ( Seg ll) by Lm13;

        then ( len h) = ll by FINSEQ_1:def 3;

        hence thesis by CARD_1:def 7, A1;

      end;

    end

    registration

      let X,Y be set;

      let f be X -defined Function, g be Y -defined Function;

      cluster <:f, g:> -> (X /\ Y) -defined;

      coherence

      proof

        reconsider F = ( dom f) as Subset of X;

        reconsider G = ( dom g) as Subset of Y;

        set h = <:f, g:>;

        

         A1: ( dom h) = (G /\ F) by FUNCT_3:def 7;

        thus thesis by XBOOLE_1: 27, A1;

      end;

    end

    registration

      let X be set;

      let f,g be X -defined Function;

      cluster <:f, g:> -> X -defined;

      coherence ;

    end

    registration

      let X,Y be set;

      let f be totalX -defined Function, g be totalY -defined Function;

      cluster <:f, g:> -> total;

      coherence

      proof

        reconsider h = <:f, g:> as (X /\ Y) -defined Function;

        ( dom f) = X & ( dom g) = Y by PARTFUN1:def 2;

        then ( dom h) = (X /\ Y) by FUNCT_3:def 7;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let X be set;

      let f,g be totalX -defined Function;

      cluster <:f, g:> -> total;

      coherence ;

    end

    registration

      let X,Y be set;

      let f be X -valued Function, g be Y -valued Function;

      cluster <:f, g:> -> [:X, Y:] -valued;

      coherence

      proof

        set h = <:f, g:>;

        ( rng h) c= [:( rng f), ( rng g):] by FUNCT_3: 51;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    registration

      let D;

      cluster D -valued for FinSequence;

      existence

      proof

        set p = the FinSequence of D;

        take p;

        thus thesis;

      end;

    end

    registration

      let D, m;

      cluster m -elementD -valued for FinSequence;

      existence

      proof

        set p = the m -element FinSequence of D;

        take p;

        thus thesis;

      end;

    end

    registration

      let X,Y be non empty set;

      let f be Function of X, Y;

      let p be X -valued FinSequence;

      cluster (f * p) -> FinSequence-like;

      coherence

      proof

        ( rng p) c= X;

        then

        reconsider pp = p as FinSequence of X by FINSEQ_1:def 4;

        (f * pp) is FinSequence of Y;

        hence thesis;

      end;

    end

    registration

      let X,Y be non empty set;

      let m;

      let f be Function of X, Y;

      let p be m -elementX -valued FinSequence;

      cluster (f * p) -> m -element;

      coherence

      proof

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

        ( rng p) c= X & ( dom f) = X by FUNCT_2:def 1;

        

        then ( dom (f * p)) = ( dom p) by RELAT_1: 27

        .= ( Seg ( len p)) by FINSEQ_1:def 3

        .= ( Seg mm) by CARD_1:def 7;

        then ( len (f * p)) = mm by FINSEQ_1:def 3;

        hence thesis by CARD_1:def 7;

      end;

    end

    definition

      let D, f;

      let p,q be Element of (D * );

      :: FOMODEL0:def13

      func f AppliedPairwiseTo (p,q) -> FinSequence of D equals (f * <:p, q:>);

      coherence

      proof

        ( rng (f * <:p, q:>)) c= D;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    registration

      let D, f, m;

      let p,q be m -element Element of (D * );

      cluster (f AppliedPairwiseTo (p,q)) -> m -element;

      coherence ;

    end

    notation

      let D, f;

      let p,q be Element of (D * );

      synonym f _\ (p,q) for f AppliedPairwiseTo (p,q);

    end

    definition

      :: original: INT

      redefine

      :: FOMODEL0:def14

      func INT equals ( NAT \/ ( [: { 0 }, NAT :] \ { [ 0 , 0 ]}));

      compatibility

      proof

         INT = (( NAT \ { [ 0 , 0 ]}) \/ ( [: { 0 }, NAT :] \ { [ 0 , 0 ]})) by NUMBERS:def 4, XBOOLE_1: 42

        .= ( NAT \/ ( [: { 0 }, NAT :] \ { [ 0 , 0 ]})) by ZFMISC_1: 57, ARYTM_3: 32;

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:16

    

     Th16: for p be FinSequence st p is Y -valued & p is m -element holds p in (m -tuples_on Y)

    proof

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

      let p be FinSequence;

      assume p is Y -valued & p is m -element;

      then ( rng p) c= Y & ( len p) = mm by CARD_1:def 7;

      hence thesis by FINSEQ_2: 132;

    end;

    notation

      let A, B;

      synonym A typed/\ B for A /\ B;

    end

    definition

      let A, B;

      :: original: typed/\

      redefine

      func A typed/\ B -> Subset of A ;

      coherence by XBOOLE_1: 17;

    end

    registration

      let A, B;

      identify B typed/\ A with A typed/\ B;

      compatibility ;

    end

    registration

      let A, B;

      identify A typed/\ B with A /\ B;

      compatibility ;

    end

    definition

      let B,A be object;

      :: FOMODEL0:def15

      func A null B -> set equals A;

      coherence by TARSKI: 1;

    end

    registration

      let A, B;

      reduce (A null B) to A;

      reducibility ;

    end

    registration

      let A;

      let B be Subset of A;

      identify B null A with A /\ B;

      compatibility by XBOOLE_1: 28;

      identify A /\ B with B null A;

      compatibility ;

    end

    registration

      let A, B, C;

      cluster ((B \ A) /\ (A /\ C)) -> empty;

      coherence

      proof

        set X = (B \ A), Y = (A /\ C);

        X misses A & Y c= A by XBOOLE_1: 79;

        hence thesis by XBOOLE_0:def 7, XBOOLE_1: 63;

      end;

    end

    definition

      let A, B;

      :: FOMODEL0:def16

      func A typed\ B -> Subset of A equals (A \ B);

      coherence ;

    end

    registration

      let A, B;

      identify A typed\ B with A \ B;

      compatibility ;

    end

    definition

      let A, B;

      :: FOMODEL0:def17

      func A \typed/ B -> Subset of (A \/ B) equals A;

      coherence by XBOOLE_1: 7;

    end

    registration

      let A, B;

      identify A null B with A \typed/ B;

      compatibility ;

      identify A \typed/ B with A null B;

      compatibility ;

    end

    registration

      let A;

      let B be Subset of A;

      identify A null B with A \/ B;

      compatibility by XBOOLE_1: 12;

      identify A \/ B with A null B;

      compatibility ;

    end

    reserve X for set,

f for Function;

    reserve U1,U2 for non empty set;

    

     Lm26: f c= g implies ( iter (f,m)) c= ( iter (g,m))

    proof

      assume

       A1: f c= g;

      defpred P[ Nat] means ( iter (f,$1)) c= ( iter (g,$1));

      

       A2: P[ 0 ]

      proof

        

         A3: ( iter (f, 0 )) = ( id ( field f)) & ( iter (g, 0 )) = ( id ( field g)) by FUNCT_7: 68;

        ( dom f) c= ( dom g) & ( rng f) c= ( rng g) by RELAT_1: 11, A1;

        then (( dom f) \/ ( rng f)) c= (( dom g) \/ ( rng g)) by XBOOLE_1: 13;

        hence thesis by A3, FUNCT_4: 3;

      end;

      

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

      proof

        let n;

        assume P[n];

        then (f * ( iter (f,n))) c= (g * ( iter (g,n))) by A1, RELAT_1: 31;

        then ( iter (f,(n + 1))) c= (g * ( iter (g,n))) by FUNCT_7: 71;

        hence thesis by FUNCT_7: 71;

      end;

       P[n] from NAT_1:sch 2( A2, A4);

      hence thesis;

    end;

    

     Lm27: (R [*] ) is_transitive_in ( field R)

    proof

      set X = ( field R), S = (R [*] );

      now

        let x,y,z be object;

        assume

         A1: x in X & y in X & z in X;

        assume

         A2: [x, y] in S & [y, z] in S;

        consider p1 be FinSequence such that

         A3: ( len p1) >= 1 & (p1 . 1) = x & (p1 . ( len p1)) = y & for i be Nat st i >= 1 & i < ( len p1) holds [(p1 . i), (p1 . (i + 1))] in R by A2, FINSEQ_1:def 16;

        consider m be Nat such that

         A4: ( len p1) = (m + 1) by NAT_1: 6, A3;

        consider p2 be FinSequence such that

         A5: ( len p2) >= 1 & (p2 . 1) = y & (p2 . ( len p2)) = z & for i be Nat st i >= 1 & i < ( len p2) holds [(p2 . i), (p2 . (i + 1))] in R by A2, FINSEQ_1:def 16;

        

         A6: 1 in ( dom p2) by FINSEQ_3: 25, A5;

        reconsider l1 = ( len p1), l2 = ( len p2) as non zero Nat by A3, A5;

        reconsider p11 = (p1 | ( Seg m)) as FinSequence;

        set p = (p11 ^ p2);

        

         A7: (m + 0 ) < (m + 1) by XREAL_1: 8;

        

         A8: ( len p11) = m by A7, A4, FINSEQ_1: 17;

        

         A9: (m + l2) >= ( 0 + 1) by A5, XREAL_1: 7;

        

         A10: n >= 1 & n <= ( len p2) implies (p . (m + n)) = (p2 . n)

        proof

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

          assume n >= 1 & n <= ( len p2);

          then n in ( Seg ( len p2));

          then n in ( dom p2) by FINSEQ_1:def 3;

          hence thesis by FINSEQ_1:def 7, A8;

        end;

        

         A11: (p . 1) = x

        proof

          per cases ;

            suppose

             A12: m = 0 ;

            thus (p . 1) = x by A12, A4, A3, A10, A5;

          end;

            suppose m <> 0 ;

            then ( 0 + 1) <= m by INT_1: 7;

            then 1 in ( Seg m);

            then

             A13: 1 in ( dom p11) by A7, A4, FINSEQ_1: 17;

            

            hence (p . 1) = (p11 . 1) by FINSEQ_1:def 7

            .= x by A3, FUNCT_1: 47, A13;

          end;

        end;

        l2 in ( Seg l2) by A5;

        then l2 in ( dom p2) by FINSEQ_1:def 3;

        then

         A14: (p . (( len p11) + ( len p2))) = z by FINSEQ_1:def 7, A5;

        

         A15: for i be Nat st i >= 1 & i < ( len p) holds [(p . i), (p . (i + 1))] in R

        proof

          let i be Nat;

          assume

           A16: i >= 1 & i < ( len p);

          then

           A17: (i + 1) >= 1 & i >= 1 & i < ( len p) by NAT_1: 11;

          per cases by XXREAL_0: 1;

            suppose i < m;

            then

             A18: i < l1 & i < m & (i + 1) <= m by INT_1: 7, A7, A4, XXREAL_0: 2;

            then i in ( Seg m) & (i + 1) in ( Seg m) by A17;

            then

             A19: i in ( dom p11) & (i + 1) in ( dom p11) by A7, A4, FINSEQ_1: 17;

            then (p . i) = (p11 . i) & (p . (i + 1)) = (p11 . (i + 1)) by FINSEQ_1:def 7;

            then (p . i) = (p1 . i) & (p . (i + 1)) = (p1 . (i + 1)) by A19, FUNCT_1: 47;

            hence [(p . i), (p . (i + 1))] in R by A3, A16, A18;

          end;

            suppose

             A20: i = m;

            

             A21: m in ( dom p11) by A20, A16, A8, FINSEQ_3: 25;

            

            then

             A22: (p . m) = (p11 . m) by FINSEQ_1:def 7

            .= (p1 . m) by FUNCT_1: 47, A21;

            

             A23: (p . (m + 1)) = (p1 . (m + 1)) by A3, A6, A4, A8, FINSEQ_1:def 7, A5;

            thus [(p . i), (p . (i + 1))] in R by A20, A22, A23, A3, A16, A7, A4;

          end;

            suppose

             A24: i > m;

            then

            consider j be Nat such that

             A25: i = (m + j) by NAT_1: 10;

            j <> 0 by A24, A25;

            then

             A26: j >= ( 0 + 1) by INT_1: 7;

            then

             A27: j >= 1 & (j + 1) >= (1 + 0 ) by XREAL_1: 7;

            (m + j) < (m + l2) by A25, A16, A8, FINSEQ_1: 22;

            then

             A28: j < l2 by XREAL_1: 7;

            then

             A29: j <= l2 & (j + 1) <= l2 by INT_1: 7;

            j in ( Seg l2) & (j + 1) in ( Seg l2) by A29, A27;

            then

             A30: j in ( dom p2) & (j + 1) in ( dom p2) by FINSEQ_1:def 3;

            

             A31: (p . i) = (p2 . j) by FINSEQ_1:def 7, A30, A25, A8;

            

             A32: (p . (i + 1)) = (p . (( len p11) + (j + 1))) by A25, A8

            .= (p2 . (j + 1)) by FINSEQ_1:def 7, A30;

            thus [(p . i), (p . (i + 1))] in R by A31, A32, A5, A28, A26;

          end;

        end;

        x in X & z in X & ( len p) >= 1 & (p . 1) = x & (p . ( len p)) = z & for i be Nat st i >= 1 & i < ( len p) holds [(p . i), (p . (i + 1))] in R by A1, A9, A8, FINSEQ_1: 22, A11, A14, A15;

        hence [x, z] in S by FINSEQ_1:def 16;

      end;

      hence thesis by RELAT_2:def 8;

    end;

    

     Lm28: ( field (R [*] )) c= ( field R)

    proof

      set RR = (R [*] ), LH = ( field RR), RH = ( field R);

      let x be object;

      assume

       A1: x in LH;

      per cases by A1, XBOOLE_0:def 3;

        suppose x in ( dom RR);

        then

        consider y be object such that

         A2: [x, y] in RR by XTUPLE_0:def 12;

        thus x in RH by A2, FINSEQ_1:def 16;

      end;

        suppose x in ( rng RR);

        then

        consider y be object such that

         A3: [y, x] in RR by XTUPLE_0:def 13;

        thus x in RH by FINSEQ_1:def 16, A3;

      end;

    end;

    

     Lm29: (R [*] ) is_reflexive_in ( field R)

    proof

      set RR = (R [*] ), X = ( field R);

      now

        let x be object;

        reconsider p = <*x*> as 1 -element FinSequence;

        ( len p) = 1 & (p . 1) = x by FINSEQ_1: 40;

        then

         A1: ( len p) >= 1 & (p . 1) = x & (p . ( len p)) = x & for i st i >= 1 & i < ( len p) holds [(p . i), (p . (i + 1))] in R;

        assume x in X;

        hence [x, x] in RR by A1, FINSEQ_1:def 16;

      end;

      hence thesis by RELAT_2:def 1;

    end;

    

     Lm30: ( field (R [*] )) = ( field R) by LANG1: 18, RELAT_1: 16, Lm28;

    registration

      let R be Relation;

      cluster (R [*] ) -> transitive;

      coherence

      proof

        (R [*] ) is_transitive_in ( field R) by Lm27;

        then (R [*] ) is_transitive_in ( field (R [*] )) by Lm30;

        hence thesis by RELAT_2:def 16;

      end;

      cluster (R [*] ) -> reflexive;

      coherence

      proof

        (R [*] ) is_reflexive_in ( field R) by Lm29;

        then (R [*] ) is_reflexive_in ( field (R [*] )) by Lm30;

        hence thesis by RELAT_2:def 9;

      end;

    end

    

     Lm31: ( iter (f, 0 )) c= (f [*] )

    proof

      set LH = ( iter (f, 0 )), RH = (f [*] );

      LH = ( id ( field f)) by FUNCT_7: 68

      .= ( id ( field RH)) by Lm30;

      hence thesis by RELAT_2: 1;

    end;

    

     Lm32: ( iter (f,(m + 1))) c= (f [*] )

    proof

      set RH = (f [*] );

      defpred P[ Nat] means ( iter (f,($1 + 1))) c= RH;

      

       A1: P[ 0 ]

      proof

        

         A2: ( iter (f,1)) = f by FUNCT_7: 70;

        thus thesis by LANG1: 18, A2;

      end;

      

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

      proof

        let n;

        assume P[n];

        then ( iter (f,(n + 1))) c= RH & f c= RH by LANG1: 18;

        then

         A4: (( iter (f,(n + 1))) * f) c= (RH * RH) by RELAT_1: 31;

        (RH * RH) c= RH by RELAT_2: 27;

        then (( iter (f,(n + 1))) * f) c= RH by A4;

        hence thesis by FUNCT_7: 69;

      end;

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

      hence thesis;

    end;

    

     Lm33: ( iter (f,m)) c= (f [*] )

    proof

      per cases ;

        suppose m = 0 ;

        hence thesis by Lm31;

      end;

        suppose m <> 0 ;

        then

        consider n such that

         A1: m = (n + 1) by NAT_1: 6;

        thus thesis by Lm32, A1;

      end;

    end;

    

     Lm34: (( rng f) c= ( dom f) & x in ( dom f) & (g . 0 ) = x & for i st i < m holds (g . (i + 1)) = (f . (g . i))) implies (g . m) = (( iter (f,m)) . x)

    proof

      assume

       A1: ( rng f) c= ( dom f) & x in ( dom f);

      then

       A2: x in (( dom f) \/ ( rng f)) by XBOOLE_0:def 3;

      defpred P[ Nat] means ((g . 0 ) = x & for i st i < $1 holds (g . (i + 1)) = (f . (g . i))) implies (g . $1) = (( iter (f,$1)) . x);

      

       A3: P[ 0 ]

      proof

        ( field f) = (( dom f) \/ ( rng f));

        then

         A4: ( iter (f, 0 )) = ( id (( dom f) \/ ( rng f))) by FUNCT_7: 68;

        assume (g . 0 ) = x & for i st i < 0 holds (g . (i + 1)) = (f . (g . i));

        hence thesis by A4, FUNCT_1: 17, A2;

      end;

      

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

      proof

        let n;

        assume

         A6: P[n];

        assume

         A7: (g . 0 ) = x;

        assume

         A8: for i st i < (n + 1) holds (g . (i + 1)) = (f . (g . i));

        

         A9: for i st i < n holds (g . (i + 1)) = (f . (g . i))

        proof

          let i;

          assume i < n;

          then (i + 0 ) < (n + 1) by XREAL_1: 8;

          hence thesis by A8;

        end;

        

         A10: x in ( dom ( iter (f,n))) by A1, FUNCT_7: 74;

        (n + 0 ) < (n + 1) by XREAL_1: 8;

        

        then (g . (n + 1)) = (f . (g . n)) by A8

        .= ((f * ( iter (f,n))) . x) by A10, FUNCT_1: 13, A9, A6, A7

        .= (( iter (f,(n + 1))) . x) by FUNCT_7: 71;

        hence thesis;

      end;

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

      hence thesis;

    end;

    definition

      :: FOMODEL0:def18

      func plus -> Function of COMPLEX , COMPLEX means

      : Def18: for z be Complex holds (it . z) = (z + 1);

      existence

      proof

        defpred P[ set, set] means for z be Complex st z = $1 holds $2 = (z + 1);

        

         A1: for x be Element of COMPLEX holds ex zz be Element of COMPLEX st P[x, zz]

        proof

          let x be Element of COMPLEX ;

          reconsider z0 = x as Complex;

          reconsider z1 = (z0 + 1) as Element of COMPLEX by XCMPLX_0:def 2;

          take z1;

          thus P[x, z1];

        end;

        consider f be Function of COMPLEX , COMPLEX such that

         A2: for x be Element of COMPLEX holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        now

          let z be Complex;

          reconsider zz = z as Element of COMPLEX by XCMPLX_0:def 2;

          z = zz & P[zz, (f . zz)] by A2;

          hence (f . z) = (z + 1);

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function of COMPLEX , COMPLEX ;

        assume

         A3: for z be Complex holds (IT1 . z) = (z + 1);

        assume

         A4: for z be Complex holds (IT2 . z) = (z + 1);

        now

          let zz be Element of COMPLEX ;

          

          thus (IT1 . zz) = (zz + 1) by A3

          .= (IT2 . zz) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    

     Lm35: (( rng f) c= ( dom f) & x in ( dom f) & (p . 1) = x & for i st i >= 1 & i < (m + 1) holds (p . (i + 1)) = (f . (p . i))) implies (p . (m + 1)) = (( iter (f,m)) . x)

    proof

      

       A1: ( dom plus ) = COMPLEX by FUNCT_2:def 1;

      then

      reconsider Z = 0 as Element of ( dom plus ) by XCMPLX_0:def 2;

      reconsider g = (p * plus ) as Function;

      

       A2: for z be Complex holds (g . z) = (p . (z + 1))

      proof

        let z be Complex;

        reconsider zz = z as Element of ( dom plus ) by XCMPLX_0:def 2, A1;

        

        thus (g . z) = (p . ( plus . zz)) by FUNCT_1: 13

        .= (p . (z + 1)) by Def18;

      end;

      assume

       A3: ( rng f) c= ( dom f) & x in ( dom f);

      assume (p . 1) = x;

      then (p . ( 0 + 1)) = x;

      then

       A4: (g . 0 ) = x by A2;

      assume

       A5: for i st i >= 1 & i < (m + 1) holds (p . (i + 1)) = (f . (p . i));

      now

        let j be Nat;

        reconsider jz = j as Complex;

        assume j < m;

        then (j + 1) >= ( 0 + 1) & (j + 1) < (m + 1) by XREAL_1: 7, XREAL_1: 8;

        

        then (p . ((j + 1) + 1)) = (f . (p . (j + 1))) by A5

        .= (f . (g . j)) by A2;

        hence (g . (j + 1)) = (f . (g . j)) by A2;

      end;

      then (g . m) = (( iter (f,m)) . x) by Lm34, A4, A3;

      hence (p . (m + 1)) = (( iter (f,m)) . x) by A2;

    end;

    

     Lm36: z in (f [*] ) & ( rng f) c= ( dom f) implies ex n st z in ( iter (f,n))

    proof

      set LH = (f [*] );

      assume

       A1: z in LH;

      then

      consider x,y be object such that

       A2: z = [x, y] by RELAT_1:def 1;

      consider p be FinSequence such that

       A3: ( len p) >= 1 & (p . 1) = x & (p . ( len p)) = y & for i be Nat st i >= 1 & i < ( len p) holds [(p . i), (p . (i + 1))] in f by A2, A1, FINSEQ_1:def 16;

      assume

       A4: ( rng f) c= ( dom f);

      then

       A5: ( field f) = ( dom f) & x in ( field f) by A2, A1, FINSEQ_1:def 16, XBOOLE_1: 12;

      consider m be Nat such that

       A6: (m + 1) = ( len p) by A3, NAT_1: 6;

      take m;

      for i st i >= 1 & i < ( len p) holds (p . i) in ( dom f) & (p . (i + 1)) = (f . (p . i))

      proof

        let i;

        assume i >= 1 & i < ( len p);

        then

         A7: [(p . i), (p . (i + 1))] in f by A3;

        hence (p . i) in ( dom f) by XTUPLE_0:def 12;

        hence (p . (i + 1)) = (f . (p . i)) by FUNCT_1:def 2, A7;

      end;

      then

       A8: (m + 1) >= 1 & (p . 1) = x & (p . (m + 1)) = y & for i be Nat st i >= 1 & i < (m + 1) holds (p . (i + 1)) = (f . (p . i)) by A3, A6;

      x in ( dom ( iter (f,m))) & (p . (m + 1)) = (( iter (f,m)) . x) by A5, A4, A8, Lm35, FUNCT_7: 74;

      hence z in ( iter (f,m)) by A2, A3, A6, FUNCT_1: 1;

    end;

    

     Lm37: ( rng f) c= ( dom f) implies (f [*] ) = ( union the set of all ( iter (f,mm)) where mm be Element of NAT )

    proof

      set F = the set of all ( iter (f,mm)) where mm be Element of NAT ;

      set LH = (f [*] ), RH = ( union F);

      now

        let x be object;

        assume x in RH;

        then

        consider X be set such that

         A1: x in X & X in F by TARSKI:def 4;

        consider mm be Element of NAT such that

         A2: X = ( iter (f,mm)) by A1;

        x in ( iter (f,mm)) & ( iter (f,mm)) c= (f [*] ) by A1, A2, Lm33;

        hence x in LH;

      end;

      then

       A3: RH c= LH;

      assume

       A4: ( rng f) c= ( dom f);

      now

        let x be object;

        assume x in LH;

        then

        consider m such that

         A5: x in ( iter (f,m)) by A4, Lm36;

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

        x in ( iter (f,mm)) & ( iter (f,mm)) in F by A5;

        hence x in RH by TARSKI:def 4;

      end;

      then

       A6: LH c= RH;

      thus thesis by A3, A6;

    end;

    theorem :: FOMODEL0:17

    ( rng f) c= ( dom f) implies (f [*] ) = ( union the set of all ( iter (f,mm)) where mm be Element of NAT ) by Lm37;

    theorem :: FOMODEL0:18

    f c= g implies ( iter (f,m)) c= ( iter (g,m)) by Lm26;

    registration

      let X be functional set;

      cluster ( union X) -> Relation-like;

      coherence

      proof

        now

          let x be object;

          assume x in ( union X);

          then

          consider Y such that

           A1: x in Y & Y in X by TARSKI:def 4;

          thus ex y,z be object st x = [y, z] by A1, RELAT_1:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:19

    Y c= ( Funcs (A,B)) implies ( union Y) c= [:A, B:] by Lm2;

    registration

      let Y;

      let R be Y -valued Relation;

      identify R null Y with Y |` R;

      compatibility ;

    end

    registration

      let Y;

      cluster (Y \ Y) -> empty;

      coherence by XBOOLE_1: 37;

    end

    registration

      let D, d;

      cluster ( {(( id D) . d)} \ {d}) -> empty;

      coherence ;

    end

    registration

      let p be FinSequence, q be empty FinSequence;

      identify p null q with p ^ q;

      compatibility by FINSEQ_1: 34;

      identify p ^ q with p null q;

      compatibility ;

      identify p null q with q ^ p;

      compatibility by FINSEQ_1: 34;

      identify q ^ p with p null q;

      compatibility ;

    end

    registration

      let Y;

      let R be Y -defined Relation;

      identify R null Y with R | Y;

      compatibility ;

      identify R | Y with R null Y;

      compatibility ;

    end

    theorem :: FOMODEL0:20

    

     Th20: f = { [x, (f . x)] where x be Element of ( dom f) : x in ( dom f) }

    proof

      set RH = { [x, (f . x)] where x be Element of ( dom f) : x in ( dom f) };

      now

        let z be object;

        assume

         A1: z in f;

        then

        consider x,y be object such that

         A2: z = [x, y] by RELAT_1:def 1;

        reconsider xx = x as Element of ( dom f) by FUNCT_1: 1, A2, A1;

        z = [xx, (f . xx)] & xx in ( dom f) by A2, FUNCT_1: 1, A1;

        hence z in RH;

      end;

      then

       A3: f c= RH;

      now

        let z be object;

        assume

         A4: z in RH;

        consider x be Element of ( dom f) such that

         A5: z = [x, (f . x)] & x in ( dom f) by A4;

        thus z in f by A5, FUNCT_1: 1;

      end;

      then RH c= f;

      hence thesis by A3;

    end;

    theorem :: FOMODEL0:21

    

     Th21: for R be totalY -defined Relation holds ( id Y) c= (R * (R ~ ))

    proof

      set X = Y;

      let R be totalX -defined Relation;

      reconsider f = ( id X) as Function;

      

       A1: f = { [x, (f . x)] where x be Element of ( dom f) : x in ( dom f) } by Th20;

      now

        let z be object;

        assume z in f;

        then

        consider x be Element of ( dom f) such that

         A2: z = [x, (( id X) . x)] & x in ( dom ( id X)) by A1;

        x in ( dom R) by A2, PARTFUN1:def 2;

        then

        consider y be object such that

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

         [y, x] in (R ~ ) by A3, RELAT_1:def 7;

        then [x, x] in (R * (R ~ )) by A3, RELAT_1:def 8;

        hence z in (R * (R ~ )) by A2;

      end;

      hence thesis;

    end;

    theorem :: FOMODEL0:22

    ((m + n) -tuples_on D) = ((D -concatenation ) .: [:(m -tuples_on D), (n -tuples_on D):])

    proof

      reconsider m, n as Element of NAT by ORDINAL1:def 12;

      set U = D, LH = ((m + n) -tuples_on U), M = (m -tuples_on U), N = (n -tuples_on U), C = (U -concatenation ), RH = (C .: [:M, N:]);

      

       A1: LH = the set of all (z ^ t) where z be Tuple of m, U, t be Tuple of n, U by FINSEQ_2: 105;

      

       A2: ( dom C) = [:(U * ), (U * ):] by FUNCT_2:def 1;

      

       A3: M c= (U * ) & N c= (U * ) by FINSEQ_2: 134;

      now

        let y be object;

        assume y in LH;

        then

        consider Tz be Tuple of m, U, Tt be Tuple of n, U such that

         A4: y = (Tz ^ Tt) by A1;

        reconsider zz = Tz as Element of M by FINSEQ_2: 131;

        reconsider tt = Tt as Element of N by FINSEQ_2: 131;

        reconsider x = [zz, tt] as Element of [:M, N:];

        reconsider xx = x as Element of ( dom C) by A2, A3, ZFMISC_1: 96, TARSKI:def 3;

        

         A5: (C .: {x}) c= RH by RELAT_1: 123;

        y = (C . (Tz,Tt)) by A4, Lm10

        .= (C . x);

        then y in {(C . xx)} by TARSKI:def 1;

        then y in ( Im (C,xx)) by FUNCT_1: 59;

        hence y in RH by A5;

      end;

      then

       A6: LH c= RH;

      now

        let y be object;

        assume y in RH;

        then

        consider x be object such that

         A7: x in ( dom C) & x in [:M, N:] & y = (C . x) by FUNCT_1:def 6;

        consider z,t be object such that

         A8: z in M & t in N & x = [z, t] by ZFMISC_1:def 2, A7;

        reconsider zz = z as Element of M by A8;

        reconsider tt = t as Element of N by A8;

        reconsider zzz = zz, ttt = tt as FinSequence of U;

        reconsider Tz = zz as Tuple of m, U;

        reconsider Tt = tt as Tuple of n, U;

        y = (C . (zzz,ttt)) by A7, A8

        .= (Tz ^ Tt) by Lm10;

        hence y in LH by A1;

      end;

      then RH c= LH;

      hence thesis by A6;

    end;

    theorem :: FOMODEL0:23

    

     Th23: for P,Q be Relation holds ((P \/ Q) " Y) = ((P " Y) \/ (Q " Y))

    proof

      let P,Q be Relation;

      set R = (P \/ Q), LH = (R " Y), RH = ((P " Y) \/ (Q " Y));

      reconsider PP = (P null Q), QQ = (Q null P) as Subset of R;

      now

        let x be object;

        assume x in LH;

        then

        consider y be object such that

         A1: [x, y] in R & y in Y by RELAT_1:def 14;

        set z = [x, y];

        (z in P & y in Y) or (z in Q & y in Y) by XBOOLE_0:def 3, A1;

        then x in (P " Y) or x in (Q " Y) by RELAT_1:def 14;

        hence x in RH by XBOOLE_0:def 3;

      end;

      then

       A2: LH c= RH;

      reconsider PX = (PP " Y), QX = (QQ " Y) as Subset of LH by RELAT_1: 144;

      (PX \/ QX) c= LH;

      hence thesis by A2;

    end;

    

     Lm38: ( chi (A,B)) = ((B --> 0 ) +* ((A /\ B) --> 1))

    proof

      set f = (B --> 0 ), g = ((A /\ B) --> 1), IT = (f +* g);

      

       A1: ( dom f) = B & ( dom g) = (A /\ B) & ( dom IT) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

      now

        let x be object;

        assume

         A2: x in B;

        then

         A3: x in B & x in ( dom IT) & x in (( dom f) \/ ( dom g)) by XBOOLE_1: 22, A1;

        thus x in A implies (IT . x) = 1

        proof

          assume

           A4: x in A;

          then

           A5: x in (A /\ B) by A2, XBOOLE_0:def 4;

          x in ( dom g) by A4, A2, XBOOLE_0:def 4;

          

          then (IT . x) = (g . x) by A3, FUNCT_4:def 1

          .= 1 by FUNCOP_1: 7, A5;

          hence thesis;

        end;

        thus not x in A implies (IT . x) = {}

        proof

          assume not x in A;

          then not x in (A /\ B);

          then not x in ( dom g);

          

          then (IT . x) = (f . x) by A3, FUNCT_4:def 1

          .= 0 by FUNCOP_1: 7, A2;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_3:def 3, XBOOLE_1: 22, A1;

    end;

    

     Lm39: ( chi (A,B)) = (((B \ A) --> 0 ) +* ((A /\ B) --> 1))

    proof

      set Z = (B \ A), O = (A /\ B), f = (B --> 0 ), g = (O --> 1), IT = ( chi (A,B));

      reconsider BB = (B /\ B), OO = O, ZZ = Z as Subset of B;

      reconsider OOO = (O /\ O) as Subset of O;

      

       A1: (O \/ Z) = B & ( dom IT) = BB by XBOOLE_1: 51, FUNCT_3:def 3;

      

       A2: (B /\ OO) = OO & (Z /\ O) = {} & (B /\ ZZ) = ZZ;

      

       A3: ((f +* g) | Z) = ((f | Z) +* (g | Z)) & ((f +* g) | O) = ((f | O) +* (g | O)) by FUNCT_4: 71;

      

       A4: (f | Z) = ((B /\ Z) --> 0 ) & (g | Z) = ( {} --> 1) & (f | O) = (OOO --> 0 ) & (g | O) = g by FUNCOP_1: 12, A2;

      then ( dom (f | O)) = OOO & ( dom (g | O)) = O;

      then

       A5: ((f | O) +* (g | O)) = (g | O) by FUNCT_4: 19;

      

      thus IT = ((IT | Z) +* (IT | O)) by FUNCT_4: 70, A1

      .= (((f +* g) | Z) +* (IT | O)) by Lm38

      .= ((((B /\ Z) --> 0 ) +* {} ) +* (g | O)) by A3, Lm38, A4, A5

      .= ((Z --> 0 ) +* g);

    end;

    

     Lm40: ( chi (A,B)) = (((B \ A) --> 0 ) \/ ((A /\ B) --> 1))

    proof

      set f = ((B \ A) --> 0 ), g = ((A /\ B) --> 1);

      ((B \ A) /\ (A /\ B)) = {} ;

      then f tolerates g by FUNCOP_1: 87, XBOOLE_0:def 7;

      then (f +* g) = (f \/ g) by FUNCT_4: 30;

      hence thesis by Lm39;

    end;

    theorem :: FOMODEL0:24

    (( chi (A,B)) " { 0 }) = (B \ A) & (( chi (A,B)) " {1}) = (A /\ B)

    proof

      set f = ((B \ A) --> 0 ), g = ((A /\ B) --> 1), IT = ( chi (A,B));

      

       A1: 0 in { 0 } & 1 in {1} & not 1 in { 0 } & not 0 in {1} by TARSKI:def 1;

      

       A2: (f " {1}) = {} & (g " { 0 }) = {} by A1, FUNCOP_1: 16;

      

      thus (IT " { 0 }) = ((f \/ g) " { 0 }) by Lm40

      .= ((f " { 0 }) \/ (g " { 0 })) by Th23

      .= (B \ A) by A1, FUNCOP_1: 14, A2;

      

      thus (IT " {1}) = ((f \/ g) " {1}) by Lm40

      .= ((f " {1}) \/ (g " {1})) by Th23

      .= (A /\ B) by A1, FUNCOP_1: 14, A2;

    end;

    theorem :: FOMODEL0:25

    for y be non empty set holds (y = (f . x) iff x in (f " {y}))

    proof

      let y be non empty set;

      thus y = (f . x) implies x in (f " {y})

      proof

        assume y = (f . x);

        then x in ( dom f) & (f . x) in {y} by FUNCT_1:def 2, TARSKI:def 1;

        hence thesis by FUNCT_1:def 7;

      end;

      assume x in (f " {y});

      then x in ( dom f) & (f . x) in {y} by FUNCT_1:def 7;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FOMODEL0:26

    f is Y -valued & f is FinSequence-like implies f is FinSequence of Y by Lm1;

    registration

      let Y;

      let X be Subset of Y;

      cluster X -valued -> Y -valued for Relation;

      coherence by XBOOLE_1: 1;

    end

    

     Lm41: for R be totalY -defined Relation holds ex f be Function of Y, ( rng R) st f c= R & ( dom f) = Y

    proof

      set X = Y;

      let R be totalX -defined Relation;

      

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

      defpred P[ object, object] means [$1, $2] in R;

      

       A2: for x be object st x in X holds ex y be object st P[x, y] by XTUPLE_0:def 12, A1;

      consider f such that

       A3: ( dom f) = X & for x be object st x in X holds P[x, (f . x)] from CLASSES1:sch 1( A2);

      

       A4: f = { [x, (f . x)] where x be Element of ( dom f) : x in ( dom f) } by Th20;

       A5:

      now

        let z be object;

        assume z in f;

        then

        consider x be Element of ( dom f) such that

         A6: z = [x, (f . x)] & x in ( dom f) by A4;

        thus z in R by A6, A3;

      end;

      then f c= R;

      then ( rng f) c= ( rng R) by RELAT_1: 11;

      then

      reconsider g = f as Function of X, ( rng R) by A3, RELSET_1: 4, FUNCT_2: 67;

      take g;

      thus thesis by A5, A3;

    end;

    

     Lm42: (( dom f) c= ( dom R) & R c= f) implies R = f

    proof

      set X = ( dom f);

      assume

       A1: X c= ( dom R) & R c= f;

      then

       A2: X c= ( dom R) & ( dom R) c= X by RELAT_1: 11;

      reconsider RR = R as X -defined Relation by RELAT_1:def 18, A1, RELAT_1: 11;

      reconsider P = RR as totalX -defined Relation by PARTFUN1:def 2, A2, XBOOLE_0:def 10;

      consider g be Function of X, ( rng P) such that

       A3: g c= P & ( dom g) = X by Lm41;

      f c= R by GRFUNC_1: 3, A3, A1, XBOOLE_1: 1;

      hence thesis by A1;

    end;

    

     Lm43: for Q be Y -defined Relation st Q is total & R is Y -defined & (((P * Q) * (Q ~ )) * R) is Function-like & ( rng P) c= ( dom R) holds (((P * Q) * (Q ~ )) * R) = (P * R)

    proof

      let Q be Y -defined Relation;

      assume Q is total;

      then

      reconsider QQ = Q as totalY -defined Relation;

      set tQ = (QQ ~ );

      assume R is Y -defined;

      then

      reconsider RR = R as Y -defined Relation;

      assume (((P * Q) * (Q ~ )) * R) is Function-like;

      then

      reconsider f = (((P * Q) * tQ) * R) as Function;

      

       A1: f = ((P * Q) * (tQ * R)) by RELAT_1: 36

      .= (P * (Q * (tQ * R))) by RELAT_1: 36

      .= (P * ((Q * tQ) * RR)) by RELAT_1: 36;

      (( id Y) * RR) c= ((Q * tQ) * RR) by RELAT_1: 30, Th21;

      then

       A2: (RR | Y) c= ((Q * tQ) * RR) by RELAT_1: 65;

      assume ( rng P) c= ( dom R);

      then

       A3: ( dom (P * R)) = ( dom P) by RELAT_1: 27;

      ( dom (P * (Q * tQ))) c= ( dom P) & ( dom (((P * Q) * tQ) * R)) c= ( dom ((P * Q) * tQ)) by RELAT_1: 25;

      then ( dom ((P * Q) * tQ)) c= ( dom P) & ( dom f) c= ( dom ((P * Q) * tQ)) by RELAT_1: 36;

      then ( dom f) c= ( dom (P * R)) by A3;

      hence thesis by A2, A1, RELAT_1: 29, Lm42;

    end;

    registration

      let A, U;

      cluster quasi_total -> total for Relation of A, U;

      coherence ;

    end

    theorem :: FOMODEL0:27

    for Q be quasi_total Relation of B, U1, R be quasi_total Relation of B, U2, P be Relation of A, B st (((P * Q) * (Q ~ )) * R) is Function-like holds (((P * Q) * (Q ~ )) * R) = (P * R)

    proof

      let Q be quasi_total Relation of B, U1;

      let R be quasi_total Relation of B, U2;

      let P be Relation of A, B;

      reconsider QQ = Q as totalB -defined Relation;

      reconsider RR = R as totalB -defined Relation;

      

       A1: ( dom R) = B & ( rng P) c= B by PARTFUN1:def 2;

      assume (((P * Q) * (Q ~ )) * R) is Function-like;

      hence thesis by A1, Lm43;

    end;

    theorem :: FOMODEL0:28

    for p,q be FinSequence st p is non empty holds ((p ^ q) . 1) = (p . 1)

    proof

      let p,q be FinSequence;

      assume p is non empty;

      then

      reconsider p as non empty FinSequence;

      set n = ( len p);

      1 <= 1 & 1 <= n by NAT_1: 14;

      then 1 in ( Seg n);

      then 1 in ( dom p) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 7;

    end;

    registration

      let U;

      let p,q be U -valued FinSequence;

      cluster (p ^ q) -> U -valued;

      coherence

      proof

        reconsider pp = p, qq = q as FinSequence of U by Lm1;

        (pp ^ qq) is U -valued;

        hence thesis;

      end;

    end

    definition

      let X be set;

      :: original: FinSequence

      redefine

      mode FinSequence of X -> Element of (X * ) ;

      coherence by FINSEQ_1:def 11;

    end

    definition

      let U, X;

      :: original: -prefix

      redefine

      :: FOMODEL0:def19

      attr X is U -prefix means for p1,q1,p2,q2 be U -valued FinSequence st p1 in X & p2 in X & (p1 ^ q1) = (p2 ^ q2) holds (p1 = p2 & q1 = q2);

      compatibility

      proof

        set f = (U -concatenation ), D = (U * );

        defpred Q[ set] means $1 is FinSequence of U;

        defpred P[] means for p1,q1,p2,q2 be U -valued FinSequence st p1 in X & p2 in X & (p1 ^ q1) = (p2 ^ q2) holds (p1 = p2 & q1 = q2);

        thus X is U -prefix implies P[]

        proof

          assume X is U -prefix;

          then

           A1: X is f -unambiguous;

          let p1,q1,p2,q2 be U -valued FinSequence;

          

           A2: Q[p1] & Q[p2] & Q[q1] & Q[q2] by Lm1;

          assume p1 in X & p2 in X;

          then

           A3: p1 in (X /\ D) & p2 in (X /\ D) & q1 in (U * ) & q2 in (U * ) by A2, XBOOLE_0:def 4;

          assume (p1 ^ q1) = (p2 ^ q2);

          

          then (f . (p1,q1)) = (p2 ^ q2) by Th4

          .= (f . (p2,q2)) by Th4;

          hence p1 = p2 & q1 = q2 by A1, A3;

        end;

        assume

         A4: P[];

        now

          let x1,x2,d1,d2 be set;

          assume

           A5: x1 in (X /\ D) & x2 in (X /\ D) & d1 in D & d2 in D;

          then

          reconsider x11 = x1, x22 = x2, d11 = d1, d22 = d2 as Element of D;

          assume (f . (x1,d1)) = (f . (x2,d2));

          

          then (x11 ^ d11) = (f . (x22,d22)) by Th4

          .= (x22 ^ d22) by Th4;

          hence x1 = x2 & d1 = d2 by A4, A5;

        end;

        hence thesis by Def10;

      end;

    end

    registration

      let X be set;

      cluster -> X -valued for Element of (X * );

      coherence ;

    end

    registration

      let U, m;

      let X be U -prefix set;

      cluster ((U -multiCat ) .: (m -tuples_on X)) -> U -prefix;

      coherence by Th7;

    end

    theorem :: FOMODEL0:29

    

     Th29: ((X \+\ Y) = {} iff X = Y) & ((X \ Y) = {} iff X c= Y) & for x be object holds (( {x} \ Y) = {} iff x in Y)

    proof

      set Z = (X \+\ Y), Z1 = (X \ Y), Z2 = (Y \ X);

      thus Z = {} implies X = Y

      proof

        assume Z = {} ;

        then Z1 = {} & Z2 = {} ;

        then X c= Y & Y c= X by XBOOLE_1: 37;

        hence thesis;

      end;

      thus X = Y implies Z = {} ;

      thus (X \ Y) = {} iff X c= Y by XBOOLE_1: 37;

      thus thesis by ZFMISC_1: 60;

    end;

    registration

      let P;

      cluster (P \ [:( dom P), ( rng P):]) -> empty;

      coherence by RELAT_1: 7, Th29;

    end

    registration

      let X,Y,Z be set;

      cluster (((X \/ Y) \/ Z) \+\ (X \/ (Y \/ Z))) -> empty;

      coherence by XBOOLE_1: 4, Th29;

    end

    registration

      let x;

      cluster (( id {x}) \+\ { [x, x]}) -> empty;

      coherence

      proof

        ( id {x}) = { [x, x]} by SYSREL: 13;

        hence thesis;

      end;

    end

    registration

      let x, y;

      cluster ((x .--> y) \+\ { [x, y]}) -> empty;

      coherence

      proof

        (x .--> y) = { [x, y]} by ZFMISC_1: 29;

        hence thesis;

      end;

    end

    registration

      let x;

      cluster (( id {x}) \+\ (x .--> x)) -> empty;

      coherence

      proof

        (( id {x}) \+\ { [x, x]}) = {} & ((x .--> x) \+\ { [x, x]}) = {} ;

        hence thesis by Th29;

      end;

    end

    theorem :: FOMODEL0:30

    x in ((D * ) \ { {} }) iff (x is D -valued FinSequence & x is non empty)

    proof

      (x is D -valued FinSequence & x is non empty) iff (x is non empty FinSequence of D) by Lm1;

      hence thesis by Th5;

    end;

    reserve f for BinOp of D;

    theorem :: FOMODEL0:31

    

     Th31: (( MultPlace f) . <*d*>) = d & for x be D -valued FinSequence st x is non empty holds (( MultPlace f) . (x ^ <*d*>)) = (f . ((( MultPlace f) . x),d))

    proof

      set F = ( MultPlace f);

      thus (F . <*d*>) = d by Lm15;

      let x be D -valued FinSequence;

      assume x is non empty;

      then

      reconsider xx = x as non empty FinSequence of D by Lm1;

      (F . (xx ^ <*d*>)) = (f . ((F . xx),d)) by Lm15;

      hence thesis;

    end;

    reserve a,a1,a2,b,b1,b2,A,B,C,X,Y,Z,x,x1,x2,y,y1,y2,z for set,

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

u,u1,u2 for Element of U,

P,Q,R for Relation,

f,f1,f2,g,g1,g2 for Function,

k,m,n for Nat,

kk,mm,nn for Element of NAT ,

m1,n1 for non zero Nat,

p,p1,p2 for FinSequence,

q,q1,q2 for U -valued FinSequence;

    registration

      let p, x, y;

      cluster (p +~ (x,y)) -> FinSequence-like;

      coherence

      proof

        set IT = (p +~ (x,y));

        ( dom IT) = ( dom p) by FUNCT_4: 99

        .= ( Seg ( len p)) by FINSEQ_1:def 3;

        hence thesis;

      end;

    end

    definition

      let x, y, p;

      :: FOMODEL0:def20

      func (x,y) -SymbolSubstIn p -> FinSequence equals (p +~ (x,y));

      coherence ;

    end

    registration

      let x, y, m;

      let p be m -element FinSequence;

      cluster ((x,y) -SymbolSubstIn p) -> m -element;

      coherence

      proof

        set IT = ((x,y) -SymbolSubstIn p);

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

        ( dom IT) = ( dom p) by FUNCT_4: 99

        .= ( Seg ( len p)) by FINSEQ_1:def 3

        .= ( Seg mm) by CARD_1:def 7;

        then ( len IT) = mm by FINSEQ_1:def 3;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      let x, U, u;

      let p be U -valued FinSequence;

      cluster ((x,u) -SymbolSubstIn p) -> U -valued;

      coherence ;

    end

    definition

      let X, x, y;

      let p be X -valued FinSequence;

      :: original: -SymbolSubstIn

      redefine

      :: FOMODEL0:def21

      func (x,y) -SymbolSubstIn p equals ((( id X) +* (x,y)) * p);

      compatibility

      proof

        ( rng p) c= X;

        hence thesis by FUNCT_7: 116;

      end;

    end

    definition

      let U, x, u, q;

      :: original: -SymbolSubstIn

      redefine

      func (x,u) -SymbolSubstIn q -> FinSequence of U ;

      coherence by Lm1;

    end

    

     Lm44: (u = u1 implies ((u1,x2) -SymbolSubstIn <*u*>) = <*x2*>) & (u <> u1 implies ((u1,x2) -SymbolSubstIn <*u*>) = <*u*>)

    proof

      set X = U, s = u, s1 = u1, s2 = x2, w = <*s*>, IT = ((s1,s2) -SymbolSubstIn w), f1 = (1 .--> s1), f2 = (1 .--> s2), f = (1 .--> s), subst = (s1 .--> s2), I = ( id X), w1 = <*s1*>, w2 = <*s2*>;

      

       A1: (w \+\ f) = {} & (w2 \+\ f2) = {} & (w1 \+\ f1) = {} ;

      then

       A2: w = f & w2 = f2 & w1 = f1 by Th29;

      

       A3: ( dom subst) = {s1} & ( dom f2) = {1} & ( dom f1) = {1} & ( dom f) = {1} & ( rng f) = {s} by FUNCOP_1: 8;

      s1 in {s1} by TARSKI:def 1;

      then

       A4: (subst . s1) = s2 by FUNCOP_1: 7;

      

       A5: IT = (w +* (subst * f)) by A1, Th29;

      thus s = s1 implies IT = w2

      proof

        assume

         A6: s = s1;

        then s in ( dom subst) by TARSKI:def 1;

        

        then IT = (f +* f2) by A6, A2, A4, FUNCOP_1: 17

        .= w2 by A2, FUNCT_4: 19, A3;

        hence IT = w2;

      end;

      assume s <> s1;

      then (subst * f) = {} by A3, ZFMISC_1: 11, RELAT_1: 44;

      hence thesis by A5;

    end;

    

     Lm45: ((x,u) -SymbolSubstIn (q1 ^ q2)) = (((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2))

    proof

      set s1 = x, s2 = u, w1 = q1, w2 = q2, w = (w1 ^ w2), IT1 = ((s1,s2) -SymbolSubstIn w1), IT2 = ((s1,s2) -SymbolSubstIn w2), IT = ((s1,s2) -SymbolSubstIn w), f = (s1 .--> s2), I = ( id U);

      reconsider g = (I +* (s1,s2)) as Function of U, U;

      reconsider w11 = w1, w22 = w2, ww = w as FinSequence of U by Lm1;

      

      thus IT = ((g * w11) ^ (g * w22)) by FINSEQOP: 9

      .= (IT1 ^ IT2);

    end;

    definition

      let U, x, u;

      set D = (U * );

      deffunc F( Element of (U * )) = ((x,u) -SymbolSubstIn $1);

      :: FOMODEL0:def22

      func x SubstWith u -> Function of (U * ), (U * ) means

      : Def22: for q holds (it . q) = ((x,u) -SymbolSubstIn q);

      existence

      proof

        consider f be Function of D, D such that

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

        take f;

        now

          let q;

          reconsider qq = q as FinSequence of U by Lm1;

          reconsider qqq = qq as Element of D;

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

          hence (f . q) = ((x,u) -SymbolSubstIn q);

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function of D, D;

        assume

         A2: for q holds (IT1 . q) = ((x,u) -SymbolSubstIn q);

        assume

         A3: for q holds (IT2 . q) = ((x,u) -SymbolSubstIn q);

        now

          let w be Element of D;

          

          thus (IT1 . w) = F(w) by A2

          .= (IT2 . w) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    

     Lm46: (u = u1 implies ((u1 SubstWith u2) . <*u*>) = <*u2*>) & (u <> u1 implies ((u1 SubstWith u2) . <*u*>) = <*u*>)

    proof

      set e = (u1 SubstWith u2), es = ((u1,u2) -SymbolSubstIn <*u*>);

      es = (e . <*u*>) by Def22;

      hence thesis by Lm44;

    end;

    registration

      let U, x, u;

      cluster (x SubstWith u) -> FinSequence-yielding;

      coherence

      proof

        set e = (x SubstWith u);

        for y be object st y in ( dom e) holds (e . y) is FinSequence;

        hence thesis by PRE_POLY:def 3;

      end;

    end

    registration

      let F be FinSequence-yielding Function, x be set;

      cluster (F . x) -> FinSequence-like;

      coherence

      proof

        per cases ;

          suppose x in ( dom F);

          hence thesis by PRE_POLY:def 3;

        end;

          suppose not x in ( dom F);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    

     Lm47: ((x SubstWith u) . (q1 ^ q2)) = (((x SubstWith u) . q1) ^ ((x SubstWith u) . q2))

    proof

      set e = (x SubstWith u), w1 = q1, w2 = q2, w = (w1 ^ w2), W1 = ((x,u) -SymbolSubstIn w1), W2 = ((x,u) -SymbolSubstIn w2), W = ((x,u) -SymbolSubstIn w);

      (e . w1) = W1 & (e . w2) = W2 & (e . w) = W by Def22;

      hence thesis by Lm45;

    end;

    registration

      let U, x, u, m;

      let p be U -valuedm -element FinSequence;

      cluster ((x SubstWith u) . p) -> m -element;

      coherence

      proof

        ((x SubstWith u) . p) = ((x,u) -SymbolSubstIn p) by Def22;

        hence thesis;

      end;

    end

    registration

      let U, x, u;

      let e be empty set;

      cluster ((x SubstWith u) . e) -> empty;

      coherence

      proof

        ( rng e) = (U /\ {} );

        then

        reconsider ee = e as U -valued 0 -element FinSequence by RELAT_1:def 19;

        ((X SubstWith u) . ee) is 0 -element;

        hence thesis;

      end;

    end

    registration

      let U;

      cluster (U -multiCat ) -> FinSequence-yielding;

      coherence

      proof

        set f = (U -multiCat );

        for x be object st x in ( dom f) holds (f . x) is FinSequence;

        hence thesis by PRE_POLY:def 3;

      end;

    end

    registration

      let U, m1, n;

      let p be (m1 + n) -elementU -valued FinSequence;

      cluster ( {(p . m1)} \ U) -> empty;

      coherence

      proof

        consider m such that

         A1: m1 = (m + 1) by NAT_1: 6;

        set IT = ( {(p . m1)} \ U), M = (m1 + n);

        p in (M -tuples_on U) by Th16;

        then p is Element of ( Funcs (( Seg M),U)) by Lm7;

        then

        reconsider f = p as Function of ( Seg M), U;

        1 <= (m + 1) & (m + 1) <= ((m + 1) + n) by NAT_1: 11;

        then

        reconsider ms = m1 as Element of ( Seg M) by A1, FINSEQ_1: 1;

        (f . ms) in U;

        hence thesis by ZFMISC_1: 60;

      end;

    end

    registration

      let U, m, n;

      let p be ((m + 1) + n) -element Element of (U * );

      cluster ( {(p . (m + 1))} \ U) -> empty;

      coherence ;

    end

    registration

      let x;

      cluster ( <*x*> \+\ { [1, x]}) -> empty;

      coherence ;

    end

    registration

      let m;

      let p be (m + 1) -element FinSequence;

      cluster (((p | ( Seg m)) ^ <*(p . (m + 1))*>) \+\ p) -> empty;

      coherence

      proof

        set q = (p | ( Seg m));

        ( len p) = (m + 1) by CARD_1:def 7;

        then p = (q ^ <*(p . (m + 1))*>) by FINSEQ_3: 55;

        hence thesis;

      end;

    end

    registration

      let m, n;

      let p be (m + n) -element FinSequence;

      cluster (p | ( Seg m)) -> m -element;

      coherence

      proof

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

        set q = (p | ( Seg m)), N = (m + n);

        (m + 0 ) <= N & ( len p) = N by XREAL_1: 7, CARD_1:def 7;

        then ( Seg m) c= ( Seg N) & ( dom p) = ( Seg N) by FINSEQ_1: 5, FINSEQ_1:def 3;

        then

        reconsider M = ( Seg m) as Subset of ( dom p);

        ( dom q) = (M null ( dom p)) by RELAT_1: 61

        .= ( Seg mm);

        then ( len q) = mm by FINSEQ_1:def 3;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      cluster { {} } -valued -> empty-yielding for Relation;

      coherence ;

      cluster empty-yielding -> { {} } -valued for Relation;

      coherence ;

    end

    theorem :: FOMODEL0:32

    

     Th32: ((U -multiCat ) . x) = (( MultPlace (U -concatenation )) . x)

    proof

      set D = (U * ), f = (U -concatenation ), F = ( MultPlace f), G = (U -multiCat );

      set g = ( {} .--> {} );

      reconsider g as { {} } -valued Function;

      ( dom f) = [:D, D:] & ( dom F) = ((D * ) \ { {} }) & ( dom G) = (D * ) by FUNCT_2:def 1;

      then

      reconsider dF = ( dom F) as Subset of ( dom G);

      per cases ;

        suppose x in ( dom F);

        hence (G . x) = (F . x) by FUNCT_4: 13;

      end;

        suppose

         A1: not x in ( dom F);

        

        hence (G . x) = (g . x) by FUNCT_4: 11

        .= (F . x) by FUNCT_1:def 2, A1;

      end;

    end;

    theorem :: FOMODEL0:33

    

     Th33: p is (U * ) -valued implies ((U -multiCat ) . (p ^ <*q*>)) = (((U -multiCat ) . p) ^ q)

    proof

      set C = (U -multiCat ), g = (U -concatenation ), G = ( MultPlace g);

      reconsider qq = q as FinSequence of U by Lm1;

      per cases ;

        suppose p is empty;

        then

        reconsider e = p as empty set;

        

         A1: ((C . e) ^ q) = q & (C . (e ^ <*q*>)) = (C . <*q*>);

        (C . (e ^ <*q*>)) = (G . <*qq*>) by Th32

        .= qq by Th31;

        hence thesis by A1;

      end;

        suppose

         A2: not p is empty;

        assume p is (U * ) -valued;

        then

        reconsider pp = p as non empty(U * ) -valued FinSequence by A2;

        reconsider ppp = pp as non empty FinSequence of (U * ) by Lm1;

        (C . (pp ^ <*q*>)) = (G . (pp ^ <*qq*>)) by Th32

        .= (g . ((G . pp),qq)) by Th31

        .= (g . ((C . ppp),q)) by Th32

        .= ((C . p) ^ q) by Th4;

        hence thesis;

      end;

    end;

    

     Lm48: p is (U * ) -valued implies ((x SubstWith u) . ((U -multiCat ) . p)) = ((U -multiCat ) . ((x SubstWith u) * p))

    proof

      set S = U, C = (S -multiCat ), SS = U, strings = (U * ), e = (x SubstWith u), m = ( len p), F = (U -firstChar ), FF = (strings -firstChar ), g = (SS -concatenation ), G = ( MultPlace g);

      defpred P[ Nat] means for p be $1 -elementstrings -valued FinSequence holds (e . (C . p)) = (C . (e * p));

      

       A1: P[ 0 ];

      

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

      proof

        let n;

        set n1 = (n + 1);

        assume

         A3: P[n];

        let p be n1 -elementstrings -valued FinSequence;

        reconsider q = (p | ( Seg n)) as n -elementstrings -valued FinSequence;

        reconsider qq = q as n -element FinSequence of strings by Lm1;

        p is (n1 + 0 ) -element;

        then ( {(p . n1)} \ strings) = {} ;

        then

        reconsider z = (p . n1) as Element of strings by ZFMISC_1: 60;

        reconsider f = (e . z) as Element of (SS * );

        ((q ^ <*z*>) \+\ p) = {} ;

        then

         A4: (q ^ <*z*>) = p by Th29;

        (C . (e * p)) = (C . ((e * qq) ^ <*f*>)) by FINSEQOP: 8, A4

        .= ((C . (e * qq)) ^ f) by Th33

        .= ((e . (C . qq)) ^ f) by A3

        .= (e . ((C . qq) ^ z)) by Lm47

        .= (e . (C . p)) by Th33, A4;

        hence thesis;

      end;

      

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

      assume p is (U * ) -valued;

      then

      reconsider pp = p as m -element(U * ) -valued FinSequence by CARD_1:def 7;

      (e . (C . pp)) = (C . (e * pp)) by A5;

      hence thesis;

    end;

    registration

      let Y;

      let X be Subset of Y;

      let R be totalY -defined Relation;

      cluster (R | X) -> total;

      coherence

      proof

        set IT = (R | X);

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

        then

         A1: ( dom IT) = (X null Y) by RELAT_1: 61;

        reconsider ITT = IT as X -defined Relation;

        thus thesis by A1, PARTFUN1:def 2;

      end;

    end

    theorem :: FOMODEL0:34

    (u = u1 implies ((u1,x2) -SymbolSubstIn <*u*>) = <*x2*>) & (u <> u1 implies ((u1,x2) -SymbolSubstIn <*u*>) = <*u*>) by Lm44;

    theorem :: FOMODEL0:35

    (u = u1 implies ((u1 SubstWith u2) . <*u*>) = <*u2*>) & (u <> u1 implies ((u1 SubstWith u2) . <*u*>) = <*u*>) by Lm46;

    theorem :: FOMODEL0:36

    ((x SubstWith u) . (q1 ^ q2)) = (((x SubstWith u) . q1) ^ ((x SubstWith u) . q2)) by Lm47;

    theorem :: FOMODEL0:37

    p is (U * ) -valued implies ((x SubstWith u) . ((U -multiCat ) . p)) = ((U -multiCat ) . ((x SubstWith u) * p)) by Lm48;

    theorem :: FOMODEL0:38

    ((U -concatenation ) .: ( id (1 -tuples_on U))) = the set of all <*u, u*> where u be Element of U

    proof

      set f = (U -concatenation ), U1 = (1 -tuples_on U), D = ( id U1), U2 = (2 -tuples_on U), A = (f .: D), B = the set of all <*u, u*> where u be Element of U;

      D c= [:U1, U1:] & U1 c= (U * ) by FINSEQ_2: 142;

      then [:U1, U1:] c= [:(U * ), (U * ):] by ZFMISC_1: 96;

      then

      reconsider DD = D as Subset of [:(U * ), (U * ):] by XBOOLE_1: 1;

      

       A1: U1 = the set of all <*u*> where u be Element of U by FINSEQ_2: 96;

      

       A2: ( dom D) = U1 & ( dom f) = [:(U * ), (U * ):] by FUNCT_2:def 1;

      then

       A3: D = { [x, (D . x)] where x be Element of U1 : x in U1 } by Th20;

      now

        let y be object;

        assume y in A;

        then

        consider x be object such that

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

        consider p be Element of U1 such that

         A5: x = [p, (D . p)] & p in U1 by A4, A3;

        consider u be Element of U such that

         A6: p = <*u*> by A5, A1;

        reconsider pp = p as FinSequence of U;

        y = (f . (pp,pp)) by A4, A5;

        then y = <*u, u*> by Th4, A6;

        hence y in B;

      end;

      then

       A7: A c= B;

      now

        let y be object;

        assume y in B;

        then

        consider u be Element of U such that

         A8: y = <*u, u*>;

        reconsider p = <*u*> as Element of U1 by FINSEQ_2: 98;

        reconsider pp = p as FinSequence of U;

         [p, (D . p)] = [p, p] & p in U1;

        then [p, p] in D by A3;

        then

        reconsider dd = [p, p] as Element of D;

        

         A9: dd in (DD null [:(U * ), (U * ):]);

        y = (f . (pp,pp)) by A8, Th4

        .= (f . dd);

        hence y in (f .: D) by A9, A2, FUNCT_1:def 6;

      end;

      then B c= A;

      hence thesis by A7;

    end;

    registration

      let f, U, u;

      cluster (((f | U) . u) \+\ (f . u)) -> empty;

      coherence

      proof

        ((f | U) . u) = (f . u) by FUNCT_1: 49;

        hence thesis;

      end;

    end

    registration

      let f, U1, U2;

      let u be Element of U1, g be Function of U1, U2;

      cluster (((f * g) . u) \+\ (f . (g . u))) -> empty;

      coherence

      proof

        ( dom g) = U1 by FUNCT_2:def 1;

        then ((f * g) . u) = (f . (g . u)) by FUNCT_1: 13;

        hence thesis;

      end;

    end

    registration

      cluster non negative -> natural for Integer;

      coherence

      proof

        let i be Integer;

        assume i is non negative;

        then i in NAT by INT_1: 3;

        hence thesis;

      end;

    end

    registration

      let x,y be Real;

      cluster (( max (x,y)) - x) -> non negative;

      coherence

      proof

        set z = ( max (x,y));

        (x + ( - x)) <= (z + ( - x)) by XREAL_1: 6, XXREAL_0: 25;

        then 0 <= (z - x);

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:39

    x is boolean implies (x = 1 iff x <> 0 ) by XBOOLEAN:def 3;

    registration

      let Y;

      let X be Subset of Y;

      cluster (X \ Y) -> empty;

      coherence by XBOOLE_1: 37;

    end

    registration

      let x,y be object;

      cluster ( {x} \ {x, y}) -> empty;

      coherence

      proof

        x in {x, y} by TARSKI:def 2;

        hence thesis by ZFMISC_1: 60;

      end;

    end

    registration

      let x,y be set;

      cluster (( [x, y] `1 ) \+\ x) -> empty;

      coherence ;

    end

    registration

      let x, y;

      cluster (( [x, y] `2 ) \+\ y) -> empty;

      coherence ;

    end

    registration

      let n be positive Nat;

      let X be non empty set;

      cluster n -element for Element of ((X * ) \ { {} });

      existence

      proof

        consider m such that

         A1: n = (m + 1) by NAT_1: 6;

        set x = the Element of ((m + 1) -tuples_on X);

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

        

         A2: x in (mm -tuples_on X) & (mm -tuples_on X) c= (X * ) by FINSEQ_2: 134;

         not x in { {} };

        then

        reconsider xx = x as Element of ((X * ) \ { {} }) by A2, XBOOLE_0:def 5;

        take xx;

        thus thesis by A1;

      end;

    end

    registration

      let m1;

      cluster (m1 + 0 ) -element -> non empty for FinSequence;

      coherence ;

    end

    registration

      let R, x;

      cluster (R null x) -> Relation-like;

      coherence ;

    end

    registration

      let f be Function-like set;

      let x;

      cluster (f null x) -> Function-like;

      coherence ;

    end

    registration

      let p be FinSequence-like Relation;

      let x;

      cluster (p null x) -> FinSequence-like;

      coherence ;

    end

    registration

      let p, x;

      cluster (p null x) -> ( len p) -element;

      coherence by CARD_1:def 7;

    end

    registration

      let p be non empty FinSequence;

      cluster ( len p) -> non zero;

      coherence ;

    end

    registration

      let R be Relation, X be set;

      cluster (R | X) -> X -defined;

      coherence by RELAT_1: 58;

    end

    registration

      let x;

      let e be empty set;

      cluster (e null x) -> empty;

      coherence ;

    end

    registration

      let X;

      let e be empty set;

      cluster (e null X) -> X -valued;

      coherence

      proof

        ( rng e) = (( rng e) /\ X);

        hence thesis;

      end;

    end

    registration

      let Y be non empty FinSequence-membered set;

      cluster Y -valued -> FinSequence-yielding for Function;

      coherence

      proof

        let f;

        assume f is Y -valued;

        then

         A1: ( rng f) c= Y;

        now

          let x be object;

          assume

           A2: x in ( dom f);

          then

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

          reconsider xx = x as Element of D by A2;

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

          (ff . xx) in Y;

          hence (f . x) is FinSequence;

        end;

        hence thesis by PRE_POLY:def 3;

      end;

    end

    registration

      let X, Y;

      cluster -> FinSequence-yielding for Element of ( Funcs (X,(Y * )));

      coherence ;

    end

    theorem :: FOMODEL0:40

    

     Th40: f is (X * ) -valued implies (f . x) in (X * )

    proof

      assume f is (X * ) -valued;

      then

       A1: ( rng f) c= (X * );

      per cases ;

        suppose

         A2: x in ( dom f);

        then

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

        reconsider e = x as Element of D by A2;

        reconsider ff = f as Function of D, (X * ) by FUNCT_2: 2, A1;

        (ff . e) is Element of (X * );

        hence thesis;

      end;

        suppose not x in ( dom f);

        then (f . x) = {} by FUNCT_1:def 2;

        hence thesis by FINSEQ_1: 49;

      end;

    end;

    registration

      let m, n;

      let p be m -element FinSequence;

      cluster (p null n) -> ( Seg (m + n)) -defined;

      coherence

      proof

        ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        then (m + 0 ) <= (m + n) & ( dom p) = ( Seg m) by CARD_1:def 7, XREAL_1: 6;

        hence thesis by FINSEQ_1: 5;

      end;

    end

    

     Lm49: for p1,p2,q1,q2 be FinSequence st p1 is m -element & q1 is m -element & (p1 ^ p2) = (q1 ^ q2) holds (p1 = q1 & p2 = q2)

    proof

      let p1,p2,q1,q2 be FinSequence;

      set P = (p1 ^ p2), Q = (q1 ^ q2);

      assume p1 is m -element & q1 is m -element;

      then

      reconsider x = p1, y = q1 as m -element FinSequence;

      ( Seg ( len p1)) = ( dom p1) & ( Seg ( len q1)) = ( dom q1) by FINSEQ_1:def 3;

      then

       A1: ( dom x) = ( Seg m) & ( dom y) = ( Seg m) by CARD_1:def 7;

      assume

       A2: P = Q;

      (x null 0 ) is ( Seg (m + 0 )) -defined & (y null 0 ) is ( Seg (m + 0 )) -defined;

      then

      reconsider p11 = p1, q11 = q1 as ( Seg m) -defined FinSequence;

      

       A3: (p11 null ( Seg m)) = ((q11 ^ q2) | ( Seg m)) by A1, A2, FINSEQ_6: 11

      .= (q11 null ( Seg m)) by A1, FINSEQ_6: 11;

      hence p1 = q1;

      thus p2 = q2 by A3, A2, FINSEQ_1: 33;

    end;

    registration

      let m, n;

      let p be m -element FinSequence;

      let q be n -element FinSequence;

      cluster (p ^ q) -> (m + n) -element;

      coherence ;

    end

    theorem :: FOMODEL0:41

    for p1,p2,q1,q2 be FinSequence st p1 is m -element & q1 is m -element & ((p1 ^ p2) = (q1 ^ q2) or (p2 ^ p1) = (q2 ^ q1)) holds (p1 = q1 & p2 = q2)

    proof

      let p1,p2,q1,q2 be FinSequence;

      set m1 = ( len p1), m2 = ( len p2), n1 = ( len q1), n2 = ( len q2);

      assume p1 is m -element & q1 is m -element;

      then

      reconsider p11 = p1, q11 = q1 as m -element FinSequence;

      reconsider p22 = (p2 null p2) as m2 -element FinSequence;

      reconsider q22 = (q2 null q2) as n2 -element FinSequence;

      set PA = (p11 ^ p22), PB = (p22 ^ p11), QA = (q11 ^ q22), QB = (q22 ^ q11);

      

       A1: ( len PA) = (m + m2) & ( len PB) = (m2 + m) & ( len QA) = (m + n2) & ( len QB) = (n2 + m) by CARD_1:def 7;

      assume

       A2: (p1 ^ p2) = (q1 ^ q2) or (p2 ^ p1) = (q2 ^ q1);

      then

       A3: PA = QA or PB = QB;

      reconsider q22 as m2 -element FinSequence by A2, A1;

      p22 is m2 -element & q22 is m2 -element;

      hence thesis by A3, Lm49;

    end;

    theorem :: FOMODEL0:42

    (((U -multiCat ) . x) is U1 -valued & x in ((U * ) * )) implies x is FinSequence of (U1 * )

    proof

      set C = (U -multiCat ), f = (U -concatenation ), F = ( MultPlace f), D = (U * );

      ( {} null (U * )) is (U * ) -valued Relation;

      then

      reconsider e = {} as (U * ) -valued FinSequence;

      defpred P[ Nat] means for p be ($1 + 1) -element(U * ) -valued FinSequence st (C . p) is U1 -valued holds p is (U1 * ) -valued;

      

       A1: P[ 0 ]

      proof

        let p be ( 0 + 1) -element(U * ) -valued FinSequence;

        reconsider ppp = p as (1 + 0 ) -element(U * ) -valued FinSequence;

        ( {(ppp . 1)} \ (U * )) = {} ;

        then

        reconsider p1 = (p . 1) as Element of (U * ) by ZFMISC_1: 60;

        

         A2: ( len p) = 1 by CARD_1:def 7;

        p = ( {} ^ <*(p . 1)*>) by A2, FINSEQ_1: 40;

        

        then

         A3: (C . p) = ((C . e) ^ p1) by Th33

        .= ( {} ^ (p . 1))

        .= (p . 1);

        p is 1 -element FinSequence of (U * ) by Lm1;

        then

        reconsider pp = p as 1 -element Element of ((U * ) * );

        assume (C . p) is U1 -valued;

        then

        reconsider u1 = (C . pp) as FinSequence of U1 by Lm1;

        u1 = (p . 1) by A3;

        then

        reconsider q = (p . 1) as Element of (U1 * );

         <*q*> is FinSequence of (U1 * );

        hence thesis by A2, FINSEQ_1: 40;

      end;

      

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

      proof

        let n;

        reconsider NN = (n + 1) as non zero Element of NAT by ORDINAL1:def 12;

        assume

         A5: P[n];

        let p be ((n + 1) + 1) -element(U * ) -valued FinSequence;

        assume

         A6: (C . p) is U1 -valued;

        reconsider pp = (p null p) as (n + 2) -element(U * ) -valued FinSequence;

        reconsider ppp = pp as (NN + 1) -element(U * ) -valued FinSequence;

        reconsider pppp = ppp as ((NN + 1) + 0 ) -element(U * ) -valued FinSequence;

        reconsider p1 = (ppp | ( Seg NN)) as NN -element(U * ) -valued FinSequence;

        ( {(pppp . (NN + 1))} \ (U * )) = {} ;

        then

        reconsider u = (ppp . (NN + 1)) as Element of (U * ) by ZFMISC_1: 60;

        

         A7: (ppp \+\ (p1 ^ <*(ppp . (NN + 1))*>)) = {} ;

        then p = (p1 ^ <*u*>) by Th29;

        then

         A8: (C . p) = ((C . p1) ^ u) by Th33;

        then ( rng (C . p)) c= U1 & ( rng (C . p1)) c= ( rng (C . p)) by A6, FINSEQ_1: 29;

        then

        reconsider q = (C . p1) as U1 -valued FinSequence by XBOOLE_1: 1, RELAT_1:def 19;

        q is U1 -valued;

        then

        reconsider p11 = p1 as NN -element(U1 * ) -valued FinSequence by A5;

        ( rng u) c= ( rng (C . p)) & ( rng (C . p)) c= U1 by A8, FINSEQ_1: 30, A6;

        then u is U1 -valued by XBOOLE_1: 1;

        then u is FinSequence of U1 by Lm1;

        then

        reconsider uu = u as Element of (U1 * );

        (p11 ^ <*uu*>) is (U1 * ) -valued;

        hence thesis by A7, Th29;

      end;

      

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

      assume

       A10: (C . x) is U1 -valued & x in ((U * ) * );

      per cases ;

        suppose x is empty;

        then

        reconsider xx = x as empty set;

        (xx null (U1 * )) is (U1 * ) -valued FinSequence;

        hence thesis by Lm1;

      end;

        suppose not x is empty;

        then

        reconsider xx = x as non empty(U * ) -valued FinSequence by A10;

        consider m such that

         A11: ( len xx) = (m + 1) by NAT_1: 6;

        (xx null {} ) is (m + 1) -element by A11;

        then

        reconsider xxx = xx as (m + 1) -element(U * ) -valued FinSequence;

        xxx is (U1 * ) -valued by A10, A9;

        hence thesis by Lm1;

      end;

    end;

    registration

      let U;

      cluster total for reflexive Relation of U;

      existence

      proof

        set R = the total symmetric transitive reflexive Relation of U;

        take R;

        thus thesis;

      end;

    end

    registration

      let m;

      cluster (m + 1) -element -> non empty for FinSequence;

      coherence ;

    end

    registration

      let U, u;

      cluster ((( id U) . u) \+\ u) -> empty;

      coherence ;

    end

    registration

      let U;

      let p be U -valued non empty FinSequence;

      cluster ( {(p . 1)} \ U) -> empty;

      coherence

      proof

        consider m such that

         A1: ( len p) = (m + 1) by NAT_1: 6;

        reconsider pp = p as (1 + m) -elementU -valued FinSequence by A1, CARD_1:def 7;

        ( {(pp . 1)} \ U) = {} ;

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:43

    (x1 = x2 implies ((f +* (x1 .--> y1)) +* (x2 .--> y2)) = (f +* (x2 .--> y2))) & (x1 <> x2 implies ((f +* (x1 .--> y1)) +* (x2 .--> y2)) = ((f +* (x2 .--> y2)) +* (x1 .--> y1)))

    proof

      set f1 = (x1 .--> y1), f2 = (x2 .--> y2), LH = ((f +* f1) +* f2);

      hereby

        assume x1 = x2;

        then {x1} = ( dom f2);

        then ( dom f1) = ( dom f2);

        then (f1 +* f2) = f2 by FUNCT_4: 19;

        hence LH = (f +* f2) by FUNCT_4: 14;

      end;

      assume x1 <> x2;

      then {x1} misses {x2} by ZFMISC_1: 11;

      then f1 tolerates f2 by FUNCOP_1: 87;

      

      then (f +* (f1 +* f2)) = (f +* (f2 +* f1)) by FUNCT_4: 34

      .= ((f +* f2) +* f1) by FUNCT_4: 14;

      hence LH = ((f +* f2) +* f1) by FUNCT_4: 14;

    end;

    registration

      let X, U;

      cluster U -valued total for X -defined Function;

      existence

      proof

        set f = the total PartFunc of X, U;

        take f;

        thus thesis;

      end;

    end

    registration

      let X, U;

      let P be U -valued totalX -defined Relation;

      let Q be totalU -defined Relation;

      cluster (P * Q) -> total;

      coherence

      proof

        ( rng P) c= U & ( dom Q) = U by PARTFUN1:def 2;

        

        then ( dom (P * Q)) = ( dom P) by RELAT_1: 27

        .= X by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: FOMODEL0:44

    ((p ^ p1) ^ p2) is X -valued implies (p2 is X -valued & p1 is X -valued & p is X -valued)

    proof

      set q = ((p ^ p1) ^ p2);

      assume q is X -valued;

      then ( rng q) c= X & ( rng (p ^ p1)) c= ( rng q) & ( rng p2) c= ( rng q) by FINSEQ_1: 29, FINSEQ_1: 30;

      then ( rng p2) c= X & ( rng p) c= ( rng (p ^ p1)) & ( rng p1) c= ( rng (p ^ p1)) & ( rng (p ^ p1)) c= X by FINSEQ_1: 29, FINSEQ_1: 30;

      hence thesis by XBOOLE_1: 1;

    end;

    registration

      let X;

      let R be Relation;

      cluster (R null X) -> (X \/ ( rng R)) -valued;

      coherence

      proof

        (( rng R) null X) c= (( rng R) \/ X);

        hence thesis;

      end;

    end

    registration

      let X,Y be functional set;

      cluster (X \/ Y) -> functional;

      coherence

      proof

        now

          let x be object;

          assume x in (X \/ Y);

          then x in X or x in Y by XBOOLE_0:def 3;

          hence x is Function;

        end;

        hence thesis by FUNCT_1:def 13;

      end;

    end

    registration

      cluster FinSequence-membered -> finite-membered for set;

      coherence

      proof

        let X;

        assume

         A1: X is FinSequence-membered;

        for x st x in X holds x is finite by A1;

        hence thesis by FINSET_1:def 6;

      end;

    end

    definition

      let X be functional set;

      :: FOMODEL0:def23

      func SymbolsOf X -> set equals ( union { ( rng x) where x be Element of (X \/ { {} }) : x in X });

      coherence ;

    end

    

     Lm50: for X be functional set st X is finite & X is finite-membered holds ( SymbolsOf X) is finite

    proof

      let X be functional set;

      set Y = (X \/ { {} }), F = { ( rng y) where y be Element of Y : y in X };

      assume

       A1: X is finite;

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

      then

      reconsider FF = F as finite set;

      assume X is finite-membered;

      then

      reconsider YY = Y as finite-membered set;

      now

        let y;

        assume y in F;

        then

        consider x be Element of Y such that

         A2: y = ( rng x) & x in X;

        reconsider xx = x as Element of YY;

        xx is finite;

        hence y is finite by A2;

      end;

      then

      reconsider FFF = FF as finite-membered finite set by FINSET_1:def 6;

      ( union FFF) is finite;

      hence thesis;

    end;

    registration

      cluster trivial for FinSequence-membered non empty set;

      existence

      proof

        set U = the non empty set;

        take IT = { the Element of (U * )};

        thus thesis;

      end;

    end

    registration

      let X be functional finite finite-membered set;

      cluster ( SymbolsOf X) -> finite;

      coherence by Lm50;

    end

    registration

      let X be finite FinSequence-membered set;

      cluster ( SymbolsOf X) -> finite;

      coherence ;

    end

    theorem :: FOMODEL0:45

    

     Th45: ( SymbolsOf {f}) = ( rng f)

    proof

      set P = f, X = {P}, F = { ( rng x) where x be Element of (X \/ { {} }) : x in X }, LH = ( union F), RH = ( rng P);

      (X null { {} }) c= (X \/ { {} });

      then

      reconsider XX = X as Subset of (X \/ { {} });

      reconsider PP = P as Element of XX by TARSKI:def 1;

      reconsider PPP = PP as Element of (X \/ { {} }) by TARSKI:def 3;

      now

        let y be object;

        assume y in LH;

        then

        consider z such that

         A1: y in z & z in F by TARSKI:def 4;

        consider x be Element of (X \/ { {} }) such that

         A2: z = ( rng x) & x in X by A1;

        thus y in RH by A1, A2, TARSKI:def 1;

      end;

      then

       A3: LH c= RH;

      now

        let y be object;

        assume y in RH;

        then y in ( rng PP) & ( rng PPP) in F;

        hence y in LH by TARSKI:def 4;

      end;

      then RH c= LH;

      hence thesis by A3;

    end;

    registration

      let P be Function;

      cluster (( SymbolsOf {P}) \+\ ( rng P)) -> empty;

      coherence by Th29, Th45;

    end

    registration

      let z be non zero Complex;

      cluster |.z.| -> positive;

      coherence by COMPLEX1: 47;

    end

    scheme :: FOMODEL0:sch1

    Sc1 { A() -> set , B() -> set , F( set) -> set } :

{ F(x) where x be Element of A() : x in A() } = { F(x) where x be Element of B() : x in A() }

      provided

       A1: A() c= B();

      set LH = { F(x) where x be Element of A() : x in A() }, RH = { F(x) where x be Element of B() : x in A() };

      now

        let y be object;

        assume y in LH;

        then

        consider x be Element of A() such that

         A2: y = F(x) & x in A();

        reconsider xx = x as Element of B() by A2, A1;

        y = F(xx) & xx in A() by A2;

        hence y in RH;

      end;

      then

       A3: LH c= RH;

      now

        let y be object;

        assume y in RH;

        then

        consider x be Element of B() such that

         A4: y = F(x) & x in A();

        reconsider xx = x as Element of A() by A4;

        thus y in LH by A4;

      end;

      then RH c= LH;

      hence thesis by A3;

    end;

    definition

      let X be functional set;

      :: original: SymbolsOf

      redefine

      :: FOMODEL0:def24

      func SymbolsOf X equals ( union { ( rng x) where x be Element of X : x in X });

      compatibility

      proof

        set F1 = { ( rng x) where x be Element of X : x in X }, F2 = { ( rng x) where x be Element of (X \/ { {} }) : x in X };

        (X null { {} }) c= (X \/ { {} });

        then

         A1: X c= (X \/ { {} });

        F1 = F2 from Sc1( A1);

        hence thesis;

      end;

    end

    

     Lm51: for B be functional set, A be Subset of B holds { ( rng x) where x be Element of A : x in A } c= { ( rng x) where x be Element of B : x in B }

    proof

      let B be functional set;

      let A be Subset of B;

      set AF = { ( rng x) where x be Element of A : x in A }, BF = { ( rng x) where x be Element of B : x in B };

      let y be object;

      assume y in AF;

      then

      consider x be Element of A such that

       A1: y = ( rng x) & x in A;

      reconsider xb = x as Element of B by A1;

      thus y in BF by A1;

    end;

    theorem :: FOMODEL0:46

    for B be functional set, A be Subset of B holds ( SymbolsOf A) c= ( SymbolsOf B) by Lm51, ZFMISC_1: 77;

    theorem :: FOMODEL0:47

    

     Th47: for A,B be functional set holds ( SymbolsOf (A \/ B)) = (( SymbolsOf A) \/ ( SymbolsOf B))

    proof

      let A,B be functional set;

      set AF = { ( rng x) where x be Element of A : x in A }, BF = { ( rng x) where x be Element of B : x in B }, F = { ( rng x) where x be Element of (A \/ B) : x in (A \/ B) };

      (A null B) c= (A \/ B) & (B null A) c= (A \/ B);

      then

      reconsider AFF = AF, BFF = BF as Subset of F by Lm51;

      

       A1: (AFF \/ BFF) c= F;

      now

        let y be object;

        assume y in (F \ BF);

        then

         A2: y in F & not y in BF by XBOOLE_0:def 5;

        then

        consider x be Element of (A \/ B) such that

         A3: y = ( rng x) & x in (A \/ B);

         not x in B by A3, A2;

        then

         A4: x in (A null { {} }) by A3, XBOOLE_0:def 3;

        then

        reconsider xx = x as Element of (A \/ { {} });

        thus y in AF by A4, A3;

      end;

      then ((F \ BF) \/ BF) c= (AF \/ BF) by XBOOLE_1: 9, TARSKI:def 3;

      then (F null BFF) c= (AF \/ BF) by XBOOLE_1: 39;

      then

       A5: (AF \/ BF) = F by A1;

      thus thesis by A5, ZFMISC_1: 78;

    end;

    registration

      let X;

      let F be Subset of ( bool X);

      cluster (( union F) \ X) -> empty;

      coherence ;

    end

    theorem :: FOMODEL0:48

    

     Th48: X = ((X \ Y) \/ (X /\ Y))

    proof

      reconsider x = (X \ Y) as Subset of X;

      X = (x \/ (X \ x)) by XBOOLE_1: 45

      .= (x \/ (X /\ Y)) by XBOOLE_1: 48;

      hence thesis;

    end;

    theorem :: FOMODEL0:49

    (m -tuples_on A) meets (n -tuples_on B) implies m = n by Lm5;

    theorem :: FOMODEL0:50

    B is D -prefix & A c= B implies A is D -prefix;

    theorem :: FOMODEL0:51

    

     Th51: f c= g iff for x st x in ( dom f) holds (x in ( dom g) & (f . x) = (g . x))

    proof

      defpred Q1[] means for x be object st x in ( dom f) holds x in ( dom g);

      defpred Q2[] means for x be object st x in ( dom f) holds (f . x) = (g . x);

       Q1[] & Q2[] iff ( dom f) c= ( dom g) & Q2[];

      hence thesis by GRFUNC_1: 2;

    end;

    registration

      let X,Y be set;

      cluster (((X \ Y) \/ (X /\ Y)) \+\ X) -> empty;

      coherence by Th29, Th48;

      let Z be set;

      cluster (((X /\ Y) \/ (X /\ Z)) \+\ (X /\ (Y \/ Z))) -> empty;

      coherence by XBOOLE_1: 23, Th29;

      cluster (((X \ Y) \ Z) \+\ (X \ (Y \/ Z))) -> empty;

      coherence by XBOOLE_1: 41, Th29;

    end

    registration

      let X,Y be functional set;

      cluster ((( SymbolsOf X) \/ ( SymbolsOf Y)) \+\ ( SymbolsOf (X \/ Y))) -> empty;

      coherence by Th47, Th29;

    end

    registration

      let U;

      cluster non empty -> non empty-yielding for Element of (((U * ) \ { {} }) * );

      coherence

      proof

        set D = (((U * ) \ { {} }) * );

        let p be Element of D;

        assume p is non empty;

        then

        consider m such that

         A1: (m + 1) = ( len p) by NAT_1: 6;

        reconsider pp = p as (1 + m) -element((U * ) \ { {} }) -valued FinSequence by A1, CARD_1:def 7;

        ( {(pp . 1)} \ ((U * ) \ { {} })) = {} ;

        then (pp . 1) in ((U * ) \ { {} }) by ZFMISC_1: 60;

        then (p . 1) in (U * ) & not (p . 1) in { {} } by XBOOLE_0:def 5;

        then (p . 1) <> {} by TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      let e be empty set;

      cluster -> empty for Element of (e * );

      coherence ;

    end

    theorem :: FOMODEL0:52

    

     Th52: (((U1 -multiCat ) . x) <> {} & ((U2 -multiCat ) . x) <> {} implies ((U1 -multiCat ) . x) = ((U2 -multiCat ) . x)) & (p is ( {} * ) -valued implies ((U1 -multiCat ) . p) = {} ) & (((U1 -multiCat ) . p) = {} & p is (U1 * ) -valued implies p is ( {} * ) -valued)

    proof

      reconsider e = {} as Element of { {} } by TARSKI:def 1;

      defpred P[ Nat] means for U1, U2, p st p is ($1 + 1) -element holds (p is ( {} * ) -valued implies ((U1 -multiCat ) . p) = {} ) & (((U1 -multiCat ) . p) = {} & p is (U1 * ) -valued implies p is { {} } -valued) & (((U1 -multiCat ) . p) <> {} & ((U2 -multiCat ) . p) <> {} implies ((U1 -multiCat ) . p) = ((U2 -multiCat ) . p));

      

       A1: P[ 0 ]

      proof

        let U1, U2, p;

        set C1 = (U1 -multiCat ), C2 = (U2 -multiCat );

        

         A2: ( dom C1) = ((U1 * ) * ) & ( dom C2) = ((U2 * ) * ) by FUNCT_2:def 1;

        ( {} /\ U1) = {} ;

        then

        reconsider EE = {} as Subset of U1;

        ( {} /\ U2) = {} ;

        then

        reconsider EE2 = {} as Subset of U2;

        reconsider E2 = (EE2 * ) as non empty Subset of (U2 * );

        reconsider eu2 = {} as Element of E2 by TARSKI:def 1;

        reconsider E = (EE * ) as non empty Subset of (U1 * );

        reconsider euu = {} as Element of E by TARSKI:def 1;

        assume p is ( 0 + 1) -element;

        then

        reconsider pp = p as (1 + 0 ) -element FinSequence;

        ( len pp) = 1 by CARD_1:def 7;

        

        then

         A3: p = ( {} ^ <*(p . 1)*>) by FINSEQ_1: 40

        .= (euu ^ <*(p . 1)*>);

        hereby

          assume p is ( {} * ) -valued;

          then p = (euu ^ <*euu*>) by A3;

          

          hence (C1 . p) = ((C1 . euu) ^ euu) by Th33

          .= ( {} ^ {} )

          .= {} ;

        end;

        hereby

          assume

           A4: (C1 . p) = {} & p is (U1 * ) -valued;

          then

          reconsider ppp = pp as non empty(U1 * ) -valued FinSequence;

          ( {(ppp . 1)} \ (U1 * )) = {} ;

          then

          reconsider l = (pp . 1) as Element of (U1 * ) by ZFMISC_1: 60;

          (C1 . p) = ((C1 . euu) ^ l) by Th33, A3

          .= ( {} ^ l)

          .= l;

          then p = (euu ^ <*euu*>) by A3, A4;

          hence p is { {} } -valued;

        end;

        hereby

          assume (C1 . p) <> {} & (C2 . p) <> {} ;

          then

           A5: p in ((U1 * ) * ) & p in ((U2 * ) * ) by FUNCT_1:def 2, A2;

          reconsider p1 = pp as non empty(U1 * ) -valued FinSequence by A5;

          reconsider p2 = pp as non empty(U2 * ) -valued FinSequence by A5;

          

           A6: ( {(p1 . 1)} \ (U1 * )) = {} & ( {(p2 . 1)} \ (U2 * )) = {} ;

          reconsider u1 = (p1 . 1) as Element of (U1 * ) by A6, ZFMISC_1: 60;

          reconsider u2 = (p2 . 1) as Element of (U2 * ) by A6, ZFMISC_1: 60;

          

           A7: (C1 . p) = ((C1 . euu) ^ u1) by A3, Th33

          .= ( {} ^ u1)

          .= u1;

          (C2 . p) = ((C2 . eu2) ^ u2) by A3, Th33

          .= ( {} ^ u1)

          .= u1;

          hence (C1 . p) = (C2 . p) by A7;

        end;

      end;

      

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

      proof

        let n;

        assume

         A9: P[n];

        let U1, U2;

        set C1 = (U1 -multiCat ), C2 = (U2 -multiCat );

        

         A10: ( dom C1) = ((U1 * ) * ) & ( dom C2) = ((U2 * ) * ) by FUNCT_2:def 1;

        let p;

        assume

         A11: p is ((n + 1) + 1) -element;

        thus p is ( {} * ) -valued implies (C1 . p) = {}

        proof

          ( {} /\ U1) = {} ;

          then

          reconsider EE = {} as Subset of U1;

          reconsider E = (EE * ) as non empty Subset of (U1 * );

          assume p is ( {} * ) -valued;

          then

          reconsider pp = p as (((n + 1) + 1) + 0 ) -element( {} * ) -valued FinSequence by A11;

          reconsider p1 = (pp | ( Seg (n + 1))) as (n + 1) -elementE -valued FinSequence;

          ( {(pp . ((n + 1) + 1))} \ ( {} * )) = {} ;

          then

          reconsider x1 = (pp . ((n + 1) + 1)) as Element of E by ZFMISC_1: 60;

          (pp \+\ (p1 ^ <*x1*>)) = {} ;

          then pp = (p1 ^ <*x1*>) & p1 is (U1 * ) -valued by Th29;

          

          then (C1 . pp) = ((C1 . p1) ^ x1) by Th33

          .= ((C1 . p1) ^ {} )

          .= {} by A9;

          hence thesis;

        end;

        thus (C1 . p) = {} & p is (U1 * ) -valued implies p is { {} } -valued

        proof

          assume

           A12: (C1 . p) = {} & p is (U1 * ) -valued;

          then

          reconsider pp = p as (((n + 1) + 1) + 0 ) -element(U1 * ) -valued FinSequence by A11;

          reconsider p1 = (pp | ( Seg (n + 1))) as (n + 1) -element(U1 * ) -valued FinSequence;

          ( {(pp . ((n + 1) + 1))} \ (U1 * )) = {} ;

          then

          reconsider x1 = (pp . ((n + 1) + 1)) as Element of (U1 * ) by ZFMISC_1: 60;

          

           A13: (pp \+\ (p1 ^ <*x1*>)) = {} ;

          then pp = (p1 ^ <*x1*>) by Th29;

          then ((C1 . p1) ^ x1) = {} by Th33, A12;

          then (C1 . p1) = {} & x1 = e;

          then (C1 . p1) = {} & <*x1*> = <*e*>;

          then

          reconsider p11 = p1, x11 = <*x1*> as { {} } -valued FinSequence by A9;

          (p11 ^ x11) is { {} } -valued;

          hence p is { {} } -valued by A13, Th29;

        end;

        assume

         A14: (C1 . p) <> {} & (C2 . p) <> {} ;

        then p in ((U1 * ) * ) by A10, FUNCT_1:def 2;

        then

        reconsider p1 = p as (((n + 1) + 1) + 0 ) -element(U1 * ) -valued FinSequence by A11;

        reconsider q1 = (p1 | ( Seg (n + 1))) as (n + 1) -element(U1 * ) -valued FinSequence;

        ( {(p1 . ((n + 1) + 1))} \ (U1 * )) = {} ;

        then

        reconsider x1 = (p1 . ((n + 1) + 1)) as Element of (U1 * ) by ZFMISC_1: 60;

        p in ((U2 * ) * ) by A14, A10, FUNCT_1:def 2;

        then

        reconsider p2 = p as (((n + 1) + 1) + 0 ) -element(U2 * ) -valued FinSequence by A11;

        reconsider q2 = (p2 | ( Seg (n + 1))) as (n + 1) -element(U2 * ) -valued FinSequence;

        ( {(p2 . ((n + 1) + 1))} \ (U2 * )) = {} ;

        then

        reconsider x2 = (p2 . ((n + 1) + 1)) as Element of (U2 * ) by ZFMISC_1: 60;

        (p1 \+\ (q1 ^ <*x1*>)) = {} & (p2 \+\ (q2 ^ <*x2*>)) = {} ;

        then p1 = (q1 ^ <*x1*>) & p2 = (q2 ^ <*x2*>) by Th29;

        then

         A15: (C1 . p1) = ((C1 . q1) ^ x1) & (C2 . p2) = ((C2 . q2) ^ x2) by Th33;

        assume

         A16: (C1 . p) <> (C2 . p);

        then (C1 . q1) = {} or (C2 . q2) = {} by A9, A15;

        then q1 is { {} } -valued by A9;

        then (C1 . q1) = {} & (C2 . q2) = {} by A9;

        hence contradiction by A16, A15;

      end;

      

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

      set C1 = (U1 -multiCat ), C2 = (U2 -multiCat );

      

       A18: ( dom C1) = ((U1 * ) * ) & ( dom C2) = ((U2 * ) * ) by FUNCT_2:def 1;

      hereby

        assume

         A19: (C1 . x) <> {} & (C2 . x) <> {} ;

        then x in ((U1 * ) * ) & x <> {} by A18, FUNCT_1:def 2;

        then

        reconsider p = x as non empty FinSequence;

        consider m such that

         A20: ( len p) = (m + 1) by NAT_1: 6;

        reconsider pp = p as (m + 1) -element FinSequence by A20, CARD_1:def 7;

        (C1 . pp) <> {} & (C2 . pp) <> {} implies (C1 . pp) = (C2 . pp) by A17;

        hence (C1 . x) = (C2 . x) by A19;

      end;

      hereby

        assume

         A21: p is ( {} * ) -valued;

        per cases ;

          suppose p = {} ;

          hence (C1 . p) = {} ;

        end;

          suppose not p = {} ;

          then

          consider m such that

           A22: (m + 1) = ( len p) by NAT_1: 6;

          reconsider pp = p as (m + 1) -element FinSequence by A22, CARD_1:def 7;

          (C1 . pp) = {} by A21, A17;

          hence (C1 . p) = {} ;

        end;

      end;

      assume

       A23: (C1 . p) = {} & p is (U1 * ) -valued;

      per cases ;

        suppose p = {} ;

        hence p is ( {} * ) -valued;

      end;

        suppose not p = {} ;

        then

        consider m such that

         A24: (m + 1) = ( len p) by NAT_1: 6;

        reconsider pp = p as (m + 1) -element FinSequence by A24, CARD_1:def 7;

        pp is ( {} * ) -valued by A23, A17;

        hence p is ( {} * ) -valued;

      end;

    end;

    registration

      let U, x;

      cluster ((U -multiCat ) . x) -> U -valued;

      coherence

      proof

        ((U -multiCat ) . x) in (U * ) by Th40;

        hence thesis;

      end;

    end

    definition

      let x;

      :: FOMODEL0:def25

      func x null equals x;

      coherence ;

    end

    registration

      let x;

      reduce (x null ) to x;

      reducibility ;

    end

    registration

      let Y be with_non-empty_elements set;

      cluster non empty -> non empty-yielding for Y -valued Relation;

      coherence

      proof

        let R be Y -valued Relation;

        assume R is non empty;

        then

        reconsider Y0 = ( rng R) as non empty set;

        set y = the Element of Y0;

        now

          assume Y0 c= { {} };

          then y in { {} } & y in Y by TARSKI:def 3;

          hence contradiction;

        end;

        hence thesis;

      end;

    end

    registration

      let X;

      cluster (X \ { {} }) -> with_non-empty_elements;

      coherence

      proof

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

        then not {} in (X \ { {} }) by XBOOLE_0:def 5;

        hence thesis by SETFAM_1:def 8;

      end;

    end

    registration

      let X be with_non-empty_elements set;

      cluster -> with_non-empty_elements for Subset of X;

      coherence

      proof

        let Y be Subset of X;

         not {} in Y;

        hence thesis by SETFAM_1:def 8;

      end;

    end

    registration

      let U;

      cluster (U * ) -> infinite;

      coherence

      proof

         omega c= ( card (U * )) by CARD_4: 14;

        hence thesis;

      end;

    end

    registration

      let U;

      cluster (U * ) -> with_non-empty_element;

      coherence ;

    end

    registration

      let X be with_non-empty_element set;

      cluster with_non-empty_elements for non empty Subset of X;

      existence

      proof

        set x = the non empty Element of X;

        take IT = {x};

        thus thesis;

      end;

    end

    

     Lm52: p <> {} & p is Y -valued & Y c= (U * ) & Y is with_non-empty_elements implies ((U -multiCat ) . p) <> {}

    proof

      assume p <> {} ;

      then

      reconsider pp = p as non empty FinSequence;

      assume

       A1: p is Y -valued & Y c= (U * ) & Y is with_non-empty_elements;

      then ( rng pp) c= Y & Y c= (U * );

      then

      reconsider YY = Y as with_non-empty_elements non empty Subset of (U * ) by A1;

      reconsider pp as non emptyYY -valued FinSequence by A1;

      pp is (U * ) -valued & not pp is ( {} * ) -valued;

      hence thesis by Th52;

    end;

    theorem :: FOMODEL0:53

    U1 c= U2 & Y c= (U1 * ) & p is Y -valued & p <> {} & Y is with_non-empty_elements implies ((U1 -multiCat ) . p) = ((U2 -multiCat ) . p)

    proof

      assume U1 c= U2;

      then

      reconsider U11 = U1 as non empty Subset of U2;

      assume Y c= (U1 * );

      then

      reconsider Y1 = Y as Subset of (U11 * );

      reconsider Y2 = Y1 as Subset of (U2 * ) by XBOOLE_1: 1;

      assume p is Y -valued;

      then

      reconsider p1 = p as Y1 -valued FinSequence;

      reconsider p2 = p1 as Y2 -valued FinSequence;

      assume p <> {} & Y is with_non-empty_elements;

      then ((U1 -multiCat ) . p1) <> {} & ((U2 -multiCat ) . p2) <> {} by Lm52;

      hence thesis by Th52;

    end;

    theorem :: FOMODEL0:54

    (ex p st x = p & p is (X * ) -valued) implies ((U -multiCat ) . x) is X -valued

    proof

      set C = (U -multiCat );

      

       A1: ( dom C) = ((U * ) * ) by FUNCT_2:def 1;

      given p such that

       A2: x = p & p is (X * ) -valued;

      x is FinSequence of (X * ) by A2, Lm1;

      then

      reconsider px = x as Element of ((X * ) * );

      per cases ;

        suppose

         A3: (C . p) <> {} ;

        then p in ((U * ) * ) & p <> {} by FUNCT_1:def 2, A1;

        then

        reconsider pp = x as non empty FinSequence of (U * ) by Lm1, A2;

        

         A4: pp is (X * ) -valued & not pp is ( {} * ) -valued by Th52, A2, A3;

        reconsider XX = X as non empty set by Th52, A2, A3;

        set CX = (XX -multiCat );

        reconsider pxx = px as Element of ((XX * ) * );

        (CX . pp) <> {} by Th52, A4;

        hence thesis by Th52, A3, A2;

      end;

        suppose (C . p) = {} ;

        then

        reconsider e = (C . p) as empty set;

        ( rng e) c= X;

        hence thesis by A2;

      end;

    end;

    registration

      let X, m;

      cluster ((m -tuples_on X) \ (X * )) -> empty;

      coherence

      proof

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

        (mm -tuples_on X) c= (X * ) by FINSEQ_2: 134;

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:55

    ((A /\ B) * ) = ((A * ) /\ (B * ))

    proof

      set X = (A /\ B);

      reconsider XA = (A /\ B) as Subset of A;

      reconsider XB = (A /\ B) as Subset of B;

      (XA * ) c= (A * ) & (XB * ) c= (B * );

      then

       A1: (X * ) c= ((A * ) /\ (B * )) by XBOOLE_1: 19;

      now

        let x be object;

        assume

         A2: x in ((A * ) /\ (B * ));

        reconsider pa = x as A -valued FinSequence by A2;

        set m = ( len pa), mA = (m -tuples_on A), mB = (m -tuples_on B), mX = (m -tuples_on X);

        (mX \ (X * )) = {} ;

        then

         A3: mX c= (X * ) by XBOOLE_1: 37;

        reconsider pb = x as B -valued FinSequence by A2;

        pa is m -element & pb is m -element by CARD_1:def 7;

        then pa in mA & pb in mB by Th16;

        then pa in (mA /\ mB) by XBOOLE_0:def 4;

        then pa in mX by Th3;

        hence x in (X * ) by A3;

      end;

      then ((A * ) /\ (B * )) c= (X * );

      hence thesis by A1;

    end;

    theorem :: FOMODEL0:56

    

     Th56: ((P \/ Q) | X) = ((P | X) \/ (Q | X))

    proof

      set R1 = (P | X), R2 = (Q | X), R = (P \/ Q), LH = (R | X), RH = (R1 \/ R2);

      ((P null Q) | X) c= ((P \/ Q) | X) & ((Q null P) | X) c= ((P \/ Q) | X) by RELAT_1: 76;

      then

       A1: RH c= LH by XBOOLE_1: 8;

      now

        let z be object;

        assume

         A2: z in LH;

        then

        consider x,y be object such that

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

        

         A4: x in X & [x, y] in (P \/ Q) by RELAT_1:def 11, A2, A3;

        (x in X & [x, y] in P) or (x in X & [x, y] in Q) by A4, XBOOLE_0:def 3;

        then [x, y] in (P | X) or [x, y] in (Q | X) by RELAT_1:def 11;

        hence z in ((P | X) \/ (Q | X)) by XBOOLE_0:def 3, A3;

      end;

      then LH c= RH;

      hence thesis by A1;

    end;

    registration

      let X;

      cluster (( bool X) \ X) -> non empty;

      coherence

      proof

         not ( bool X) c= X by CARD_1: 25;

        hence thesis by XBOOLE_1: 37;

      end;

    end

    registration

      let X;

      let R be Relation;

      cluster (R null X) -> (X \/ ( dom R)) -defined;

      coherence

      proof

        (( dom R) null X) c= (( dom R) \/ X);

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:57

    

     Th57: ((f | X) +* g) = ((f | (X \ ( dom g))) \/ g)

    proof

      set f1 = (f | (X \ ( dom g))), a1 = g;

      ( dom f1) c= (X \ ( dom a1)) & (X \ ( dom a1)) misses ( dom a1) by XBOOLE_1: 79;

      then

       A1: f1 tolerates a1 by PARTFUN1: 56, XBOOLE_1: 63;

      ((f | X) +* a1) = ((f | ((X \ ( dom a1)) \/ (X /\ ( dom a1)))) +* a1) by Th48

      .= ((f1 +* (f | (X /\ ( dom a1)))) +* a1) by FUNCT_4: 78

      .= (f1 +* ((f | (X /\ ( dom a1))) +* ((a1 null {} ) null ( {} \/ ( dom a1))))) by FUNCT_4: 14

      .= (f1 +* (((f | X) | ( dom a1)) +* (a1 | ( dom a1)))) by RELAT_1: 71

      .= (f1 +* (((f | X) +* a1) | ( dom a1))) by FUNCT_4: 71

      .= (f1 +* a1)

      .= (f1 \/ a1) by A1, FUNCT_4: 30;

      hence thesis;

    end;

    registration

      let X;

      let f be X -defined Function, g be totalX -defined Function;

      identify g null f with f +* g;

      compatibility

      proof

        ( dom g) = X & ( dom f) c= X by PARTFUN1:def 2;

        hence thesis by FUNCT_4: 19;

      end;

      identify f +* g with g null f;

      compatibility ;

    end

    theorem :: FOMODEL0:58

    

     Th58: not y in ( proj2 X) implies [:A, {y}:] misses X

    proof

      set X2 = ( proj2 X), Y = [:A, {y}:], Z = (X /\ Y);

      assume

       A1: not y in X2;

      assume Y meets X;

      then Z <> {} ;

      then

      consider z be object such that

       A2: z in Z;

      set x1 = (z `1 ), y1 = (z `2 );

      x1 in A & y1 in {y} & z = [x1, y1] & z in X by A2, MCART_1: 10, MCART_1: 21;

      then y1 = y & y1 in X2 by TARSKI:def 1, XTUPLE_0:def 13;

      hence contradiction by A1;

    end;

    definition

      let X;

      :: FOMODEL0:def26

      func X -freeCountableSet -> set equals [: NAT , { the Element of (( bool ( proj2 X)) \ ( proj2 X))}:];

      coherence ;

    end

    theorem :: FOMODEL0:59

    

     Th59: ((X -freeCountableSet ) /\ X) = {} & (X -freeCountableSet ) is infinite

    proof

      set X2 = ( proj2 X), Y = (( bool X2) \ X2), y = the Element of Y, IT = (X -freeCountableSet );

       not y in X2 by XBOOLE_0:def 5;

      hence (IT /\ X) = {} by XBOOLE_0:def 7, Th58;

      thus thesis;

    end;

    registration

      let X;

      cluster (X -freeCountableSet ) -> infinite;

      coherence ;

    end

    registration

      let X;

      cluster ((X -freeCountableSet ) /\ X) -> empty;

      coherence by Th59;

    end

    registration

      let X;

      cluster (X -freeCountableSet ) -> countable;

      coherence by CARD_4: 7;

    end

    registration

      cluster ( NAT \ INT ) -> empty;

      coherence

      proof

        set X = ( NAT null ( [: { 0 }, NAT :] \ { [ 0 , 0 ]}));

        reconsider XX = X as Subset of INT ;

        (XX \ INT ) = {} ;

        hence thesis;

      end;

    end

    registration

      let x, p;

      cluster ((( <*x*> ^ p) . 1) \+\ x) -> empty;

      coherence

      proof

        (( <*x*> ^ p) . 1) = x by FINSEQ_1: 41;

        hence thesis;

      end;

    end

    registration

      let m;

      let m0 be zero number;

      let p be m -element FinSequence;

      cluster (p null m0) -> total;

      coherence

      proof

        reconsider l = ( len p) as Element of NAT ;

        ( dom p) = ( Seg l) by FINSEQ_1:def 3

        .= ( Seg m) by CARD_1:def 7;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let U, q1, q2;

      cluster (((U -multiCat ) . <*q1, q2*>) \+\ (q1 ^ q2)) -> empty;

      coherence

      proof

        reconsider f = (U -concatenation ) as BinOp of (U * );

        q1 is FinSequence of U by Lm1;

        then

        reconsider q11 = q1 as Element of (U * );

        set F = ( MultPlace f), p = <*q11*>, C = (U -multiCat );

        (C . <*q1, q2*>) = ((C . p) ^ q2) by Th33

        .= ((F . p) ^ q2) by Th32

        .= (q1 ^ q2) by Lm15;

        hence thesis;

      end;

    end

    registration

      let f;

      let e be empty set;

      identify f null e with f +* e;

      compatibility ;

      identify f +* e with f null e;

      compatibility ;

      identify f null e with e +* f;

      compatibility ;

      identify e +* f with f null e;

      compatibility ;

    end

    registration

      let X be infinite set;

      cluster denumerable for Subset of X;

      existence

      proof

        consider Y such that

         A1: Y c= X & ( card Y) = omega by CARD_3: 87;

        reconsider YY = Y as Subset of X by A1;

        take YY;

        thus YY is denumerable by A1, CARD_3:def 15;

      end;

    end

    registration

      let X be countable finite-membered set;

      cluster ( union X) -> countable;

      coherence

      proof

        for Y st Y in X holds Y is countable;

        hence thesis by CARD_4: 12;

      end;

    end

    registration

      let X be countable finite-membered functional set;

      cluster ( SymbolsOf X) -> countable;

      coherence

      proof

        deffunc F( Relation) = ( rng $1);

        defpred P[ set] means $1 in X;

        reconsider A = (X \/ { {} }) as non empty finite-membered functional set;

        set IT = { F(x) where x be Element of A : P[x] };

         A1:

        now

          let y;

          assume y in IT;

          then

          consider x be Element of A such that

           A2: y = F(x) & P[x];

          thus y is finite by A2;

        end;

        ( card IT) c= ( card X) from TREES_2:sch 2;

        then

        reconsider ITT = IT as countable finite-membered set by A1, FINSET_1:def 6, WAYBEL12: 1;

        ( union ITT) = ( SymbolsOf X);

        hence thesis;

      end;

    end

    registration

      let A,B be countable set;

      cluster (A \/ B) -> countable;

      coherence by CARD_2: 85;

    end

    theorem :: FOMODEL0:60

    

     Th60: ( union X) c= Y implies X c= ( bool Y)

    proof

      assume

       A1: ( union X) c= Y & not X c= ( bool Y);

      then

      consider A be object such that

       A2: A in X & not A in ( bool Y);

      reconsider AA = A as set by TARSKI: 1;

      AA c= Y by A2, A1, SETFAM_1: 41;

      hence contradiction by A2;

    end;

    theorem :: FOMODEL0:61

    

     Th61: for X be set holds A is_finer_than B & X is_finer_than Y implies (A \/ X) is_finer_than (B \/ Y)

    proof

      let X be set;

      set LH = (A \/ X), RH = (B \/ Y);

      assume

       A1: A is_finer_than B & X is_finer_than Y;

      now

        let Z be set;

        assume

         A2: Z in LH;

        per cases by XBOOLE_0:def 3, A2;

          suppose Z in A;

          then

          consider b be set such that

           A3: b in B & Z c= b by SETFAM_1:def 2, A1;

          take b;

          thus b in RH by A3, XBOOLE_0:def 3;

          thus Z c= b by A3;

        end;

          suppose Z in X;

          then

          consider y be set such that

           A4: y in Y & Z c= y by SETFAM_1:def 2, A1;

          take y;

          thus y in RH by A4, XBOOLE_0:def 3;

          thus Z c= y by A4;

        end;

      end;

      hence thesis by SETFAM_1:def 2;

    end;

    theorem :: FOMODEL0:62

    

     Th62: A is_finer_than B implies (A \/ B) is_finer_than B

    proof

      assume A is_finer_than B;

      then (A \/ B) is_finer_than (B \/ B) by Th61;

      hence thesis;

    end;

    theorem :: FOMODEL0:63

    

     Th63: B is c=directed & A is_finer_than B implies (A \/ B) is c=directed

    proof

      assume

       A1: B is c=directed & A is_finer_than B;

      reconsider BB = B as c=directed set by A1;

      reconsider X = (A \/ BB) as non empty set;

      now

        let a,b be set;

        assume a in X;

        then

        consider aa be set such that

         A2: aa in B & a c= aa by SETFAM_1:def 2, A1, Th62;

        assume b in X;

        then

        consider bb be set such that

         A3: bb in B & b c= bb by SETFAM_1:def 2, A1, Th62;

        consider cc be set such that

         A4: (aa \/ bb) c= cc & cc in B by A1, A2, A3, COHSP_1: 5;

        take cc;

        (a \/ b) c= (aa \/ bb) by A2, A3, XBOOLE_1: 13;

        hence (a \/ b) c= cc by A4;

        thus cc in X by A4, XBOOLE_0:def 3;

      end;

      hence (A \/ B) is c=directed by COHSP_1: 6;

    end;

    theorem :: FOMODEL0:64

    

     Th64: ( INTERSECTION (X,Y)) is_finer_than X

    proof

      now

        let xy be set;

        assume xy in ( INTERSECTION (X,Y));

        then

        consider x, y such that

         A1: x in X & y in Y & xy = (x /\ y) by SETFAM_1:def 5;

        take x;

        thus x in X & xy c= x by A1;

      end;

      hence thesis by SETFAM_1:def 2;

    end;

    theorem :: FOMODEL0:65

    Y is c=directed implies for X be finite Subset of ( union Y) holds ex y st y in Y & X c= y

    proof

      set F = Y;

      assume

       A1: F is c=directed;

      let X be finite Subset of ( union F);

      (X /\ ( union F)) = ( union ( INTERSECTION ( {X},F))) by SETFAM_1: 25;

      then

      reconsider FF = ( INTERSECTION ( {X},F)) as finite Subset-Family of X by Th60;

      

       A2: (X null ( union F)) = ( union FF) by SETFAM_1: 25;

      (F \/ FF) is c=directed & (FF null F) c= (F \/ FF) by Th63, Th64, A1;

      then

      consider a be set such that

       A3: ( union FF) c= a & a in (F \/ FF) by COHSP_1:def 4;

      a in F or (a in FF & FF is_finer_than F) by A3, Th64, XBOOLE_0:def 3;

      then

      consider b be set such that

       A4: b in F & a c= b by SETFAM_1:def 2;

      take b;

      thus b in F & X c= b by A2, A3, A4;

    end;

    

     Lm53: X is Subset of ( Funcs (A,B)) implies X is Subset-Family of [:A, B:]

    proof

      

       A1: ( Funcs (A,B)) c= ( bool [:A, B:]) by FRAENKEL: 2;

      assume X is Subset of ( Funcs (A,B));

      hence thesis by A1, XBOOLE_1: 1;

    end;

    theorem :: FOMODEL0:66

    X is Subset of ( Funcs (A,B)) implies X is Subset-Family of [:A, B:] by Lm53;

    

     Lm54: for x,y be Element of U st x in Y iff y in Y holds [(( chi (Y,U)) . x), (( chi (Y,U)) . y)] in ( id BOOLEAN )

    proof

      let x,y be Element of U;

      set f = ( chi (Y,U));

      assume

       A1: x in Y iff y in Y;

      per cases ;

        suppose x in Y;

        then (f . x) = 1 & y in Y by A1, RFUNCT_1: 63;

        then (f . x) = 1 & (f . y) = 1 & 1 in BOOLEAN by RFUNCT_1: 63;

        hence thesis by RELAT_1:def 10;

      end;

        suppose not x in Y;

        then (f . x) = 0 & not y in Y by A1, RFUNCT_1: 64;

        then (f . x) = 0 & (f . y) = 0 & 0 in BOOLEAN by RFUNCT_1: 64;

        hence thesis by RELAT_1:def 10;

      end;

    end;

    theorem :: FOMODEL0:67

    for x,y be Element of U st x in Y iff y in Y holds [(( chi (Y,U)) . x), (( chi (Y,U)) . y)] in ( id BOOLEAN ) by Lm54;

    definition

      let A, R;

      :: FOMODEL0:def27

      func R typed| A -> Subset of R equals (R | A);

      coherence by RELAT_1: 59;

    end

    registration

      let A, R;

      identify R | A with R typed| A;

      compatibility ;

      identify R typed| A with R | A;

      compatibility ;

    end

    

     Lm55: (R | (A \ B)) = ((R | A) \ [:B, ( rng R):])

    proof

      set lh = (R | (A \ B)), rh = ((R | A) \ [:B, ( rng R):]);

      lh = ((R | A) \ (R | B)) by RELAT_1: 80

      .= ((R | A) \ (R /\ [:B, ( rng R):])) by RELAT_1: 67

      .= ((((R | A) null R) \ R) \/ rh) by XBOOLE_1: 54

      .= ( {} \/ rh);

      hence thesis;

    end;

    

     Lm56: (f +* g) = ((f \ [:( dom g), ( rng f):]) \/ g)

    proof

      set df = ( dom f), dg = ( dom g), rf = ( rng f);

      ((f | df) +* g) = ((f | (df \ dg)) \/ g) by Th57

      .= (((f | df) \ [:dg, rf:]) \/ g) by Lm55;

      hence thesis;

    end;

    

     Lm57: (A /\ C) = (A \ ((A \/ B) \ C))

    proof

      set Y = (A \/ B);

      (A \ (Y \ C)) = (((A null B) \ Y) \/ (A /\ C)) by XBOOLE_1: 52

      .= ( {} \/ (A /\ C));

      hence thesis;

    end;

    registration

      let A, B, C;

      cluster ((A \ ((A \/ B) \ C)) \+\ (A /\ C)) -> empty;

      coherence by Lm57, Th29;

    end

    definition

      let X;

      let P be set;

      :: FOMODEL0:def28

      func P |1 X -> set equals (P /\ [:X, ( proj2 P):]);

      coherence ;

    end

    registration

      let X, P;

      identify P | X with P |1 X;

      compatibility by RELAT_1: 67;

      identify P |1 X with P | X;

      compatibility ;

    end

    

     Lm58: (P | (( dom P) \ X)) = (P \ [:X, ( rng P):])

    proof

      set A = ( dom P), B = ( rng P), C = [:(A \ X), B:];

      (P \ [:A, B:]) = {} ;

      then

      reconsider P as Subset of [:A, B:] by Th29;

      ((P \ ((P \/ [:A, B:]) \ C)) \+\ (P /\ C)) = {} & (( [:A, B:] \ (( [:A, B:] \/ {} ) \ [:X, B:])) \+\ ( [:A, B:] /\ [:X, B:])) = {} ;

      then

       A1: (P \ (( [:A, B:] null P) \ C)) = (P /\ C) & ( [:A, B:] \ ( [:A, B:] \ [:X, B:])) = ( [:A, B:] /\ [:X, B:]) by Th29;

      (P | (A \ X)) = (P \ ( [:A, B:] /\ [:X, B:])) by A1, ZFMISC_1: 102

      .= ((P \ [:A, B:]) \/ (P \ [:X, B:])) by XBOOLE_1: 54

      .= ( {} \/ (P \ [:X, B:]));

      hence thesis;

    end;

    definition

      let P, Q;

      :: FOMODEL0:def29

      func P +*1 Q equals ((P \ [:( dom Q), ( rng P):]) \/ Q);

      coherence ;

      :: FOMODEL0:def30

      func P +*2 Q equals ((P | (( dom P) \ ( dom Q))) \/ Q);

      coherence ;

      :: FOMODEL0:def31

      func P +*3 Q equals (((P | ( dom P)) \ (P | ( dom Q))) \/ Q);

      coherence ;

    end

    registration

      let P, Q;

      identify P +*2 Q with P +*1 Q;

      compatibility by Lm58;

      identify P +*3 Q with P +*2 Q;

      compatibility by RELAT_1: 80;

    end

    registration

      let f, g;

      identify f +*1 g with f +* g;

      compatibility by Lm56;

      identify f +* g with f +*1 g;

      compatibility ;

    end

    registration

      let U be non empty set, u be Element of U, q be U -valued FinSequence;

      set f = (U -firstChar ), p = <*u*>, P = (p ^ q);

      cluster (((U -firstChar ) . ( <*u*> ^ q)) \+\ u) -> empty;

      coherence

      proof

        ((P . 1) \+\ u) = {} ;

        

        then u = (P . 1) by Th29

        .= (f . P) by Th6;

        hence thesis;

      end;

    end

    registration

      cluster negative integer for Real;

      existence

      proof

        take ( - 1);

        thus thesis;

      end;

      cluster positive -> natural for Integer;

      coherence ;

    end

    registration

      let X, Y;

      let x be Subset of X, y be Subset of Y;

      cluster ((x \ Y) \ (X \ y)) -> empty;

      coherence

      proof

        (x \ Y) c= (X \ y) by XBOOLE_1: 35;

        hence thesis;

      end;

    end

    registration

      let X, Y;

      let x be Subset of X, y be Subset of Y;

      cluster ((x \ Y) \ (X \ y)) -> empty;

      coherence ;

    end

    registration

      let X, Y;

      let x be Subset of X;

      cluster ((x \ Y) \ (X \ Y)) -> empty;

      coherence

      proof

        ((x \ Y) \ (X \ (Y /\ Y))) = {} ;

        hence thesis;

      end;

    end

    registration

      let X, Y;

      let x be Subset of X, y be Subset of Y;

      cluster (((x \/ y) \ Y) \ X) -> empty;

      coherence

      proof

        ((x \/ y) \ Y) = ((x \ Y) \/ (y \ Y)) by XBOOLE_1: 42

        .= (x \ Y);

        hence thesis;

      end;

    end

    theorem :: FOMODEL0:68

    (( dom f) c= ( dom R) & R c= f) implies R = f by Lm42;

    begin

    registration

      let T be trivial set, x,y be Element of T;

      cluster (x \+\ y) -> empty;

      coherence

      proof

        set t = the Element of T;

        per cases ;

          suppose T = {} ;

          then x = {} & y = {} by SUBSET_1:def 1;

          hence thesis;

        end;

          suppose T <> {} ;

          then

          consider t be object such that

           A1: T = {t} by ZFMISC_1: 131;

          x = t by A1, TARSKI:def 1

          .= y by A1, TARSKI:def 1;

          hence thesis;

        end;

      end;

    end

    scheme :: FOMODEL0:sch2

    FraenkelTrivial { E() -> trivial set , F( object) -> object , P[ set, set] } :

{ F(x) where x be Element of E() : P[x, E()] } c= {F()};

      set e = the Element of E(), LH = { F(x) where x be Element of E() : P[x, E()] }, RH = {F(e)};

      let z be object;

      assume z in LH;

      then

      consider x be Element of E() such that

       A1: z = F(x) & P[x, E()];

      (x \+\ e) = {} ;

      then z = F(e) by A1, Th29;

      hence z in RH by TARSKI:def 1;

    end;

    scheme :: FOMODEL0:sch3

    OnSingleTonsGen { X() -> set , F( set) -> set , P[ set] } :

{ [o, F(o)] where o be Element of X() : P[o] } is Function;

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

      defpred Q[ set, set] means P[$1];

      per cases ;

        suppose X() is non empty;

        then

        reconsider XX = X() as non empty set;

        { [o, F(o)] where o be Element of XX : P[o] } is Function from ALTCAT_2:sch 1;

        hence thesis;

      end;

        suppose X() is empty;

        then

        reconsider XX = X() as trivial set;

        { G(o) where o be Element of XX : Q[o, XX] } c= { G()} from FraenkelTrivial;

        hence thesis;

      end;

    end;

    scheme :: FOMODEL0:sch4

    FraenkelInclusion { X() -> set , F( set, set) -> set , P[ set, set] } :

X() c= { F(x,X) where x be Element of X() : P[x, X()] }

      provided

       A1: for y be set st y in X() holds ex x be set st x in X() & P[x, X()] & y = F(x,X);

      set Y = { F(z,X) where z be Element of X() : P[z, X()] };

      let y be object;

      assume y in X();

      then

      consider x be set such that

       A2: x in X() & P[x, X()] & y = F(x,X) by A1;

      thus y in Y by A2;

    end;

    scheme :: FOMODEL0:sch5

    FraenkelInclusion2 { X() -> set , P[ set, set] } :

X() c= { x where x be Element of X() : P[x, X()] }

      provided

       A1: for x be set st x in X() holds P[x, X()];

      deffunc F( set, set) = $1;

      set Y = { F(x,X) where x be Element of X() : P[x, X()] };

      

       A2: for y be set st y in X() holds ex x be set st x in X() & P[x, X()] & y = F(x,X) by A1;

      X() c= Y from FraenkelInclusion( A2);

      hence thesis;

    end;

    scheme :: FOMODEL0:sch6

    FraenkelEq { X() -> non empty set , P[ set] } :

X() = { x where x be Element of X() : P[x] }

      provided

       A1: for x be set st x in X() holds P[x];

      set Y = { x where x be Element of X() : P[x] };

      

       A2: Y c= X() from FRAENKEL:sch 10;

      defpred Q[ set, set] means P[$1];

      set Z = { x where x be Element of X() : Q[x, X()] };

      

       A3: for x be set st x in X() holds Q[x, X()] by A1;

      X() c= Z from FraenkelInclusion2( A3);

      hence thesis by A2;

    end;

    begin

    registration

      let Y be set, X be Subset of Y;

      cluster (( proj1 X) \ ( proj1 Y)) -> empty;

      coherence by XTUPLE_0: 8, Th29;

      cluster (( proj2 X) \ ( proj2 Y)) -> empty;

      coherence by XTUPLE_0: 9, Th29;

    end

    registration

      let X, Y;

      cluster (( proj1 [:X, Y:]) \ X) -> empty;

      coherence by FUNCT_5: 10, Th29;

      cluster ((( proj1 [:X, Y:]) /\ X) \+\ ( proj1 [:X, Y:])) -> empty;

      coherence

      proof

        set LH = ( proj1 [:X, Y:]);

        (LH \ X) = {} ;

        then

        reconsider LH as Subset of X by Th29;

        (LH /\ X) = (LH null X);

        hence thesis;

      end;

      cluster (( proj2 [:X, Y:]) \ Y) -> empty;

      coherence by FUNCT_5: 10, Th29;

      cluster ((( proj2 [:X, Y:]) /\ Y) \+\ ( proj2 [:X, Y:])) -> empty;

      coherence

      proof

        set LH = ( proj2 [:X, Y:]);

        (LH \ Y) = {} ;

        then

        reconsider LH as Subset of Y by Th29;

        (LH /\ Y) = (LH null Y);

        hence thesis;

      end;

      cluster ((( proj2 X) \/ ( proj2 Y)) \+\ ( proj2 (X \/ Y))) -> empty;

      coherence by XTUPLE_0: 27, Th29;

      cluster ((( proj1 X) \/ ( proj1 Y)) \+\ ( proj1 (X \/ Y))) -> empty;

      coherence by XTUPLE_0: 23, Th29;

      let y be Subset of Y;

      cluster ((X \ Y) /\ y) -> empty;

      coherence

      proof

        ((X \ Y) /\ (Y /\ y)) = {} ;

        hence thesis;

      end;

    end

    registration

      let X;

      let U be non empty set;

      cluster (( proj1 [:X, U:]) \+\ X) -> empty;

      coherence

      proof

        ( proj1 [:X, U:]) = X by FUNCT_5: 9;

        hence thesis;

      end;

      cluster (( proj2 [:U, X:]) \+\ X) -> empty;

      coherence

      proof

        ( proj2 [:U, X:]) = X by FUNCT_5: 9;

        hence thesis;

      end;

    end

    registration

      let X;

      let Y be non empty set;

      reduce ( proj1 [:X, Y:]) to X;

      reducibility

      proof

        (( proj1 [:X, Y:]) \+\ X) = {} ;

        hence thesis by Th29;

      end;

      reduce ( proj2 [:Y, X:]) to X;

      reducibility

      proof

        (( proj2 [:Y, X:]) \+\ X) = {} ;

        hence thesis by Th29;

      end;

    end

    registration

      let R, X;

      cluster ((R .: X) \ ( rng R)) -> empty;

      coherence by RELAT_1: 111, Th29;

    end

    registration

      let A, B, X, Y;

      cluster ( [:A, B:] \ [:(A \/ X), (B \/ Y):]) -> empty;

      coherence

      proof

        (A null X) c= (A \/ X) & (B null Y) c= (B \/ Y);

        hence thesis by ZFMISC_1: 96, Th29;

      end;

    end

    registration

      let X, Y, Z;

      cluster (((X /\ Y) /\ Z) \+\ (X /\ (Y /\ Z))) -> empty;

      coherence by Th29, XBOOLE_1: 16;

    end

    registration

      let X, Y;

      reduce ((X \ Y) \/ (X /\ Y)) to X;

      reducibility by Th48;

    end

    registration

      let P;

      let X be Subset of ( dom P);

      reduce ( dom (P | X)) to X;

      reducibility by RELAT_1: 62;

    end

    registration

      let X;

      let x,y be Subset of X;

      cluster ((x \/ y) \ X) -> empty;

      coherence ;

    end

    registration

      let X;

      cluster ( id X) -> onto;

      coherence ;

    end

    registration

      cluster symmetric -> involutive for Function;

      coherence

      proof

        let g;

        set G = ( field g), D = ( dom g), C = ( rng g);

        assume g is symmetric;

        then

         A1: g is_symmetric_in G by RELAT_2:def 11;

        now

          let x;

          set y = (g . x);

          assume

           A2: x in (D null C);

          then y in (C null D) & [x, y] in g by FUNCT_1: 3, FUNCT_1:def 2;

          then [y, x] in g by A2, A1, RELAT_2:def 3;

          hence x = (g . y) by FUNCT_1: 1;

        end;

        hence thesis by PARTIT_2:def 2;

      end;

    end

    registration

      cluster non empty involutive for Function;

      existence

      proof

        take ( id 1);

        thus thesis;

      end;

    end

    registration

      let f be non empty involutive Function;

      let x be Element of ( dom f);

      reduce (f . (f . x)) to x;

      reducibility by PARTIT_2:def 2;

    end

    registration

      let X, Y;

      cluster [:X, Y:] -> Y -valued;

      coherence

      proof

        (( rng [:X, Y:]) \ Y) = {} ;

        hence thesis by Th29;

      end;

    end

    registration

      let x, y;

      cluster ( [: {x}, {y}:] +* [: {y}, {x}:]) -> symmetric;

      coherence

      proof

        set a = y, b = x, f = ((x,y) --> (a,b));

        reconsider R = f as Relation;

        per cases ;

          suppose x = y;

          then

           A1: f = { [x, x]} by ZFMISC_1: 29;

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

          hence thesis by A1, Th29;

        end;

          suppose

           A2: x <> y;

          

           A3: f = ( [: {x}, {a}:] +* [: {y}, {b}:])

          .= (( [: {x}, {a}:] | {x}) \/ [: {y}, {b}:]) by ZFMISC_1: 14, A2

          .= ( [: {x}, {a}:] \/ [: {y}, {b}:]);

          (R ~ ) = (( [: {x}, {a}:] ~ ) \/ ( [: {y}, {b}:] ~ )) by RELAT_1: 23, A3

          .= (( [: {x}, {a}:] ~ ) \/ [: {b}, {y}:]) by SYSREL: 5

          .= R by A3, SYSREL: 5;

          hence thesis by RELAT_2: 13;

        end;

      end;

    end

    registration

      let X, P;

      let x be Subset of X;

      cluster ((P " x) \ (P " X)) -> empty;

      coherence by RELAT_1: 143, Th29;

    end

    registration

      let X, P;

      cluster ((P " (X \/ ( rng P))) \+\ ( dom P)) -> empty;

      coherence

      proof

        set D = ( dom P), C = ( rng P), XX = (X \/ C);

        ((P " (C null X)) \ (P " XX)) = {} ;

        then (P " C) c= (P " XX) by Th29;

        then D c= (P " XX) & (P " XX) c= D by RELAT_1: 134, RELAT_1: 132;

        hence thesis by XBOOLE_0:def 10, Th29;

      end;

    end

    registration

      let X;

      let R be totalX -defined Relation;

      cluster (X \+\ ( dom R)) -> empty;

      coherence by PARTFUN1:def 2, Th29;

    end

    registration

      let P be non empty Relation;

      cluster -> pair for Element of P;

      coherence

      proof

        let x be Element of P;

        consider y,z be object such that

         A1: x = [y, z] by RELAT_1:def 1;

        thus thesis by A1;

      end;

    end

    registration

      let X;

      let Y be non empty set;

      let f be Y -valued totalX -defined Function;

      cluster ( {f} \ ( Funcs (X,Y))) -> empty;

      coherence

      proof

        f = f & ( dom f) = X & ( rng f) c= Y by PARTFUN1:def 2;

        then f in ( Funcs (X,Y)) by FUNCT_2:def 2;

        hence thesis by Th29;

      end;

    end

    registration

      let X be non empty set;

      let f be X -valued totalX -defined Function;

      cluster (( rng f) \ ( dom f)) -> empty;

      coherence

      proof

        set D = ( dom f), C = ( rng f);

        D = X & C c= X by PARTFUN1:def 2;

        hence thesis;

      end;

    end

    registration

      let X;

      let Y be Subset of X;

      reduce (( id X) .: Y) to Y;

      reducibility by FUNCT_1: 92;

    end

    registration

      let A, B;

      let a be Subset of A;

      cluster ((a \ (A \ B)) \+\ (a /\ B)) -> empty;

      coherence

      proof

        ((a \ ((A \/ a) \ B)) \+\ (a /\ B)) = {} ;

        hence thesis;

      end;

    end

    definition

      let a, b;

      :: FOMODEL0:def32

      func a doubleton b equals ( {a} \/ {b});

      coherence ;

    end

    registration

      let a, b;

      identify a doubleton b with {a,b};

      compatibility by ENUMSET1: 1;

      identify {a,b} with a doubleton b;

      compatibility ;

      identify b doubleton a with a doubleton b;

      compatibility ;

    end

    definition

      let X, Y;

      :: FOMODEL0:def33

      func X .:1 Y -> set equals ( proj2 (X |1 Y));

      coherence ;

    end

    registration

      let P, X;

      identify P .:1 X with P .: X;

      compatibility by RELAT_1: 115;

      identify P .: X with P .:1 X;

      compatibility ;

    end

    notation

      let P, Q;

      synonym P >*> Q for P * Q;

    end

    notation

      let f, g;

      synonym g <*< f for g * f;

    end

    definition

      let P, Q;

      :: original: +*1

      redefine

      func P +*1 Q -> Subset of (P \/ Q) ;

      coherence

      proof

        set dp = ( dom P), dq = ( dom Q), rp = ( rng P), rq = ( rng Q), R = (P \/ Q);

        reconsider p = (P \ [:dq, rp:]) as Subset of P;

        p c= P & (P null Q) c= (P \/ Q);

        then

        reconsider p as Subset of R by XBOOLE_1: 1;

        reconsider QQ = (Q null P) as Subset of R;

        ((p \/ QQ) \ R) = {} ;

        hence thesis;

      end;

    end

    

     Lm59: for x be Element of [:f, g:] st f <> {} & g <> {} holds (x `1 ) is pair & (x `2 ) is pair

    proof

      set F = [:f, g:], D = ( dom F), C = ( rng F), df = ( dom f), dg = ( dom g), rf = ( rng f), rg = ( rng g);

      let x be Element of F;

      assume f <> {} & g <> {} ;

      then

      reconsider U = [: [:df, dg:], [:rf, rg:]:] as non empty Relation;

      

       A1: F c= [:D, C:] & D = [:df, dg:] & C = [:rf, rg:] by FUNCT_3:def 8, RELAT_1: 7, FUNCT_3: 67;

      then

      reconsider F as Function-like Relation-like Subset of U;

      F <> {} by A1;

      then x in F;

      then

      reconsider xx = x as Element of U;

      consider a,b be object such that

       A2: a in [:df, dg:] & b in [:rf, rg:] & xx = [a, b] by ZFMISC_1:def 2;

      reconsider a, b as set by TARSKI: 1;

      thus (x `1 ) is pair & (x `2 ) is pair by A2;

    end;

    registration

      let f,g be non empty Function;

      let x be Element of [:f, g:];

      cluster (x `1 ) -> pair;

      coherence by Lm59;

      cluster (x `2 ) -> pair;

      coherence by Lm59;

    end

    

     Lm60: (P * [:B, C:]) c= [:(P " B), C:]

    proof

      set A = (P " B), R1 = [:B, C:], R2 = [:A, C:], Q = (P * R1);

      

       A1: (( dom R1) \ B) = {} ;

      ( dom Q) = (P " ( dom R1)) by RELAT_1: 147;

      then

      reconsider DQ = ( dom Q) as Subset of A by A1, Th29, RELAT_1: 143;

      ( [:DQ, C:] \ [:(A \/ DQ), (C \/ {} ):]) = {} ;

      then

       A2: [:DQ, C:] c= [:A, C:] by Th29;

      reconsider PP = P as Relation of ( dom P), ( rng P) by RELAT_1: 7;

       [:B, C:] c= [:B, C:];

      then

      reconsider RR1 = [:B, C:] as Relation of B, C;

      reconsider QQ = (PP * RR1) as Relation of ( dom P), C;

       [:( dom Q), ( rng Q):] c= [:( dom Q), C:] & Q c= [:( dom Q), ( rng Q):] by RELAT_1: 7, ZFMISC_1: 95;

      then Q c= [:( dom Q), C:];

      hence Q c= [:A, C:] by A2;

    end;

    

     Lm61: (P * [:B, C:]) = [:(P " B), C:]

    proof

      set A = (P " B), R1 = [:B, C:], R2 = [:A, C:], Q = (P * R1), LH = Q, RH = R2;

      now

        let z be object;

        assume z in RH;

        then

        consider x,y be object such that

         A1: x in A & y in C & z = [x, y] by ZFMISC_1:def 2;

        consider x1 be object such that

         A2: [x, x1] in P & x1 in B by RELAT_1:def 14, A1;

         [x1, y] in [:B, C:] by A1, A2, ZFMISC_1:def 2;

        hence z in LH by A1, A2, RELAT_1:def 8;

      end;

      then RH c= LH & LH c= RH by Lm60;

      hence thesis;

    end;

    

     Lm62: y <> {} & y c= Y implies ( [:X, y:] * [:Y, Z:]) = [:X, Z:]

    proof

      assume y <> {} ;

      then

      reconsider yy = y as non empty set;

      set P = [:X, yy:], Q = [:Y, Z:];

      assume y c= Y;

      then

      reconsider z = ( rng P) as Subset of Y by XBOOLE_1: 1;

      ((P " (Y \/ z)) \+\ ( dom P)) = {} & (( dom P) \+\ X) = {} ;

      then (P " Y) = ( dom P) & ( dom P) = X by Th29;

      hence thesis by Lm61;

    end;

    

     Lm63: (P * [:( rng P), X:]) = [:( dom P), X:]

    proof

      (P * [:( rng P), X:]) = [:(P " ( rng P)), X:] by Lm61;

      hence thesis by RELAT_1: 134;

    end;

    

     Lm64: ( rng f) = ( dom f) implies f is onto Function of ( dom f), ( dom f)

    proof

      set D = ( dom f), C = ( rng f);

      reconsider ff = f as Element of ( Funcs (D,C)) by FUNCT_2:def 2;

      assume

       A1: C = D;

      then

      reconsider fff = ff as Function of D, D by FUNCT_2: 66;

      fff is ontoD -valued by FUNCT_2:def 3, A1;

      hence thesis;

    end;

    

     Lm65: f is involutive implies (f * f) c= ( id ( dom f))

    proof

      assume f is involutive;

      then

      reconsider ff = f as involutive Function;

      set g = (ff * ff), df = ( dom ff), dg = ( dom g), I = ( id df);

      now

        let x;

        assume

         A1: x in dg;

        then

         A2: x in df by RELAT_1: 25, TARSKI:def 3;

        thus x in ( dom I) by RELAT_1: 25, TARSKI:def 3, A1;

        

        thus (I . x) = x by FUNCT_1: 18, A2

        .= (f . (f . x)) by A2, PARTIT_2:def 2

        .= (g . x) by FUNCT_1: 13, A2;

      end;

      hence thesis by Th51;

    end;

    

     Lm66: (X /\ ( id (( proj1 X) /\ ( proj2 X)))) = (X /\ ( id ( proj1 X)))

    proof

      set D = ( proj1 X), C = ( proj2 X), i = ( id (D /\ C)), I = ( id D), R = (X /\ I), r = (X /\ i);

      (X /\ i) = (X /\ (I /\ ( id ( proj2 X)))) & (((X /\ I) /\ ( id ( proj2 X))) \+\ (X /\ (I /\ ( id ( proj2 X))))) = {} by SYSREL: 14;

      then

      reconsider r as Subset of R by Th29;

      now

        let z be object;

        assume

         A1: z in R;

        consider x,y be object such that

         A2: z = [x, y] by RELAT_1:def 1, A1;

        

         A3: x in D & y in C by A1, A2, XTUPLE_0:def 12, XTUPLE_0:def 13;

        

         A4: x = y by A2, A1, RELAT_1:def 10;

        then x in (D /\ C) by A3, XBOOLE_0:def 4;

        then [x, y] in i by A4, RELAT_1:def 10;

        hence z in r by A1, A2, XBOOLE_0:def 4;

      end;

      then R c= r;

      hence thesis;

    end;

    

     Lm67: (( id X) | Y) = ( id (X /\ Y))

    proof

      

       A1: ( dom ( id (X \ Y))) = (X \ Y) & ( dom ( id (X /\ Y))) = (X /\ Y) & ((X \ Y) /\ (Y /\ Y)) = {} & (X /\ Y) c= Y;

      then

       A2: ( dom ( id (X \ Y))) misses Y & ( dom ( id (X /\ Y))) c= Y;

      reconsider i = ( id (X /\ Y)) as Y -defined Function by RELAT_1:def 18, A1;

      X = ((X /\ Y) \/ (X \ Y));

      then ( id X) = (( id (X /\ Y)) \/ ( id (X \ Y))) by SYSREL: 14;

      then (( id X) | Y) = ((( id (X /\ Y)) | Y) \/ (( id (X \ Y)) | Y)) by Th56;

      

      then (( id X) | Y) = ((( id (X /\ Y)) | Y) \/ {} ) by A2, RELAT_1: 152

      .= (i null Y)

      .= i;

      hence thesis;

    end;

    

     Lm68: (( rng f1) /\ ( rng f2)) = {} & b1 <> b2 & ( rng f1) c= ( dom f2) & ( rng f2) c= ( dom f1) implies ( [:( rng f1), {b2}:] \/ [:( rng f2), {b1}:]) c= (((f1 \/ f2) >*> ( [:( rng f1), {b2}:] \/ [:( rng f2), {b1}:])) >*> ((b1,b2) --> (b2,b1)))

    proof

      set A1 = ( dom f1), A2 = ( dom f2), g1 = [:( rng f1), {b2}:], g2 = [:( rng f2), {b1}:], h1 = (b1 .--> b2), h2 = (b2 .--> b1), h = ((b1,b2) --> (b2,b1)), f = (f1 \/ f2), g = (g1 \/ g2);

      assume (( rng f1) /\ ( rng f2)) = {} ;

      then

      reconsider e = (( rng f1) /\ ( rng f2)) as empty set;

      

       A1: (( dom g1) /\ ( rng f2)) = (( dom g1) /\ e)

      .= {} ;

      

       A2: (( dom g2) /\ ( rng f1)) = (( dom g2) /\ e)

      .= {} ;

      

       A3: (((( rng [:A1, {b2}:]) /\ {b2}) /\ {b1}) \+\ (( rng [:A1, {b2}:]) /\ ( {b2} /\ {b1}))) = {} ;

      ((( rng [:A1, {b2}:]) /\ {b2}) \+\ ( rng [:A1, {b2}:])) = {} ;

      

      then

       A4: (( rng [:A1, {b2}:]) /\ {b1}) = ((( rng [:A1, {b2}:]) /\ {b2}) /\ {b1}) by Th29

      .= (( rng [:A1, {b2}:]) /\ ( {b1} /\ {b2})) by A3, Th29;

      (f * g) = ((f >*> g1) \/ (f >*> g2)) by RELAT_1: 32

      .= (((f1 >*> g1) \/ (f2 >*> g1)) \/ (f >*> g2)) by SYSREL: 6

      .= (((f1 >*> g1) \/ (f2 >*> g1)) \/ ((f1 >*> g2) \/ (f2 >*> g2))) by SYSREL: 6

      .= (((f1 >*> g1) \/ (f2 >*> g1)) \/ ( {} \/ (f2 >*> g2))) by A2, XBOOLE_0:def 7, RELAT_1: 44

      .= ((((f1 >*> g1) \/ {} ) \/ {} ) \/ (f2 >*> g2)) by A1, XBOOLE_0:def 7, RELAT_1: 44

      .= ( [:A1, {b2}:] \/ (f2 >*> g2)) by Lm63

      .= ( [:A1, {b2}:] \/ [:A2, {b1}:]) by Lm63;

      

      then

       A5: ((f * g) >*> (h1 \/ h2)) = (( [:A1, {b2}:] >*> (h1 \/ h2)) \/ ( [:A2, {b1}:] >*> (h1 \/ h2))) by SYSREL: 6

      .= ((( [:A1, {b2}:] >*> h1) \/ ( [:A1, {b2}:] >*> h2)) \/ ( [:A2, {b1}:] >*> (h1 \/ h2))) by RELAT_1: 32

      .= ((( [:A1, {b2}:] >*> h1) \/ ( [:A1, {b2}:] >*> h2)) \/ (( [:A2, {b1}:] >*> h1) \/ ( [:A2, {b1}:] >*> h2))) by RELAT_1: 32;

      assume

       A6: b1 <> b2;

      then

       A7: ( {b1} /\ {b2}) = {} by XBOOLE_0:def 7, ZFMISC_1: 11;

      then {} = (( rng [:A1, {b2}:]) /\ ( dom h1)) by A4;

      then

       A8: ((f * g) >*> (h1 \/ h2)) = (( {} \/ ( [:A1, {b2}:] >*> h2)) \/ (( [:A2, {b1}:] >*> h1) \/ ( [:A2, {b1}:] >*> h2))) by RELAT_1: 44, A5, XBOOLE_0:def 7;

      

       A9: ((( rng [:A2, {b1}:]) /\ ( {b1} /\ {b2})) \+\ ((( rng [:A2, {b1}:]) /\ {b1}) /\ {b2})) = {} ;

      ((( rng [:A2, {b1}:]) /\ {b1}) \+\ ( rng [:A2, {b1}:])) = {} ;

      

      then (( rng [:A2, {b1}:]) /\ {b2}) = ((( rng [:A2, {b1}:]) /\ {b1}) /\ {b2}) by Th29

      .= (( rng [:A2, {b1}:]) /\ ( {b1} /\ {b2})) by A9, Th29;

      then (( rng [:A2, {b1}:]) /\ ( dom h2)) = {} by A7;

      then ( [:A2, {b1}:] >*> h2) = {} by RELAT_1: 44, XBOOLE_0:def 7;

      

      then

       A10: ((f * g) >*> (h1 \/ h2)) = (( [:A1, {b2}:] >*> h2) \/ [:((A2 --> b1) " {b1}), {b2}:]) by Lm61, A8

      .= (( [:A1, {b2}:] >*> h2) \/ [:A2, {b2}:]) by FUNCOP_1: 15

      .= ( [:((A1 --> b2) " {b2}), {b1}:] \/ [:A2, {b2}:]) by Lm61

      .= ( [:A1, {b1}:] \/ (A2 --> b2)) by FUNCOP_1: 15;

      assume ( rng f1) c= A2;

      then

      reconsider B1 = ( rng f1) as Subset of A2;

      assume ( rng f2) c= A1;

      then

      reconsider B2 = ( rng f2) as Subset of A1;

      ( [:B1, {b2}:] \ [:(A2 null B1), ( {b2} \/ {} ):]) = {} & ( [:B2, {b1}:] \ [:(A1 null B2), ( {b1} \/ {} ):]) = {} ;

      then

       A11: (B1 --> b2) c= (A2 --> b2) & (B2 --> b1) c= (A1 --> b1) by Th29;

      h = ( [:( {b1} \ {b2}), {b2}:] \/ h2) by ZFMISC_1: 102

      .= (h1 \/ h2) by A6, ZFMISC_1: 11, XBOOLE_1: 83;

      hence thesis by A11, A10, XBOOLE_1: 13;

    end;

    

     Lm69: a in {a1, (f . a1)} & f is involutive & a1 in ( dom f) implies {a, (f . a)} = {a1, (f . a1)}

    proof

      assume

       A1: a in {a1, (f . a1)} & f is involutive & a1 in ( dom f);

      per cases ;

        suppose a = a1;

        hence thesis;

      end;

        suppose a <> a1;

        then a = (f . a1) by A1, TARSKI:def 2;

        hence {a, (f . a)} = {a1, (f . a1)} by A1, PARTIT_2:def 2;

      end;

    end;

    

     Lm70: ((a in {a1, (f . a1)} or (f . a) in {a1, (f . a1)}) & f is involutive & a in ( dom f) & a1 in ( dom f)) implies {a, (f . a)} = {a1, (f . a1)}

    proof

      set X1 = {a1, (f . a1)}, X = {a, (f . a)};

      assume

       A1: (a in X1 or (f . a) in X1) & f is involutive & a in ( dom f) & a1 in ( dom f);

      assume

       A2: not thesis;

      

      then {a1, (f . a1)} = {(f . a), (f . (f . a))} by Lm69, A1

      .= {(f . a), a} by A1, PARTIT_2:def 2;

      hence contradiction by A2;

    end;

    

     Lm71: X c= f implies ( dom (f \ X)) = (( dom f) \ ( proj1 X))

    proof

      assume X c= f;

      then

      reconsider g = X as Function-like Relation-like Subset of f;

      set dg = ( dom g), df = ( dom f);

      (f | dg) = g by GRFUNC_1: 23;

      hence thesis by RELAT_1: 177;

    end;

    

     Lm72: X <> {} implies the set of all x where x be Element of X = X

    proof

      assume X <> {} ;

      then

      reconsider XX = X as non empty set;

      defpred P[ set] means not contradiction;

      

       A1: for x st x in XX holds P[x];

      set Y = { x where x be Element of XX : P[x] };

      XX = Y from FraenkelEq( A1);

      hence thesis;

    end;

    

     Lm73: [ [a1, a2], [b1, b2]] in [:f, g:] iff ( [a1, b1] in f & [a2, b2] in g)

    proof

      set a = [a1, a2], b = [b1, b2], F = [:f, g:];

      thus [a, b] in F implies [a1, b1] in f & [a2, b2] in g

      proof

        assume

         A1: [a, b] in F;

        then

        reconsider F as non empty Function;

        set D = ( dom F), C = ( rng F);

        F <> {} ;

        then

        reconsider ff = f, gg = g as non empty Function;

        set df = ( dom ff), dg = ( dom gg), rf = ( rng ff), rg = ( rng gg);

        reconsider ff as Function of df, rf by FUNCT_2: 1;

        reconsider gg as Function of dg, rg by FUNCT_2: 1;

        

         A2: a in D & b = ( [:ff, gg:] . (a1,a2)) by FUNCT_1: 1, A1;

        reconsider aa = a as Element of D by FUNCT_1: 1, A1;

        reconsider aaa = aa as Element of [:df, dg:] by FUNCT_3:def 8;

        

         A3: ( {(aaa `1 )} \ df) = {} & ( {(aaa `2 )} \ dg) = {} & (a `1 ) = a1 & (a `2 ) = a2;

        reconsider a1 as Element of df by A3;

        reconsider a2 as Element of dg by A3;

        b = [(ff . a1), (gg . a2)] & ( [(ff . a1), (gg . a2)] `1 ) = (ff . a1) & (b `1 ) = b1 & ( [(ff . a1), (gg . a2)] `2 ) = (gg . a2) & (b `2 ) = b2 by A2, FUNCT_3: 75;

        hence thesis by FUNCT_1:def 2;

      end;

      assume

       A4: [a1, b1] in f & [a2, b2] in g;

      then

      reconsider ff = f, gg = g as non empty Function;

      set df = ( dom f), dg = ( dom g);

      a1 in df & b1 = (ff . a1) & a2 in dg & b2 = (gg . a2) by FUNCT_1: 1, A4;

      

      then [b1, b2] = (F . (a1,a2)) by FUNCT_3:def 8

      .= (F . [a1, a2]);

      then (F . [a1, a2]) = [b1, b2] & [a1, a2] in ( dom F) by FUNCT_1:def 2;

      hence thesis by FUNCT_1:def 2;

    end;

    

     Lm74: X = Y iff for x st x in (X \/ Y) holds (x in X iff x in Y)

    proof

      set Z = (X \/ Y);

      defpred W[ object] means $1 in X iff $1 in Y;

      thus X = Y implies for x st x in Z holds W[x];

      assume

       A1: for x st x in Z holds W[x];

      now

        let x be object;

        per cases ;

          suppose x in Z;

          hence W[x] by A1;

        end;

          suppose not x in Z;

          hence W[x] by XBOOLE_0:def 3;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm75: x in [:f, g:] implies x = [ [((x `1 ) `1 ), ((x `1 ) `2 )], [((x `2 ) `1 ), ((x `2 ) `2 )]]

    proof

      set F = [:f, g:], y = (x `1 ), z = (x `2 ), x1 = (y `1 ), x2 = (y `2 ), x3 = (z `1 ), x4 = (z `2 );

      assume

       A1: x in F;

      then

      reconsider F as non empty Function;

      F <> {} ;

      then

      reconsider ff = f as non empty Function;

      F <> {} ;

      then

      reconsider gg = g as non empty Function;

      reconsider F = [:ff, gg:] as non empty Function by A1;

      reconsider xx = x as Element of F by A1;

      reconsider y = (xx `1 ), z = (xx `2 ) as pair object;

      y = [(y `1 ), (y `2 )] & z = [(z `1 ), (z `2 )] & xx = [(xx `1 ), (xx `2 )];

      hence thesis;

    end;

    

     Lm76: ( [:f1, f2:] /\ [:g1, g2:]) = [:(f1 /\ g1) qua Function, (f2 /\ g2) qua Function:]

    proof

      set H1 = (f1 /\ g1), H2 = (f2 /\ g2), F = [:f1, f2:], G = [:g1, g2:], lh = (F /\ G);

      reconsider H1, H2 as Function;

      set rh = [:H1, H2:];

      now

        let x;

        set y = (x `1 ), z = (x `2 ), x1 = (y `1 ), x2 = (y `2 ), x3 = (z `1 ), x4 = (z `2 ), xx = [ [x1, x2], [x3, x4]];

        xx in lh iff xx in F & xx in G by XBOOLE_0:def 4;

        then xx in lh iff ( [x1, x3] in f1 & [x1, x3] in g1 & [x2, x4] in f2 & [x2, x4] in g2) by Lm73;

        then xx in lh iff ( [x1, x3] in (f1 /\ g1) & [x2, x4] in (f2 /\ g2)) by XBOOLE_0:def 4;

        then

         A1: xx in lh iff xx in rh by Lm73;

        assume x in (lh \/ rh);

        thus x in lh iff x in rh by A1, Lm75;

      end;

      hence thesis by Lm74;

    end;

    begin

    definition

      let P;

      :: FOMODEL0:def34

      attr P is oneone means

      : Def34: (P ~ ) is Function-like;

    end

    registration

      cluster one-to-one -> oneone for Function;

      coherence ;

      cluster oneone -> one-to-one for Function;

      coherence

      proof

        let f be Function;

        set D = ( dom f);

        assume f is oneone;

        then

        reconsider g = (f ~ ) as Function;

        now

          let x1,x2 be object;

          assume x1 in D & x2 in D & (f . x1) = (f . x2);

          then [x1, (f . x1)] in f & [x2, (f . x1)] in f by FUNCT_1:def 2;

          then [(f . x1), x1] in g & [(f . x1), x2] in g by RELAT_1:def 7;

          hence x1 = x2 by FUNCT_1:def 1;

        end;

        hence thesis by FUNCT_1:def 4;

      end;

    end

    registration

      cluster oneone for one-to-one Function;

      existence

      proof

        take the one-to-one Function;

        thus thesis;

      end;

    end

    registration

      let P be oneone Relation;

      cluster (P ~ ) -> Function-like;

      coherence by Def34;

    end

    registration

      cluster non empty one-to-one for Function;

      existence

      proof

        take ( id the non empty set);

        thus thesis;

      end;

      let P be oneone Relation;

      cluster -> oneone for Subset of P;

      coherence

      proof

        let Q be Subset of P;

        (Q ~ ) c= (P ~ ) by SYSREL: 11;

        hence thesis;

      end;

    end

    begin

    definition

      let R be set;

      :: FOMODEL0:def35

      func fixpoints R -> set equals ( proj1 (R /\ ( id ( proj1 R))));

      coherence ;

      :: FOMODEL0:def36

      func fixpoints1 R -> set equals ( proj1 (R /\ ( id (( proj1 R) /\ ( proj2 R)))));

      coherence ;

    end

    registration

      let X;

      let R be Subset of ( id X);

      reduce (R ~ ) to R;

      reducibility

      proof

        set RR = ( id (X /\ ( dom R))), I = ( id X);

        

         A1: R = (I | ( dom R)) by GRFUNC_1: 23

        .= RR by Lm67;

        thus thesis by A1;

      end;

    end

    

     Lm77: ( fixpoints1 R) = ( fixpoints1 (R ~ ))

    proof

      set Q = (R ~ ), dq = ( dom Q), dr = ( dom R), rq = ( rng Q), rr = ( rng R), iq = ( id (dq /\ rq)), ir = ( id (dr /\ rr)), r = (R /\ ir), q = (Q /\ iq);

      reconsider r as Subset of ir;

      dq = rr & rq = dr by RELAT_1: 20;

      

      then q = (Q /\ (ir ~ ))

      .= (r ~ ) by RELAT_1: 22

      .= r;

      hence thesis;

    end;

    registration

      let R;

      cluster (( fixpoints1 (R ~ )) \+\ ( fixpoints1 R)) -> empty;

      coherence by Lm77, Th29;

    end

    registration

      let f be one-to-one Function;

      cluster (( fixpoints1 (f " )) \+\ ( fixpoints1 f)) -> empty;

      coherence

      proof

        (f " ) = (f ~ ) by FUNCT_1:def 5;

        hence thesis;

      end;

    end

    registration

      let R be set;

      identify fixpoints1 R with fixpoints R;

      compatibility by Lm66;

      identify fixpoints R with fixpoints1 R;

      compatibility ;

    end

    

     Lm78: for x be object holds x in ( fixpoints f) iff x is_a_fixpoint_of f

    proof

      let x be object;

      set FP = ( fixpoints f), D = ( dom f), I = ( id D);

      reconsider g = (f /\ I) as Function;

      set y = (g . x);

      defpred P[ object] means $1 is_a_fixpoint_of f;

      (FP \ D) = {} & (FP \ ( dom I)) = {} ;

      then

       A1: FP c= D & FP c= ( dom I) by Th29;

      thus x in FP implies P[x]

      proof

        assume

         A2: x in FP;

         [x, y] in g by A2, FUNCT_1:def 2;

        then y = (f . x) & y = (I . x) by FUNCT_1:def 2, A1, A2;

        then (f . x) = x by FUNCT_1: 17, A1, A2;

        hence P[x] by ABIAN:def 3, A1, A2;

      end;

      assume

       A3: P[x];

      then

       A4: x in D & x in ( dom I) & x = (f . x) by ABIAN:def 3;

      x = (f . x) & x = (I . x) by A3, ABIAN:def 3, FUNCT_1: 18;

      then [x, x] in f & [x, x] in I by A4, FUNCT_1:def 2;

      then [x, x] in g by XBOOLE_0:def 4;

      hence x in FP by XTUPLE_0:def 12;

    end;

    registration

      let X;

      reduce ( fixpoints ( id X)) to X;

      reducibility ;

    end

    

     Lm79: ( fixpoints [:f, g:]) = [:( fixpoints f), ( fixpoints g):]

    proof

      set h = [:f, g:], F = ( fixpoints f), G = ( fixpoints g), LH = ( fixpoints h), RH = [:F, G:], df = ( dom f), dg = ( dom g);

      (h /\ ( id ( dom h))) = (h /\ ( id [:df, dg:])) by FUNCT_3:def 8

      .= (h /\ [:( id df), ( id dg):]) by FUNCT_3: 69

      .= [:(f /\ ( id df)), (g /\ ( id dg)):] by Lm76;

      hence LH = RH by FUNCT_3:def 8;

    end;

    registration

      let X be non empty set;

      cluster ( id X) -> with_fixpoint;

      coherence

      proof

        set I = ( id X), x = the Element of X;

        x in ( fixpoints I);

        hence thesis by ABIAN:def 5, Lm78;

      end;

    end

    registration

      let X be non empty set;

      cluster with_fixpoint non empty symmetric for Permutation of X;

      existence

      proof

        take ( id X);

        thus thesis;

      end;

    end

    registration

      cluster with_fixpoint non empty symmetric for Function;

      existence

      proof

        take the with_fixpoint non empty symmetric Permutation of the non empty set;

        thus thesis;

      end;

    end

    registration

      let f be with_fixpoint Function;

      cluster ( dom f) -> non empty;

      coherence

      proof

        consider x be object such that

         A1: x is_a_fixpoint_of f by ABIAN:def 5;

        thus thesis by A1, ABIAN:def 3;

      end;

    end

    registration

      cluster empty -> without_fixpoints for Function;

      coherence

      proof

        ( dom {} ) = {} ;

        hence thesis;

      end;

    end

    registration

      cluster without_fixpoints empty for Function;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      let f be with_fixpoint Function;

      cluster ( fixpoints f) -> non empty;

      coherence

      proof

        consider x be object such that

         A1: x is_a_fixpoint_of f by ABIAN:def 5;

        thus thesis by A1, Lm78;

      end;

    end

    registration

      let f be without_fixpoints Function;

      cluster ( fixpoints f) -> empty;

      coherence by Lm78, ABIAN:def 5;

    end

    begin

    definition

      let X;

      :: FOMODEL0:def37

      attr X is constanT means

      : Def37: ( proj2 X) is trivial;

    end

    registration

      cluster empty -> constanT for set;

      coherence ;

    end

    registration

      cluster empty constanT for Function;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      cluster constant -> constanT for Function;

      coherence ;

      cluster constanT -> constant for Function;

      coherence ;

    end

    

     Lm80: X is non empty trivial & P is X -valued implies P is constant Function

    proof

      assume X is non empty trivial;

      then

      reconsider T = X as non empty trivial set;

      consider t be Element of T such that

       A1: T = {t} by SUBSET_1: 46;

      set d = ( dom P), r = ( rng P);

      reconsider f = [:d, {t}:] as Function;

      assume P is X -valued;

      then

      reconsider r as Subset of {t} by A1;

      ( [:d, r:] \ [:(d \/ {} ), ( {t} null r):]) = {} ;

      then P c= [:d, r:] & [:d, r:] c= f by RELAT_1: 7, Th29;

      then

      reconsider fP = P as Function-like Subset of f by XBOOLE_1: 1;

      (( rng fP) \ ( rng f)) = {} & (( rng f) \ {t}) = {} ;

      then ( rng fP) c= ( rng f) & ( rng f) c= {t} by Th29;

      hence thesis;

    end;

    registration

      let x be trivial set;

      cluster x -valued -> Function-like for Relation;

      coherence

      proof

        let P;

        per cases ;

          suppose

           A1: x = {} ;

          assume P is x -valued;

          hence thesis by A1;

        end;

          suppose

           A2: not x = {} ;

          assume P is x -valued;

          hence thesis by Lm80, A2;

        end;

      end;

    end

    registration

      let x be trivial set;

      cluster x -valued -> constant for Function;

      coherence ;

    end

    registration

      let P;

      let Q be constanT Relation;

      cluster (P * Q) -> constanT;

      coherence

      proof

        set p2 = ( rng P), q2 = ( rng Q), R = (P * Q), r2 = ( rng R);

        r2 c= q2 & q2 is trivial by RELAT_1: 26, Def37;

        hence thesis;

      end;

    end

    registration

      cluster constanT -> Function-like for set;

      coherence

      proof

        let X be set;

        set X2 = ( proj2 X);

        assume

         A1: X is constanT;

        now

          let x,y1,y2 be object;

          set a1 = [x, y1], a2 = [x, y2];

          assume a1 in X & a2 in X;

          then y1 in X2 & y2 in X2 by XTUPLE_0:def 13;

          hence y1 = y2 by A1, ZFMISC_1:def 10;

        end;

        hence thesis by FUNCT_1:def 1;

      end;

    end

    registration

      let P;

      let c be constanT Relation;

      cluster (P >*> c) -> Function-like;

      coherence ;

    end

    registration

      let X, Y;

      let x be trivial set;

      cluster ( [:X, Y:] >*> [:Y, x:]) -> Function-like;

      coherence ;

    end

    theorem :: FOMODEL0:69

    x in ( fixpoints f) iff x is_a_fixpoint_of f by Lm78;

    theorem :: FOMODEL0:70

    a in {a1, (f . a1)} & f is involutive & a1 in ( dom f) implies {a, (f . a)} = {a1, (f . a1)} by Lm69;

    theorem :: FOMODEL0:71

    ((a in {a1, (f . a1)} or (f . a) in {a1, (f . a1)}) & f is involutive & a in ( dom f) & a1 in ( dom f)) implies {a, (f . a)} = {a1, (f . a1)} by Lm70;

    theorem :: FOMODEL0:72

    f is involutive implies (f * f) c= ( id ( dom f)) by Lm65;

    theorem :: FOMODEL0:73

    y <> {} & y c= Y implies ( [:X, y:] * [:Y, Z:]) = [:X, Z:] by Lm62;

    theorem :: FOMODEL0:74

    X <> {} implies the set of all x where x be Element of X = X by Lm72;

    theorem :: FOMODEL0:75

    ( rng f) = ( dom f) implies f is onto Function of ( dom f), ( dom f) by Lm64;

    theorem :: FOMODEL0:76

    ( fixpoints [:f, g:]) = [:( fixpoints f), ( fixpoints g):] by Lm79;

    theorem :: FOMODEL0:77

    (( rng f1) /\ ( rng f2)) = {} & b1 <> b2 & ( rng f1) c= ( dom f2) & ( rng f2) c= ( dom f1) implies ( [:( rng f1), {b2}:] \/ [:( rng f2), {b1}:]) c= (((f1 \/ f2) >*> ( [:( rng f1), {b2}:] \/ [:( rng f2), {b1}:])) >*> ((b1,b2) --> (b2,b1))) by Lm68;

    theorem :: FOMODEL0:78

    X c= f implies ( dom (f \ X)) = (( dom f) \ ( proj1 X)) by Lm71;