pre_poly.miz



    begin

    definition

      let D be set;

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

      :: original: ^

      redefine

      func p ^ q -> Element of (D * ) ;

      coherence

      proof

        (p ^ q) is FinSequence of D;

        hence thesis by FINSEQ_1:def 11;

      end;

    end

    registration

      let D be set;

      cluster empty for Element of (D * );

      existence

      proof

        ( <*> D) is Element of (D * ) by FINSEQ_1:def 11;

        hence thesis;

      end;

    end

    definition

      let D be set;

      :: original: <*>

      redefine

      func <*> D -> empty Element of (D * ) ;

      coherence by FINSEQ_1:def 11;

    end

    definition

      let D be non empty set;

      let d be Element of D;

      :: original: <*

      redefine

      func <*d*> -> Element of (D * ) ;

      coherence

      proof

         <*d*> is FinSequence of D;

        hence thesis by FINSEQ_1:def 11;

      end;

      let e be Element of D;

      :: original: <*

      redefine

      func <*d,e*> -> Element of (D * ) ;

      coherence

      proof

         <*d, e*> = ( <*d*> ^ <*e*>) by FINSEQ_1:def 9;

        hence thesis by FINSEQ_1:def 11;

      end;

    end

    begin

    registration

      let X be set;

      cluster -> FinSequence-like for Element of (X * );

      coherence ;

    end

    definition

      let D be set, F be FinSequence of (D * );

      :: PRE_POLY:def1

      func FlattenSeq F -> Element of (D * ) means

      : Def1: ex g be BinOp of (D * ) st (for p,q be Element of (D * ) holds (g . (p,q)) = (p ^ q)) & it = (g "**" F);

      existence

      proof

        deffunc F( Element of (D * ), Element of (D * )) = ($1 ^ $2);

        consider g be BinOp of (D * ) such that

         A1: for a,b be Element of (D * ) holds (g . (a,b)) = F(a,b) from BINOP_1:sch 4;

        take (g "**" F), g;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Element of (D * );

        given g1 be BinOp of (D * ) such that

         A2: for p,q be Element of (D * ) holds (g1 . (p,q)) = (p ^ q) and

         A3: it1 = (g1 "**" F);

        given g2 be BinOp of (D * ) such that

         A4: for p,q be Element of (D * ) holds (g2 . (p,q)) = (p ^ q) and

         A5: it2 = (g2 "**" F);

        now

          let a,b be Element of (D * );

          

          thus (g1 . (a,b)) = (a ^ b) by A2

          .= (g2 . (a,b)) by A4;

        end;

        hence thesis by A3, A5, BINOP_1: 2;

      end;

    end

    theorem :: PRE_POLY:1

    

     Th1: for D be set, d be Element of (D * ) holds ( FlattenSeq <*d*>) = d

    proof

      let D be set, d be Element of (D * );

      ex g be BinOp of (D * ) st (for p,q be Element of (D * ) holds (g . (p,q)) = (p ^ q)) & ( FlattenSeq <*d*>) = (g "**" <*d*>) by Def1;

      hence thesis by FINSOP_1: 11;

    end;

    theorem :: PRE_POLY:2

    

     Th2: for D be set holds ( FlattenSeq ( <*> (D * ))) = ( <*> D)

    proof

      let D be set;

      consider g be BinOp of (D * ) such that

       A1: for d1,d2 be Element of (D * ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq ( <*> (D * ))) = (g "**" ( <*> (D * ))) by Def1;

      

       A3: {} is Element of (D * ) by FINSEQ_1: 49;

      reconsider p = {} as Element of (D * ) by FINSEQ_1: 49;

      now

        let a be Element of (D * );

        

        thus (g . ( {} ,a)) = ( {} ^ a) by A1, A3

        .= a by FINSEQ_1: 34;

        

        thus (g . (a, {} )) = (a ^ {} ) by A1, A3

        .= a by FINSEQ_1: 34;

      end;

      then

       A4: p is_a_unity_wrt g by BINOP_1: 3;

      then (g "**" ( <*> (D * ))) = ( the_unity_wrt g) by FINSOP_1: 10, SETWISEO:def 2;

      hence thesis by A2, A4, BINOP_1:def 8;

    end;

    theorem :: PRE_POLY:3

    

     Th3: for D be set, F,G be FinSequence of (D * ) holds ( FlattenSeq (F ^ G)) = (( FlattenSeq F) ^ ( FlattenSeq G))

    proof

      let D be set, F,G be FinSequence of (D * );

      consider g be BinOp of (D * ) such that

       A1: for d1,d2 be Element of (D * ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq (F ^ G)) = (g "**" (F ^ G)) by Def1;

      now

        let a,b,c be Element of (D * );

        

        thus (g . (a,(g . (b,c)))) = (a ^ (g . (b,c))) by A1

        .= (a ^ (b ^ c)) by A1

        .= ((a ^ b) ^ c) by FINSEQ_1: 32

        .= ((g . (a,b)) ^ c) by A1

        .= (g . ((g . (a,b)),c)) by A1;

      end;

      then

       A3: g is associative;

      

       A4: {} is Element of (D * ) by FINSEQ_1: 49;

      reconsider p = {} as Element of (D * ) by FINSEQ_1: 49;

      now

        let a be Element of (D * );

        

        thus (g . ( {} ,a)) = ( {} ^ a) by A1, A4

        .= a by FINSEQ_1: 34;

        

        thus (g . (a, {} )) = (a ^ {} ) by A1, A4

        .= a by FINSEQ_1: 34;

      end;

      then p is_a_unity_wrt g by BINOP_1: 3;

      

      hence ( FlattenSeq (F ^ G)) = (g . ((g "**" F),(g "**" G))) by A2, A3, FINSOP_1: 5, SETWISEO:def 2

      .= ((g "**" F) ^ (g "**" G)) by A1

      .= (( FlattenSeq F) ^ (g "**" G)) by A1, Def1

      .= (( FlattenSeq F) ^ ( FlattenSeq G)) by A1, Def1;

    end;

    theorem :: PRE_POLY:4

    for D be set, p,q be Element of (D * ) holds ( FlattenSeq <*p, q*>) = (p ^ q)

    proof

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

      consider g be BinOp of (D * ) such that

       A1: for d1,d2 be Element of (D * ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq <*p, q*>) = (g "**" <*p, q*>) by Def1;

      

      thus ( FlattenSeq <*p, q*>) = (g . (p,q)) by A2, FINSOP_1: 12

      .= (p ^ q) by A1;

    end;

    theorem :: PRE_POLY:5

    for D be set, p,q,r be Element of (D * ) holds ( FlattenSeq <*p, q, r*>) = ((p ^ q) ^ r)

    proof

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

      consider g be BinOp of (D * ) such that

       A1: for d1,d2 be Element of (D * ) holds (g . (d1,d2)) = (d1 ^ d2) and

       A2: ( FlattenSeq <*p, q, r*>) = (g "**" <*p, q, r*>) by Def1;

      

      thus ( FlattenSeq <*p, q, r*>) = (g . ((g . (p,q)),r)) by A2, FINSOP_1: 14

      .= ((g . (p,q)) ^ r) by A1

      .= ((p ^ q) ^ r) by A1;

    end;

    theorem :: PRE_POLY:6

    for D be set, F,G be FinSequence of (D * ) holds F c= G implies ( FlattenSeq F) c= ( FlattenSeq G)

    proof

      let D be set, F,G be FinSequence of (D * );

      assume F c= G;

      then

      consider F9 be FinSequence of (D * ) such that

       A1: (F ^ F9) = G by FINSEQ_4: 82;

      (( FlattenSeq F) ^ ( FlattenSeq F9)) = ( FlattenSeq G) by A1, Th3;

      hence thesis by FINSEQ_6: 10;

    end;

    begin

    reserve A for set,

x,y,z for object,

k for Element of NAT ;

    scheme :: PRE_POLY:sch1

    Regr1 { n() -> Nat , P[ set] } :

for k st k <= n() holds P[k]

      provided

       A1: P[n()]

       and

       A2: for k st k < n() & P[(k + 1)] holds P[k];

      reconsider n9 = n() as Element of NAT by ORDINAL1:def 12;

      defpred X[ Nat] means $1 <= n() & not P[$1];

      assume not thesis;

      then

       A3: ex k be Nat st X[k];

      

       A4: for l be Nat st X[l] holds l <= n9;

      consider l be Nat such that

       A5: X[l] and

       A6: for n be Nat st X[n] holds n <= l from NAT_1:sch 6( A4, A3);

      

       A7: l in NAT by ORDINAL1:def 12;

      

       A8: l < n() by A1, A5, XXREAL_0: 1;

      then (l + 1) <= n() by NAT_1: 13;

      then P[(l + 1)] by A6, XREAL_1: 29;

      hence contradiction by A2, A5, A8, A7;

    end;

    registration

      let n be Nat;

      cluster ( Seg (n + 1)) -> non empty;

      coherence ;

    end

    theorem :: PRE_POLY:7

    ( {} |_2 A) = {} ;

    registration

      let X be set;

      cluster non empty for Subset of ( Fin X);

      existence

      proof

         { {} } is Subset of ( Fin X) by FINSUB_1: 7, ZFMISC_1: 31;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster non empty with_non-empty_elements for Subset of ( Fin X);

      existence

      proof

        set x = the Element of X;

         {x} in ( Fin X) by FINSUB_1:def 5;

        then

        reconsider s = { {x}} as Subset of ( Fin X) by SUBSET_1: 33;

        take s;

        thus s is non empty;

        assume {} in s;

        hence contradiction;

      end;

    end

    registration

      let X be non empty set, F be non empty with_non-empty_elements Subset of ( Fin X);

      cluster non empty for Element of F;

      existence

      proof

        set f = the Element of F;

        f <> {} ;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster with_non-empty_element for Subset of ( Fin X);

      existence

      proof

        set x = the Element of X;

         {x} in ( Fin X) by FINSUB_1:def 5;

        then

        reconsider s = { {x}} as Subset of ( Fin X) by SUBSET_1: 33;

        take s;

        thus thesis;

      end;

    end

    definition

      let X be non empty set, R be Order of X, A be Subset of X;

      :: original: |_2

      redefine

      func R |_2 A -> Order of A ;

      coherence

      proof

        R partially_orders X by ORDERS_1: 44;

        hence (R |_2 A) is Order of A by ORDERS_1: 35, ORDERS_1: 45;

      end;

    end

    scheme :: PRE_POLY:sch2

    SubFinite { D() -> set , A() -> Subset of D() , P[ set] } :

P[A()]

      provided

       A1: A() is finite

       and

       A2: P[( {} D())]

       and

       A3: for x be Element of D(), B be Subset of D() st x in A() & B c= A() & P[B] holds P[(B \/ {x})];

      now

        defpred X[ set] means ex B be set st B = $1 & P[B];

        assume A() <> {} ;

        consider G be set such that

         A4: for x be set holds x in G iff x in ( bool A()) & X[x] from XFAMILY:sch 1;

        G c= ( bool A()) by A4;

        then

        reconsider GA = G as Subset-Family of A();

         {} c= A();

        then GA <> {} by A2, A4;

        then

        consider B be set such that

         A5: B in GA and

         A6: for X be set st X in GA holds B c= X implies B = X by A1, FINSET_1: 6;

        

         A7: ex A st A = B & P[A] by A4, A5;

        now

          set x = the Element of (A() \ B);

          assume B <> A();

          then not A() c= B by A5;

          then

           A8: (A() \ B) <> {} by XBOOLE_1: 37;

          then not x in B by XBOOLE_0:def 5;

          then

           A9: (B \/ {x}) <> B by XBOOLE_1: 7, ZFMISC_1: 31;

          

           A10: x in A() by A8, XBOOLE_0:def 5;

          then {x} c= A() by ZFMISC_1: 31;

          then

           A11: (B \/ {x}) c= A() by A5, XBOOLE_1: 8;

          B is Subset of D() by A5, XBOOLE_1: 1;

          then (B \/ {x}) in GA by A4, A11, A3, A5, A7, A10;

          hence contradiction by A6, A9, XBOOLE_1: 7;

        end;

        hence thesis by A7;

      end;

      hence thesis by A2;

    end;

    registration

      let X be non empty set, F be with_non-empty_element Subset of ( Fin X);

      cluster finite non empty for Element of F;

      existence

      proof

        consider x be non empty set such that

         A1: x in F by SETFAM_1:def 10;

        reconsider x1 = x as Element of F by A1;

        take x1;

        thus thesis;

      end;

    end

    definition

      let X be set, A be finite Subset of X, R be Order of X;

      assume

       A1: R linearly_orders A;

      :: PRE_POLY:def2

      func SgmX (R,A) -> FinSequence of X means

      : Def2: ( rng it ) = A & for n,m be Nat st n in ( dom it ) & m in ( dom it ) & n < m holds (it /. n) <> (it /. m) & [(it /. n), (it /. m)] in R;

      existence

      proof

        per cases ;

          suppose

           A2: A is empty;

          take ( <*> X);

          thus thesis by A2;

        end;

          suppose

           A3: A is non empty;

          then

          reconsider X9 = X as non empty set;

          reconsider A1 = A as non empty finite Subset of X9 by A3;

          reconsider R9 = R as Order of X9;

          deffunc F( set) = $1;

          deffunc V( Element of A1) = { F(x) where x be Element of A1 : x <=_ (R9,$1) & x <> $1 };

          deffunc U( Element of A1) = (( card V($1)) +^ 1);

          

           A4: for x be Element of A1 holds U(x) is Element of NAT

          proof

            let a be Element of A1;

            defpred P[ Element of A1] means $1 <=_ (R9,a) & $1 <> a;

            { F(x) where x be Element of A1 : P[x] } is finite from PRE_CIRC:sch 1;

            then

            reconsider X = { F(x) where x be Element of A1 : P[x] } as finite set;

            reconsider n = ( card X) as Element of NAT ;

            (n +^ 1) = (n + 1) by CARD_2: 36;

            hence U(a) is Element of NAT ;

          end;

          consider f be Function of A1, NAT such that

           A5: for x be Element of A1 holds (f . x) = U(x) from FUNCT_2:sch 9( A4);

          

           A6: for x be Element of A1 holds not x in V(x)

          proof

            let a be Element of A1;

            assume a in V(a);

            then ex x be Element of A1 st x = a & x <=_ (R9,a) & x <> a;

            hence thesis;

          end;

          

           A7: for x be Element of A1 holds V(x) c= A1

          proof

            let a be Element of A1;

            let y be object;

            assume y in V(a);

            then ex x be Element of A1 st x = y & x <=_ (R9,a) & x <> a;

            hence thesis;

          end;

          ( rng f) c= ( Seg ( card A1))

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x1 be object such that

             A8: x1 in ( dom f) and

             A9: y = (f . x1) by FUNCT_1:def 3;

            reconsider y1 = y as Nat by A9;

            reconsider x2 = x1 as Element of A1 by A8;

            defpred P[ Element of A1] means $1 <=_ (R9,x2) & $1 <> x2;

            { F(x) where x be Element of A1 : P[x] } is finite from PRE_CIRC:sch 1;

            then

            reconsider Vx2 = V(x2) as finite set;

            Vx2 <> A1 by A6;

            then

             A10: ( card Vx2) <> ( card A1) by A7, CARD_2: 102;

            ( card Vx2) <= ( card A1) by A7, NAT_1: 43;

            then ( card Vx2) < ( card A1) by A10, XXREAL_0: 1;

            then

             A11: (( card Vx2) + 1) <= ( card A1) by NAT_1: 13;

            

             A12: y = (( card Vx2) +^ 1) by A5, A9

            .= (( card Vx2) + 1) by CARD_2: 36;

            then ( 0 qua Nat + 1) <= y1 by XREAL_1: 6;

            hence thesis by A11, A12, FINSEQ_1: 1;

          end;

          then

          reconsider f1 = f as Function of A1, ( Seg ( card A1)) by FUNCT_2: 6;

          

           A13: (R |_2 A) c= R by XBOOLE_1: 17;

          

           A14: R is_connected_in A by A1, ORDERS_1:def 9;

          then

           A15: (R |_2 A) is connected by ORDERS_1: 75;

          

           A16: ( field (R9 |_2 A1)) = A by ORDERS_1: 15;

          

           A17: R9 is_transitive_in A by A1, ORDERS_1:def 9;

          

           A18: R9 is_antisymmetric_in A by A1, ORDERS_1:def 9;

          for x1,x2 be object st x1 in A1 & x2 in A1 & (f . x1) = (f . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume that

             A19: x1 in A1 and

             A20: x2 in A1 and

             A21: (f . x1) = (f . x2);

            reconsider x29 = x2 as Element of A1 by A20;

            reconsider x19 = x1 as Element of A1 by A19;

            defpred P[ Element of A1] means $1 <=_ (R9,x19) & $1 <> x19;

            { F(x) where x be Element of A1 : P[x] } is finite from PRE_CIRC:sch 1;

            then

            reconsider Vx1 = V(x19) as finite set;

            defpred P[ Element of A1] means $1 <=_ (R9,x29) & $1 <> x29;

            { F(x) where x be Element of A1 : P[x] } is finite from PRE_CIRC:sch 1;

            then

            reconsider Vx2 = V(x29) as finite set;

            

             A22: for x1,x2 be Element of A1 st x1 <=_ ((R |_2 A),x2) holds V(x1) c= V(x2)

            proof

              let x1,x2 be Element of A1;

              assume x1 <=_ ((R |_2 A),x2);

              then

               A23: [x1, x2] in (R |_2 A) by ARROW:def 4;

              let x be object;

              assume x in V(x1);

              then

              consider a be Element of A such that

               A24: a = x and

               A25: a <=_ (R9,x1) and

               A26: a <> x1;

              

               A27: [a, x1] in R9 by A25, ARROW:def 4;

              then [a, x2] in R9 by A23, A13, A17;

              then

               A28: a <=_ (R9,x2) by ARROW:def 4;

              a <> x2 by A26, A27, A23, A13, A18;

              hence x in V(x2) by A24, A28;

            end;

            (f . x19) = (( card Vx1) +^ 1) by A5

            .= (( card Vx1) + 1) by CARD_2: 36;

            

            then

             A29: (( card Vx1) + 1) = (( card Vx2) +^ 1) by A5, A21

            .= (( card Vx2) + 1) by CARD_2: 36;

            now

              per cases ;

                suppose x19 = x29;

                hence thesis;

              end;

                suppose x19 <> x29;

                then

                 A30: [x19, x29] in (R |_2 A) or [x29, x19] in (R |_2 A) by A16, A15, RELAT_2:def 6;

                

                 A31: for x1,x2 be Element of A1 st x1 <> x2 & x1 <=_ ((R |_2 A),x2) holds x1 in V(x2)

                proof

                  let x1,x2 be Element of A1 such that

                   A32: x1 <> x2;

                  assume x1 <=_ ((R |_2 A),x2);

                  then [x1, x2] in (R |_2 A) by ARROW:def 4;

                  then x1 <=_ (R9,x2) by A13, ARROW:def 4;

                  hence x1 in V(x2) by A32;

                end;

                 A33:

                now

                  per cases by A30, ARROW:def 4;

                    suppose x19 <=_ ((R |_2 A),x29);

                    hence Vx1 = Vx2 by A29, A22, CARD_2: 102;

                  end;

                    suppose x29 <=_ ((R |_2 A),x19);

                    hence Vx1 = Vx2 by A29, A22, CARD_2: 102;

                  end;

                end;

                now

                  assume

                   A34: x19 <> x29;

                  then

                   A35: [x19, x29] in (R |_2 A) or [x29, x19] in (R |_2 A) by A16, A15, RELAT_2:def 6;

                  per cases by A35, ARROW:def 4;

                    suppose x19 <=_ ((R |_2 A),x29);

                    hence contradiction by A33, A6, A34, A31;

                  end;

                    suppose x29 <=_ ((R |_2 A),x19);

                    hence contradiction by A33, A6, A34, A31;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          then

           A36: f1 is one-to-one by FUNCT_2: 19;

          

           A37: for x1,x2 be Element of A1 st (f . x1) qua Nat < (f . x2) holds x1 <=_ (R9,x2) & x1 <> x2

          proof

            let x1,x2 be Element of A1;

            defpred P[ Element of A1] means $1 <=_ (R9,x1) & $1 <> x1;

            { F(x) where x be Element of A1 : P[x] } is finite from PRE_CIRC:sch 1;

            then

            reconsider Vx1 = V(x1) as finite set;

            defpred P[ Element of A1] means $1 <=_ (R9,x2) & $1 <> x2;

            { F(x) where x be Element of A1 : P[x] } is finite from PRE_CIRC:sch 1;

            then

            reconsider Vx2 = V(x2) as finite set;

            assume

             A38: (f . x1) < (f . x2);

            

             A39: (f . x1) = (( card Vx1) +^ 1) by A5

            .= (( card Vx1) + 1) by CARD_2: 36;

            (f . x2) = (( card Vx2) +^ 1) by A5

            .= (( card Vx2) + 1) by CARD_2: 36;

            then

             A40: ((( card Vx1) + 1) - 1) < ((( card Vx2) + 1) - 1) by A39, A38, XREAL_1: 9;

            reconsider Cx2 = ( card Vx2) as Cardinal;

            reconsider Cx1 = ( card Vx1) as Cardinal;

            

             A41: ( card ( Segm ( card Vx2))) = ( card Vx2);

            ( card ( Segm ( card Vx1))) = ( card Vx1);

            then (Vx2 \ Vx1) <> {} by A41, A40, CARD_1: 68, NAT_1: 41;

            then

            consider a be object such that

             A42: a in (Vx2 \ Vx1) by XBOOLE_0:def 1;

            

             A43: not a in Vx1 by A42, XBOOLE_0:def 5;

            

             A44: a in Vx2 by A42;

            Vx2 c= A1 by A7;

            then

            reconsider a as Element of A1 by A44;

            

             A45: ex x be Element of A1 st a = x & x <=_ (R9,x2) & x <> x2 by A44;

            then

             A46: [a, x2] in R9 by ARROW:def 4;

            per cases by A43;

              suppose not a <=_ (R9,x1);

              then

               A47: not [a, x1] in R9 by ARROW:def 4;

              per cases ;

                suppose x1 = a;

                hence thesis by A45;

              end;

                suppose

                 A48: x1 <> a;

                then

                 A49: [x1, a] in R9 by A14, A47;

                then [x1, x2] in R9 by A46, A17;

                hence x1 <=_ (R9,x2) by ARROW:def 4;

                assume x1 = x2;

                hence contradiction by A48, A49, A46, A18;

              end;

            end;

              suppose a = x1;

              hence thesis by A45;

            end;

          end;

          ( card ( Seg ( card A1))) = ( card A1) by FINSEQ_1: 57;

          then f1 is onto by A36, FINSEQ_4: 63;

          then ( rng f1) = ( Seg ( card A1)) by FUNCT_2:def 3;

          then ( dom (f1 qua Function " )) = ( Seg ( card A1)) by A36, FUNCT_1: 33;

          then

          reconsider g1 = (f1 qua Function " ) as FinSequence by FINSEQ_1:def 2;

          

           A50: ( dom f1) = A by FUNCT_2:def 1;

          then

           A51: ( rng g1) = A by A36, FUNCT_1: 33;

          then

          reconsider g = g1 as FinSequence of X by FINSEQ_1:def 4;

          take g;

          thus ( rng g) = A by A36, A50, FUNCT_1: 33;

          let n,m be Nat;

          assume that

           A52: n in ( dom g) and

           A53: m in ( dom g) and

           A54: n < m;

          reconsider gn = (g . n) as Element of A1 by A51, A52, FUNCT_1:def 3;

          n in ( rng f) by A36, A52, FUNCT_1: 33;

          then

           A55: n = (f . gn) by A36, FUNCT_1: 35;

          reconsider gm = (g . m) as Element of A1 by A51, A53, FUNCT_1:def 3;

          

           A56: gm = (g /. m) by A53, PARTFUN1:def 6;

          

           A57: m in ( rng f) by A36, A53, FUNCT_1: 33;

          then m = (f . gm) by A36, FUNCT_1: 35;

          then

           A58: [gn, gm] in R by A37, A54, A55, ARROW:def 4;

          gn = (g /. n) by A52, PARTFUN1:def 6;

          hence thesis by A36, A54, A57, A55, A58, A56, FUNCT_1: 35;

        end;

      end;

      uniqueness

      proof

        let p9,q9 be FinSequence of X;

        assume that

         A59: ( rng p9) = A and

         A60: for n,m be Nat st n in ( dom p9) & m in ( dom p9) & n < m holds (p9 /. n) <> (p9 /. m) & [(p9 /. n), (p9 /. m)] in R and

         A61: ( rng q9) = A and

         A62: for n,m be Nat st n in ( dom q9) & m in ( dom q9) & n < m holds (q9 /. n) <> (q9 /. m) & [(q9 /. n), (q9 /. m)] in R;

        per cases ;

          suppose

           A63: A is empty;

          then p9 is empty by A59;

          hence thesis by A61, A63;

        end;

          suppose

           A64: A is non empty;

          then

          reconsider X9 = X as non empty set;

          reconsider A9 = A as non empty finite Subset of X9 by A64;

          set E = ( <*> A9);

          defpred X[ FinSequence of A9] means ($1 is FinSequence of A9 & for n,m be Nat st n in ( dom $1) & m in ( dom $1) & n < m holds ($1 /. n) <> ($1 /. m) & [($1 /. n), ($1 /. m)] in R) implies for q be FinSequence of A9 st ( rng q) = ( rng $1) & for n,m be Nat st n in ( dom q) & m in ( dom q) & n < m holds (q /. n) <> (q /. m) & [(q /. n), (q /. m)] in R holds q = $1;

          reconsider p = p9, q = q9 as FinSequence of A9 by A59, A61, FINSEQ_1:def 4;

          

           A65: for p be FinSequence of A9 holds for x be Element of A9 st X[p] holds X[(p ^ <*x*>) qua FinSequence of A9]

          proof

            let p be FinSequence of A9, x be Element of A9;

            assume

             A66: X[p];

            assume (p ^ <*x*>) is FinSequence of A9;

            assume

             A67: for n,m be Nat st n in ( dom (p ^ <*x*>)) & m in ( dom (p ^ <*x*>)) & n < m holds ((p ^ <*x*>) qua FinSequence of A9 /. n) <> ((p ^ <*x*>) qua FinSequence of A9 /. m) & [((p ^ <*x*>) qua FinSequence of A9 /. n), ((p ^ <*x*>) qua FinSequence of A9 /. m)] in R;

            let q be FinSequence of A9;

            assume that

             A68: ( rng q) = ( rng (p ^ <*x*>)) and

             A69: for n,m be Nat st n in ( dom q) & m in ( dom q) & n < m holds (q /. n) <> (q /. m) & [(q /. n), (q /. m)] in R;

            deffunc V( Nat) = (q . $1);

            

             A70: q <> 0 by A68;

            then

            consider n be Nat such that

             A71: ( len q) = (n + 1) by NAT_1: 6;

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

            ex q9 be FinSequence st ( len q9) = n & for m be Nat st m in ( dom q9) holds (q9 . m) = V(m) from FINSEQ_1:sch 2;

            then

            consider q9 be FinSequence such that

             A72: ( len q9) = n and

             A73: for m be Nat st m in ( dom q9) holds (q9 . m) = (q . m);

            1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

            then

             A74: 1 in ( dom <*x*>) by FINSEQ_1:def 8;

            

             A75: ex m be Element of A9 st m = x & for l be Element of A9 st l in ( rng (p ^ <*x*>)) & l <> x holds [l, m] in R

            proof

              reconsider m = x as Element of A9;

              take m;

              thus m = x;

              thus for l be Element of A9 st l in ( rng (p ^ <*x*>)) & l <> x holds [l, m] in R

              proof

                let l be Element of A9;

                assume that

                 A76: l in ( rng (p ^ <*x*>)) and

                 A77: l <> x;

                consider y be object such that

                 A78: y in ( dom (p ^ <*x*>)) and

                 A79: l = ((p ^ <*x*>) . y) by A76, FUNCT_1:def 3;

                

                 A80: l = ((p ^ <*x*>) qua FinSequence of A9 /. y) by A78, A79, PARTFUN1:def 6;

                reconsider k = y as Element of NAT by A78;

                

                 A81: k <> (( len p) + 1)

                proof

                  assume k = (( len p) + 1);

                  

                  then ((p ^ <*x*>) . k) = ( <*x*> . 1) by A74, FINSEQ_1:def 7

                  .= x by FINSEQ_1:def 8;

                  hence contradiction by A77, A79;

                end;

                

                 A82: y in ( Seg ( len (p ^ <*x*>))) by A78, FINSEQ_1:def 3;

                then k <= ( len (p ^ <*x*>)) by FINSEQ_1: 1;

                then k <= (( len p) + ( len <*x*>)) by FINSEQ_1: 22;

                then k <= (( len p) + 1) by FINSEQ_1: 39;

                then k < (( len p) + 1) by A81, XXREAL_0: 1;

                then k < (( len p) + ( len <*x*>)) by FINSEQ_1: 39;

                then

                 A83: k < ( len (p ^ <*x*>)) by FINSEQ_1: 22;

                1 <= k by A82, FINSEQ_1: 1;

                then (1 - ( len (p ^ <*x*>))) < (k - k) by A83, XREAL_1: 15;

                then 1 < ( len (p ^ <*x*>)) by XREAL_1: 48;

                then ( len (p ^ <*x*>)) in ( Seg ( len (p ^ <*x*>))) by FINSEQ_1: 1;

                then

                 A84: ( len (p ^ <*x*>)) in ( dom (p ^ <*x*>)) by FINSEQ_1:def 3;

                m = ((p ^ <*x*>) . (( len p) + 1)) by FINSEQ_1: 42

                .= ((p ^ <*x*>) . (( len p) + ( len <*x*>))) by FINSEQ_1: 39

                .= ((p ^ <*x*>) . ( len (p ^ <*x*>))) by FINSEQ_1: 22;

                then m = ((p ^ <*x*>) qua FinSequence of A9 /. ( len (p ^ <*x*>))) by A84, PARTFUN1:def 6;

                hence thesis by A67, A78, A80, A83, A84;

              end;

            end;

            

             A85: for m be Nat st m in ( dom <*x*>) holds (q . (( len q9) + m)) = ( <*x*> . m)

            proof

              let m be Nat;

              assume m in ( dom <*x*>);

              then

               A86: m in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

              

               A87: (q . (( len q9) + m)) = x

              proof

                consider d1 be Element of A9 such that

                 A88: d1 = x and

                 A89: for l be Element of A9 st l in ( rng (p ^ <*x*>)) & l <> x holds [l, d1] in R by A75;

                reconsider d = d1 as Element of A9;

                ( len q) in ( Seg ( len q)) by A70, FINSEQ_1: 3;

                then

                 A90: ( len q) in ( dom q) by FINSEQ_1:def 3;

                then (q . ( len q)) in ( rng q) by FUNCT_1:def 3;

                then

                reconsider k = (q . ( len q)) as Element of A9;

                

                 A91: k = (q /. ( len q)) by A90, PARTFUN1:def 6;

                

                 A92: ( field R) = X by ORDERS_1: 12;

                assume (q . (( len q9) + m)) <> x;

                then

                 A93: (q . ( len q)) <> x by A71, A72, A86, TARSKI:def 1;

                x in {x} by TARSKI:def 1;

                then x in ( rng <*x*>) by FINSEQ_1: 38;

                then x in (( rng p) \/ ( rng <*x*>)) by XBOOLE_0:def 3;

                then x in ( rng q) by A68, FINSEQ_1: 31;

                then

                consider y be object such that

                 A94: y in ( dom q) and

                 A95: x = (q . y) by FUNCT_1:def 3;

                

                 A96: y in ( Seg ( len q)) by A94, FINSEQ_1:def 3;

                reconsider y as Element of NAT by A94;

                y <= ( len q) by A96, FINSEQ_1: 1;

                then

                 A97: y < ( len q) by A93, A95, XXREAL_0: 1;

                (q . ( len q)) in ( rng (p ^ <*x*>)) by A68, A90, FUNCT_1:def 3;

                then

                 A98: [k, d] in R by A93, A89;

                

                 A99: d = (q /. y) by A88, A94, A95, PARTFUN1:def 6;

                then

                 A100: [d, k] in R by A69, A94, A90, A97, A91;

                k <> d by A69, A94, A90, A97, A91, A99;

                hence contradiction by A98, A100, A92, RELAT_2:def 4, RELAT_2:def 12;

              end;

              m = 1 by A86, TARSKI:def 1;

              hence thesis by A87, FINSEQ_1: 40;

            end;

            now

              let x be object;

              

               A101: n <= (n + 1) by NAT_1: 11;

              assume x in ( rng q9);

              then

              consider y be object such that

               A102: y in ( dom q9) and

               A103: x = (q9 . y) by FUNCT_1:def 3;

              

               A104: y in ( Seg ( len q9)) by A102, FINSEQ_1:def 3;

              reconsider y as Element of NAT by A102;

              y <= n by A72, A104, FINSEQ_1: 1;

              then

               A105: y <= (n + 1) by A101, XXREAL_0: 2;

              1 <= y by A104, FINSEQ_1: 1;

              then y in ( dom q) by A71, A105, FINSEQ_3: 25;

              then (q . y) in ( rng q) by FUNCT_1:def 3;

              then (q . y) in A9;

              hence x in A9 by A73, A102, A103;

            end;

            then

            reconsider f = q9 as FinSequence of A9 by FINSEQ_1:def 4, TARSKI:def 3;

            ( dom q) = ( Seg (n + 1)) by A71, FINSEQ_1:def 3

            .= ( Seg (( len q9) + ( len <*x*>))) by A72, FINSEQ_1: 39;

            then

             A106: (q9 ^ <*x*>) = q by A73, A85, FINSEQ_1:def 7;

            

             A107: not x in ( rng p)

            proof

              (( len p) + 1) = (( len p) + ( len <*x*>)) by FINSEQ_1: 39

              .= ( len (p ^ <*x*>)) by FINSEQ_1: 22;

              then (( len p) + 1) in ( Seg ( len (p ^ <*x*>))) by FINSEQ_1: 4;

              then

               A108: (( len p) + 1) in ( dom (p ^ <*x*>)) by FINSEQ_1:def 3;

              assume x in ( rng p);

              then

              consider y be object such that

               A109: y in ( dom p) and

               A110: x = (p . y) by FUNCT_1:def 3;

              

               A111: y in ( Seg ( len p)) by A109, FINSEQ_1:def 3;

              

               A112: ( dom p) c= ( dom (p ^ <*x*>)) by FINSEQ_1: 26;

              reconsider y as Element of NAT by A109;

              x = ((p ^ <*x*>) qua FinSequence of A9 . y) by A109, A110, FINSEQ_1:def 7;

              then

               A113: x = ((p ^ <*x*>) qua FinSequence of A9 /. y) by A109, A112, PARTFUN1:def 6;

              y <= ( len p) by A111, FINSEQ_1: 1;

              then

               A114: y < (( len p) + 1) by NAT_1: 13;

              x = ((p ^ <*x*>) qua FinSequence of A9 . (( len p) + 1)) by FINSEQ_1: 42;

              then ((p ^ <*x*>) qua FinSequence of A9 /. y) = ((p ^ <*x*>) qua FinSequence of A9 /. (( len p) + 1)) by A108, A113, PARTFUN1:def 6;

              hence contradiction by A67, A109, A108, A112, A114;

            end;

            

             A115: for z be object holds z in ((( rng p) \/ {x}) \ {x}) iff z in ( rng p)

            proof

              let z be object;

              thus z in ((( rng p) \/ {x}) \ {x}) implies z in ( rng p)

              proof

                assume

                 A116: z in ((( rng p) \/ {x}) \ {x});

                then

                 A117: not z in {x} by XBOOLE_0:def 5;

                z in (( rng p) \/ {x}) by A116, XBOOLE_0:def 5;

                hence thesis by A117, XBOOLE_0:def 3;

              end;

              assume

               A118: z in ( rng p);

              then

               A119: z in (( rng p) \/ {x}) by XBOOLE_0:def 3;

               not z in {x} by A107, A118, TARSKI:def 1;

              hence thesis by A119, XBOOLE_0:def 5;

            end;

            ( rng (p ^ <*x*>)) = (( rng p) \/ ( rng <*x*>)) by FINSEQ_1: 31

            .= (( rng p) \/ {x}) by FINSEQ_1: 39;

            then

             A120: ( rng p) = (( rng (p ^ <*x*>)) \ {x}) by A115, TARSKI: 2;

            

             A121: ( rng f) = ( rng p) & for l,m be Nat st l in ( dom f) & m in ( dom f) & l < m holds (f /. l) <> (f /. m) & [(f /. l), (f /. m)] in R

            proof

              

               A122: not x in ( rng f)

              proof

                (( len f) + 1) = (( len f) + ( len <*x*>)) by FINSEQ_1: 39

                .= ( len (f ^ <*x*>)) by FINSEQ_1: 22;

                then (( len f) + 1) in ( Seg ( len (f ^ <*x*>))) by FINSEQ_1: 4;

                then

                 A123: (( len f) + 1) in ( dom (f ^ <*x*>)) by FINSEQ_1:def 3;

                assume x in ( rng f);

                then

                consider y be object such that

                 A124: y in ( dom f) and

                 A125: x = (f . y) by FUNCT_1:def 3;

                

                 A126: y in ( Seg ( len f)) by A124, FINSEQ_1:def 3;

                

                 A127: ( dom f) c= ( dom (f ^ <*x*>)) by FINSEQ_1: 26;

                reconsider y as Element of NAT by A124;

                x = (q . y) by A73, A124, A125;

                then

                 A128: x = (q /. y) by A106, A124, A127, PARTFUN1:def 6;

                y <= ( len f) by A126, FINSEQ_1: 1;

                then

                 A129: y < (( len f) + 1) by NAT_1: 13;

                x = (q . (( len f) + 1)) by A106, FINSEQ_1: 42;

                then (q /. y) = (q /. (( len f) + 1)) by A106, A123, A128, PARTFUN1:def 6;

                hence contradiction by A69, A106, A124, A123, A127, A129;

              end;

              

               A130: for z be object holds z in ((( rng f) \/ {x}) \ {x}) iff z in ( rng f)

              proof

                let z be object;

                hereby

                  assume

                   A131: z in ((( rng f) \/ {x}) \ {x});

                  then

                   A132: not z in {x} by XBOOLE_0:def 5;

                  z in (( rng f) \/ {x}) by A131, XBOOLE_0:def 5;

                  hence z in ( rng f) by A132, XBOOLE_0:def 3;

                end;

                assume

                 A133: z in ( rng f);

                then

                 A134: z in (( rng f) \/ {x}) by XBOOLE_0:def 3;

                 not z in {x} by A122, A133, TARSKI:def 1;

                hence thesis by A134, XBOOLE_0:def 5;

              end;

              ( rng (f ^ <*x*>)) = (( rng f) \/ ( rng <*x*>)) by FINSEQ_1: 31

              .= (( rng f) \/ {x}) by FINSEQ_1: 39;

              hence ( rng f) = ( rng p) by A68, A106, A120, A130, TARSKI: 2;

              let l,m be Nat;

              assume that

               A135: l in ( dom f) and

               A136: m in ( dom f) and

               A137: l < m;

              

               A138: (f . m) = (f /. m) by A136, PARTFUN1:def 6;

              

               A139: ( dom f) c= ( dom q) by A106, FINSEQ_1: 26;

              then (q . m) = (q /. m) by A136, PARTFUN1:def 6;

              then

               A140: (f /. m) = (q /. m) by A73, A136, A138;

              

               A141: (f . l) = (f /. l) by A135, PARTFUN1:def 6;

              (q . l) = (q /. l) by A139, A135, PARTFUN1:def 6;

              then (f /. l) = (q /. l) by A73, A135, A141;

              hence thesis by A69, A139, A135, A136, A137, A140;

            end;

            p is FinSequence of A9 & for l,m be Nat st l in ( dom p) & m in ( dom p) & l < m holds (p /. l) <> (p /. m) & [(p /. l), (p /. m)] in R

            proof

              thus p is FinSequence of A9;

              let l,m be Nat;

              assume that

               A142: l in ( dom p) and

               A143: m in ( dom p) and

               A144: l < m;

              

               A145: ( dom p) c= ( dom (p ^ <*x*>)) by FINSEQ_1: 26;

              (p . m) = ((p ^ <*x*>) . m) by A143, FINSEQ_1:def 7;

              then (p . m) = ((p ^ <*x*>) qua FinSequence of A9 /. m) by A143, A145, PARTFUN1:def 6;

              then

               A146: (p /. m) = ((p ^ <*x*>) qua FinSequence of A9 /. m) by A143, PARTFUN1:def 6;

              (p . l) = ((p ^ <*x*>) . l) by A142, FINSEQ_1:def 7;

              then (p . l) = ((p ^ <*x*>) qua FinSequence of A9 /. l) by A142, A145, PARTFUN1:def 6;

              then (p /. l) = ((p ^ <*x*>) qua FinSequence of A9 /. l) by A142, PARTFUN1:def 6;

              hence thesis by A67, A142, A143, A144, A145, A146;

            end;

            hence thesis by A66, A106, A121;

          end;

           A147:

          now

            let n,m be Nat;

            assume that

             A148: n in ( dom p) and

             A149: m in ( dom p) and

             A150: n < m;

            

             A151: (p /. m) = (p . m) by A149, PARTFUN1:def 6

            .= (p9 /. m) by A149, PARTFUN1:def 6;

            (p /. n) = (p . n) by A148, PARTFUN1:def 6

            .= (p9 /. n) by A148, PARTFUN1:def 6;

            hence (p /. n) <> (p /. m) & [(p /. n), (p /. m)] in R by A60, A148, A149, A150, A151;

          end;

           A152:

          now

            let n,m be Nat;

            assume that

             A153: n in ( dom q) and

             A154: m in ( dom q) and

             A155: n < m;

            

             A156: (q /. m) = (q . m) by A154, PARTFUN1:def 6

            .= (q9 /. m) by A154, PARTFUN1:def 6;

            (q /. n) = (q . n) by A153, PARTFUN1:def 6

            .= (q9 /. n) by A153, PARTFUN1:def 6;

            hence (q /. n) <> (q /. m) & [(q /. n), (q /. m)] in R by A62, A153, A154, A155, A156;

          end;

          

           A157: X[E];

          for p be FinSequence of A9 holds X[p] from FINSEQ_2:sch 2( A157, A65);

          hence thesis by A59, A61, A147, A152;

        end;

      end;

    end

    ::$Canceled

    theorem :: PRE_POLY:9

    for X be set, A be finite Subset of X, R be Order of X, f be FinSequence of X st ( rng f) = A & for n,m be Nat st n in ( dom f) & m in ( dom f) & n < m holds (f /. n) <> (f /. m) & [(f /. n), (f /. m)] in R holds f = ( SgmX (R,A))

    proof

      let X be set, A be finite Subset of X, R be Order of X, f be FinSequence of X;

      assume that

       A1: ( rng f) = A and

       A2: for n,m be Nat st n in ( dom f) & m in ( dom f) & n < m holds (f /. n) <> (f /. m) & [(f /. n), (f /. m)] in R;

      now

        let a,b be object;

        assume that

         A3: a in A and

         A4: b in A and

         A5: a <> b;

        consider n be Nat such that

         A6: n in ( dom f) and

         A7: (f . n) = a by A1, A3, FINSEQ_2: 10;

        consider m be Nat such that

         A8: m in ( dom f) and

         A9: (f . m) = b by A1, A4, FINSEQ_2: 10;

        

         A10: (f /. m) = (f . m) by A8, PARTFUN1:def 6;

        

         A11: (f /. n) = (f . n) by A6, PARTFUN1:def 6;

        now

          assume that

           A12: not [a, b] in R and

           A13: not [b, a] in R;

          per cases ;

            suppose n = m;

            hence contradiction by A5, A7, A9;

          end;

            suppose

             A14: n <> m;

            now

              per cases by A14, XXREAL_0: 1;

                suppose n > m;

                hence contradiction by A2, A6, A7, A8, A9, A11, A10, A13;

              end;

                suppose m > n;

                hence contradiction by A2, A6, A7, A8, A9, A11, A10, A12;

              end;

            end;

            hence contradiction;

          end;

        end;

        hence [a, b] in R or [b, a] in R;

      end;

      then

       A15: R is_connected_in A;

      

       A16: ( field R) = X by ORDERS_1: 12;

      then

       A17: R is_antisymmetric_in A by ORDERS_1: 9, RELAT_2:def 12;

      R is_transitive_in X by A16, RELAT_2:def 16;

      then

       A18: R is_transitive_in A;

      R is_reflexive_in X by A16, RELAT_2:def 9;

      then R is_reflexive_in A;

      then R linearly_orders A by A17, A18, A15, ORDERS_1:def 9;

      hence thesis by A1, A2, Def2;

    end;

    registration

      let X be set, F be non empty Subset of ( Fin X);

      cluster -> finite for Element of F;

      coherence ;

    end

    definition

      let X be set, F be non empty Subset of ( Fin X);

      :: original: Element

      redefine

      mode Element of F -> Subset of X ;

      coherence

      proof

        let a be Element of F;

        thus thesis by FINSUB_1: 16;

      end;

    end

    theorem :: PRE_POLY:10

    

     Th9: for X be set, A be finite Subset of X, R be Order of X st R linearly_orders A holds ( SgmX (R,A)) is one-to-one

    proof

      let X be set, A be finite Subset of X, R be Order of X;

      set f = ( SgmX (R,A));

      assume

       A1: R linearly_orders A;

      then ( rng f) = A by Def2;

      then

      reconsider f as FinSequence of A by FINSEQ_1:def 4;

      f is one-to-one

      proof

        let k,l be object;

        assume that

         A2: k in ( dom f) and

         A3: l in ( dom f) and

         A4: (f . k) = (f . l);

        reconsider k, l as Element of NAT by A2, A3;

        reconsider fk = (f . k) as Element of A by A2, FINSEQ_2: 11;

        reconsider fl = (f . l) as Element of A by A3, FINSEQ_2: 11;

        

         A5: fl = (f /. l) by A3, PARTFUN1:def 6;

        

         A6: fk = (f /. k) by A2, PARTFUN1:def 6;

        now

          

           A7: (f /. l) = (f . l) by A3, PARTFUN1:def 6

          .= (( SgmX (R,A)) /. l) by A3, PARTFUN1:def 6;

          

           A8: (f /. k) = (f . k) by A2, PARTFUN1:def 6

          .= (( SgmX (R,A)) /. k) by A2, PARTFUN1:def 6;

          assume

           A9: k <> l;

          per cases by A9, XXREAL_0: 1;

            suppose k < l;

            hence contradiction by A1, A2, A3, A4, A6, A5, A8, A7, Def2;

          end;

            suppose l < k;

            hence contradiction by A1, A2, A3, A4, A6, A5, A8, A7, Def2;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:11

    

     Th10: for X be set, A be finite Subset of X, R be Order of X st R linearly_orders A holds ( len ( SgmX (R,A))) = ( card A)

    proof

      let X be set, A be finite Subset of X, R be Order of X;

      set f = ( SgmX (R,A));

      

       A1: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      

       A2: ( card ( Seg ( len f))) = ( card ( len f)) by CARD_1: 5, FINSEQ_1: 54;

      assume

       A3: R linearly_orders A;

      then

       A4: f is one-to-one by Th9;

      ( rng f) = A by A3, Def2;

      hence thesis by A2, A1, A4, CARD_1: 5, WELLORD2:def 4;

    end;

    begin

    reserve n for Nat,

x for object;

    theorem :: PRE_POLY:12

    

     Th11: for M be FinSequence st ( len M) = (n + 1) holds ( len ( Del (M,(n + 1)))) = n

    proof

      let M be FinSequence;

      assume

       A1: ( len M) = (n + 1);

      then (n + 1) in ( Seg ( len M)) by FINSEQ_1: 4;

      then (n + 1) in ( dom M) by FINSEQ_1:def 3;

      hence thesis by A1, FINSEQ_3: 109;

    end;

    theorem :: PRE_POLY:13

    for M be FinSequence st M <> {} holds M = (( Del (M,( len M))) ^ <*(M . ( len M))*>)

    proof

      let M be FinSequence;

      assume M <> {} ;

      then

      consider q be FinSequence, x be object such that

       A1: M = (q ^ <*x*>) by FINSEQ_1: 46;

      

       A2: ( len M) = (( len q) + ( len <*x*>)) by A1, FINSEQ_1: 22

      .= (( len q) + 1) by FINSEQ_1: 39;

      then

       A3: ( len ( Del (M,( len M)))) = ( len q) by Th11;

      

       A4: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

       A5:

      now

        let i be Nat;

        assume

         A6: i in ( dom q);

        then i <= ( len q) by A4, FINSEQ_1: 1;

        then i in NAT & i < ( len M) by A2, NAT_1: 13, ORDINAL1:def 12;

        

        hence (( Del (M,( len M))) . i) = (M . i) by FINSEQ_3: 110

        .= (q . i) by A1, A6, FINSEQ_1:def 7;

      end;

      (M . ( len M)) = x by A1, A2, FINSEQ_1: 42;

      hence thesis by A1, A3, A5, FINSEQ_2: 9;

    end;

    definition

      let IT be Function;

      :: PRE_POLY:def3

      attr IT is FinSequence-yielding means

      : Def3: for x st x in ( dom IT) holds (IT . x) is FinSequence;

    end

    registration

      cluster FinSequence-yielding for Function;

      existence

      proof

        set f = the FinSequence, I = the set;

        take F = (I --> f);

        let x;

        assume x in ( dom F);

        hence thesis by FUNCOP_1: 7;

      end;

    end

    definition

      let F,G be FinSequence-yielding Function;

      :: PRE_POLY:def4

      func F ^^ G -> Function means

      : Def4: ( dom it ) = (( dom F) /\ ( dom G)) & for i be set st i in ( dom it ) holds for f,g be FinSequence st f = (F . i) & g = (G . i) holds (it . i) = (f ^ g);

      existence

      proof

        defpred P[ object, object] means for f be FinSequence, g be FinSequence st f = (F . $1) & g = (G . $1) holds $2 = (f ^ g);

        

         A1: for i be object st i in (( dom F) /\ ( dom G)) holds ex u be object st P[i, u]

        proof

          let i be object;

          assume i in (( dom F) /\ ( dom G));

          then i in ( dom F) & i in ( dom G) by XBOOLE_0:def 4;

          then

          reconsider f = (F . i), g = (G . i) as FinSequence by Def3;

          take (f ^ g);

          thus thesis;

        end;

        consider H be Function such that

         A2: ( dom H) = (( dom F) /\ ( dom G)) & for i be object st i in (( dom F) /\ ( dom G)) holds P[i, (H . i)] from CLASSES1:sch 1( A1);

        take H;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let F1,F2 be Function such that

         A3: ( dom F1) = (( dom F) /\ ( dom G)) and

         A4: for i be set st i in ( dom F1) holds for f,g be FinSequence st f = (F . i) & g = (G . i) holds (F1 . i) = (f ^ g) and

         A5: ( dom F2) = (( dom F) /\ ( dom G)) and

         A6: for i be set st i in ( dom F2) holds for f,g be FinSequence st f = (F . i) & g = (G . i) holds (F2 . i) = (f ^ g);

        now

          let x be object;

          assume

           A7: x in ( dom F1);

          then x in ( dom F) & x in ( dom G) by A3, XBOOLE_0:def 4;

          then

          reconsider f = (F . x), g = (G . x) as FinSequence by Def3;

          

          thus (F1 . x) = (f ^ g) by A4, A7

          .= (F2 . x) by A3, A5, A6, A7;

        end;

        hence thesis by A3, A5;

      end;

    end

    registration

      let F,G be FinSequence-yielding Function;

      cluster (F ^^ G) -> FinSequence-yielding;

      coherence

      proof

        let x be object;

        assume

         A1: x in ( dom (F ^^ G));

        then

         A2: x in (( dom F) /\ ( dom G)) by Def4;

        then x in ( dom F) by XBOOLE_0:def 4;

        then

        reconsider f = (F . x) as FinSequence by Def3;

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

        then

        reconsider g = (G . x) as FinSequence by Def3;

        ((F ^^ G) . x) = (f ^ g) by A1, Def4;

        hence thesis;

      end;

    end

    begin

    reserve V,C for set;

    theorem :: PRE_POLY:14

    for V,C be non empty set holds ex f be Element of ( PFuncs (V,C)) st f <> {}

    proof

      let V,C be non empty set;

      consider a be object such that

       A1: a in V by XBOOLE_0:def 1;

      consider b be object such that

       A2: b in C by XBOOLE_0:def 1;

      set f = { [a, b]};

       {a} c= V by A1, ZFMISC_1: 31;

      then

       A3: ( dom f) c= V by RELAT_1: 9;

       {b} c= C by A2, ZFMISC_1: 31;

      then ( rng f) c= C by RELAT_1: 9;

      then

      reconsider f as Element of ( PFuncs (V,C)) by A3, PARTFUN1:def 3;

      f <> {} ;

      hence thesis;

    end;

    theorem :: PRE_POLY:15

    for f be Element of ( PFuncs (V,C)), g be set st g c= f holds g in ( PFuncs (V,C))

    proof

      let f be Element of ( PFuncs (V,C)), g be set;

      consider f1 be Function such that

       A1: f1 = f and

       A2: ( dom f1) c= V and

       A3: ( rng f1) c= C by PARTFUN1:def 3;

      assume

       A4: g c= f;

      then

      reconsider g9 = g as Function;

      ( rng g9) c= ( rng f1) by A4, A1, RELAT_1: 11;

      then

       A5: ( rng g9) c= C by A3;

      ( dom g9) c= ( dom f1) by A4, A1, RELAT_1: 11;

      then ( dom g9) c= V by A2;

      hence thesis by A5, PARTFUN1:def 3;

    end;

    theorem :: PRE_POLY:16

    

     Th15: ( PFuncs (V,C)) c= ( bool [:V, C:])

    proof

      let x be object;

      assume x in ( PFuncs (V,C));

      then

      consider f be Function such that

       A1: x = f and

       A2: ( dom f) c= V and

       A3: ( rng f) c= C by PARTFUN1:def 3;

      

       A4: f c= [:( dom f), ( rng f):] by RELAT_1: 7;

       [:( dom f), ( rng f):] c= [:V, C:] by A2, A3, ZFMISC_1: 96;

      then f c= [:V, C:] by A4;

      hence thesis by A1;

    end;

    theorem :: PRE_POLY:17

    

     Th16: V is finite & C is finite implies ( PFuncs (V,C)) is finite

    proof

      assume that

       A1: V is finite and

       A2: C is finite;

      ( PFuncs (V,C)) c= ( bool [:V, C:]) by Th15;

      hence thesis by A1, A2;

    end;

    registration

      cluster functional finite non empty for set;

      existence

      proof

        set A = the finite non empty set;

        take P = ( PFuncs (A,A));

        thus P is functional;

        thus P is finite by Th16;

        thus thesis;

      end;

    end

    begin

    registration

      let D be set;

      cluster -> FinSequence-yielding for FinSequence of (D * );

      coherence ;

    end

    registration

      cluster FinSequence-yielding -> Function-yielding for Function;

      coherence

      proof

        let f be Function;

        assume

         A1: f is FinSequence-yielding;

        let x be object;

        thus thesis by A1;

      end;

    end

    begin

    theorem :: PRE_POLY:18

    

     Th17: for X be set, R be Relation st ( field R) c= X holds R is Relation of X

    proof

      let X be set, R be Relation;

      assume

       A1: ( field R) c= X;

      R c= [:X, X:]

      proof

        let x,y be object;

        assume [x, y] in R;

        then x in ( field R) & y in ( field R) by RELAT_1: 15;

        hence thesis by A1, ZFMISC_1:def 2;

      end;

      hence thesis;

    end;

    registration

      let X be set, f be ManySortedSet of X, x,y be object;

      cluster (f +* (x,y)) -> X -defined;

      coherence

      proof

        ( dom (f +* (x,y))) = ( dom f) by FUNCT_7: 30

        .= X by PARTFUN1:def 2;

        hence thesis;

      end;

    end

    registration

      let X be set, f be ManySortedSet of X, x,y be object;

      cluster (f +* (x,y)) -> total;

      coherence

      proof

        ( dom (f +* (x,y))) = ( dom f) by FUNCT_7: 30

        .= X by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: PRE_POLY:19

    

     Th18: for f be one-to-one Function holds ( card f) = ( card ( rng f))

    proof

      let f be one-to-one Function;

      

       A1: ( rng f) = ( dom (f " )) & ( dom f) = ( rng (f " )) by FUNCT_1: 33;

      ( card ( rng f)) c= ( card ( dom f)) & ( card ( rng (f " ))) c= ( card ( dom (f " ))) by CARD_2: 61;

      then ( card ( rng f)) = ( card ( dom f)) by A1;

      hence thesis by CARD_1: 62;

    end;

    definition

      let A be set;

      let X be set, D be non empty FinSequenceSet of A, p be PartFunc of X, D, i be set;

      :: original: /.

      redefine

      func p /. i -> Element of D ;

      coherence ;

    end

    registration

      let X be set;

      cluster being_linear-order well-ordering for Order of X;

      existence

      proof

        consider R be Relation such that

         A1: R is well-ordering and

         A2: ( field R) = X by WELLSET1: 6;

        reconsider R as Relation of X by A2, Th17;

        R is reflexive by A1;

        then R is_reflexive_in X by A2;

        then ( dom R) = X by ORDERS_1: 13;

        then

        reconsider R as Order of X by A1, PARTFUN1:def 2;

        take R;

        thus thesis by A1, ORDERS_1:def 6;

      end;

    end

    theorem :: PRE_POLY:20

    

     Th19: for X be non empty set, A be non empty finite Subset of X, R be Order of X, x be Element of X st x in A & R linearly_orders A & for y be Element of X st y in A holds [x, y] in R holds (( SgmX (R,A)) /. 1) = x

    proof

      let X be non empty set, A be non empty finite Subset of X, R be Order of X, x be Element of X;

      assume that

       A1: x in A and

       A2: R linearly_orders A and

       A3: for y be Element of X st y in A holds [x, y] in R and

       A4: (( SgmX (R,A)) /. 1) <> x;

      

       A5: A = ( rng ( SgmX (R,A))) by A2, Def2;

      then

      consider i be Element of NAT such that

       A6: i in ( dom ( SgmX (R,A))) and

       A7: (( SgmX (R,A)) /. i) = x by A1, PARTFUN2: 2;

      ( SgmX (R,A)) is non empty by A2, Def2, RELAT_1: 38;

      then

       A8: 1 in ( dom ( SgmX (R,A))) by FINSEQ_5: 6;

      then

       A9: [x, (( SgmX (R,A)) /. 1)] in R by A3, A5, PARTFUN2: 2;

      

       A10: ( field R) = X by ORDERS_1: 12;

      1 <= i by A6, FINSEQ_3: 25;

      then 1 < i by A4, A7, XXREAL_0: 1;

      then [(( SgmX (R,A)) /. 1), x] in R by A2, A6, A7, A8, Def2;

      hence contradiction by A4, A9, A10, RELAT_2:def 4, RELAT_2:def 12;

    end;

    theorem :: PRE_POLY:21

    

     Th20: for X be non empty set, A be non empty finite Subset of X, R be Order of X, x be Element of X st x in A & R linearly_orders A & for y be Element of X st y in A holds [y, x] in R holds (( SgmX (R,A)) /. ( len ( SgmX (R,A)))) = x

    proof

      let X be non empty set, A be non empty finite Subset of X, R be Order of X, x be Element of X;

      assume that

       A1: x in A and

       A2: R linearly_orders A and

       A3: for y be Element of X st y in A holds [y, x] in R and

       A4: (( SgmX (R,A)) /. ( len ( SgmX (R,A)))) <> x;

      set L = ( len ( SgmX (R,A)));

      

       A5: A = ( rng ( SgmX (R,A))) by A2, Def2;

      then

      consider i be Element of NAT such that

       A6: i in ( dom ( SgmX (R,A))) and

       A7: (( SgmX (R,A)) /. i) = x by A1, PARTFUN2: 2;

      ( SgmX (R,A)) is non empty by A2, Def2, RELAT_1: 38;

      then

       A8: L in ( dom ( SgmX (R,A))) by FINSEQ_5: 6;

      then

       A9: [(( SgmX (R,A)) /. L), x] in R by A3, A5, PARTFUN2: 2;

      

       A10: ( field R) = X by ORDERS_1: 12;

      i <= L by A6, FINSEQ_3: 25;

      then i < L by A4, A7, XXREAL_0: 1;

      then [x, (( SgmX (R,A)) /. L)] in R by A2, A6, A7, A8, Def2;

      hence contradiction by A4, A9, A10, RELAT_2:def 4, RELAT_2:def 12;

    end;

    registration

      let X be non empty set, A be non empty finite Subset of X, R be being_linear-order Order of X;

      cluster ( SgmX (R,A)) -> non empty one-to-one;

      coherence

      proof

        ( field R) = X by ORDERS_1: 15;

        then R linearly_orders A by ORDERS_1: 37, ORDERS_1: 38;

        hence thesis by Th9, Def2, RELAT_1: 38;

      end;

    end

    registration

      cluster empty -> FinSequence-yielding for Function;

      coherence ;

    end

    registration

      let F,G be FinSequence-yielding FinSequence;

      cluster (F ^^ G) -> FinSequence-like;

      coherence

      proof

        ( dom (F ^^ G)) = (( dom F) /\ ( dom G)) by Def4

        .= (( Seg ( len F)) /\ ( dom G)) by FINSEQ_1:def 3

        .= (( Seg ( len F)) /\ ( Seg ( len G))) by FINSEQ_1:def 3

        .= ( Seg ( min (( len F),( len G)))) by FINSEQ_2: 2;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    registration

      let i be Element of NAT , f be FinSequence;

      cluster (i |-> f) -> FinSequence-yielding;

      coherence by FUNCOP_1: 7;

    end

    registration

      let F be FinSequence-yielding FinSequence, x be object;

      cluster (F . x) -> FinSequence-like;

      coherence

      proof

        per cases ;

          suppose not x in ( dom F);

          hence thesis by FUNCT_1:def 2;

        end;

          suppose x in ( dom F);

          hence thesis by Def3;

        end;

      end;

    end

    registration

      let F be FinSequence;

      cluster ( Card F) -> FinSequence-like;

      coherence

      proof

        ( dom ( Card F)) = ( dom F) by CARD_3:def 2

        .= ( Seg ( len F)) by FINSEQ_1:def 3;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    registration

      cluster Cardinal-yielding for FinSequence;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    theorem :: PRE_POLY:22

    

     Th21: for f be Function holds f is Cardinal-yielding iff for y be set st y in ( rng f) holds y is Cardinal

    proof

      let f be Function;

      hereby

        assume

         A1: f is Cardinal-yielding;

        let y be set;

        assume y in ( rng f);

        then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        hence y is Cardinal by A1;

      end;

      assume

       A2: for y be set st y in ( rng f) holds y is Cardinal;

      let x be object;

      assume x in ( dom f);

      then (f . x) in ( rng f) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    registration

      let F,G be Cardinal-yielding FinSequence;

      cluster (F ^ G) -> Cardinal-yielding;

      coherence

      proof

        

         A1: ( rng (F ^ G)) = (( rng F) \/ ( rng G)) by FINSEQ_1: 31;

        now

          let y be set;

          assume y in ( rng (F ^ G));

          then y in ( rng F) or y in ( rng G) by A1, XBOOLE_0:def 3;

          hence y is Cardinal by Th21;

        end;

        hence thesis by Th21;

      end;

    end

    registration

      cluster -> Cardinal-yielding for FinSequence of NAT ;

      coherence ;

    end

    registration

      cluster Cardinal-yielding for FinSequence of NAT ;

      existence

      proof

        take ( <*> NAT );

        thus thesis;

      end;

    end

    definition

      let D be set;

      let F be FinSequence of (D * );

      :: original: Card

      redefine

      func Card F -> Cardinal-yielding FinSequence of NAT ;

      coherence

      proof

        ( rng ( Card F)) c= NAT

        proof

          let y be object;

          assume y in ( rng ( Card F));

          then

          consider x be object such that

           A1: x in ( dom ( Card F)) and

           A2: y = (( Card F) . x) by FUNCT_1:def 3;

          reconsider Fx = (F . x) as finite set;

          x in ( dom F) by A1, CARD_3:def 2;

          then y = ( card Fx) by A2, CARD_3:def 2;

          hence thesis;

        end;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    registration

      let F be FinSequence of NAT , i be Element of NAT ;

      cluster (F | i) -> Cardinal-yielding;

      coherence ;

    end

    theorem :: PRE_POLY:23

    

     Th22: for F be Function, X be set holds ( Card (F | X)) = (( Card F) | X)

    proof

      let F be Function, X be set;

      

       A1: ( dom (( Card F) | X)) = (( dom ( Card F)) /\ X) by RELAT_1: 61

      .= (( dom F) /\ X) by CARD_3:def 2

      .= ( dom (F | X)) by RELAT_1: 61;

      now

        let x be object;

        

         A2: ( dom (F | X)) c= ( dom F) by RELAT_1: 60;

        assume

         A3: x in ( dom (F | X));

        

        hence ((( Card F) | X) . x) = (( Card F) . x) by A1, FUNCT_1: 47

        .= ( card (F . x)) by A3, A2, CARD_3:def 2

        .= ( card ((F | X) . x)) by A3, FUNCT_1: 47;

      end;

      hence thesis by A1, CARD_3:def 2;

    end;

    registration

      let F be empty Function;

      cluster ( Card F) -> empty;

      coherence

      proof

        ( dom F) is empty;

        then ( dom ( Card F)) is empty by CARD_3:def 2;

        hence thesis;

      end;

    end

    theorem :: PRE_POLY:24

    

     Th23: for p be set holds ( Card <*p*>) = <*( card p)*>

    proof

      let p be set;

      set Cp = <*( card p)*>;

      

       A1: ( dom Cp) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      now

        let x be object;

        assume x in ( dom Cp);

        then x = 1 by A1, TARSKI:def 1;

        hence (Cp . x) is Cardinal by FINSEQ_1: 40;

      end;

      then

      reconsider Cp as Cardinal-Function by CARD_3:def 1;

      

       A2: ( dom <*p*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      now

        let x be object;

        assume x in ( dom <*p*>);

        then

         A3: x = 1 by A2, TARSKI:def 1;

        

        hence ( <*( card p)*> . x) = ( card p) by FINSEQ_1: 40

        .= ( card ( <*p*> . x)) by A3, FINSEQ_1: 40;

      end;

      then ( Card <*p*>) = Cp by A1, A2, CARD_3:def 2;

      hence thesis;

    end;

    theorem :: PRE_POLY:25

    

     Th24: for F,G be FinSequence holds ( Card (F ^ G)) = (( Card F) ^ ( Card G))

    proof

      let F,G be FinSequence;

      

       A1: ( dom ( Card G)) = ( dom G) by CARD_3:def 2;

      then

       A2: ( len ( Card G)) = ( len G) by FINSEQ_3: 29;

      

       A3: ( dom ( Card F)) = ( dom F) by CARD_3:def 2;

      then

       A4: ( len ( Card F)) = ( len F) by FINSEQ_3: 29;

       A5:

      now

        let x be object;

        assume

         A6: x in ( dom (F ^ G));

        then

        reconsider k = x as Element of NAT ;

        x in ( Seg (( len F) + ( len G))) by A6, FINSEQ_1:def 7;

        then

         A7: 1 <= k by FINSEQ_1: 1;

        per cases ;

          suppose k <= ( len F);

          then

           A8: k in ( dom F) by A7, FINSEQ_3: 25;

          

          hence ((( Card F) ^ ( Card G)) . x) = (( Card F) . k) by A3, FINSEQ_1:def 7

          .= ( card (F . k)) by A8, CARD_3:def 2

          .= ( card ((F ^ G) . x)) by A8, FINSEQ_1:def 7;

        end;

          suppose ( len F) < k;

          then not k in ( dom F) by FINSEQ_3: 25;

          then

          consider n be Nat such that

           A9: n in ( dom G) and

           A10: k = (( len F) + n) by A6, FINSEQ_1: 25;

          

          thus ((( Card F) ^ ( Card G)) . x) = (( Card G) . n) by A1, A4, A9, A10, FINSEQ_1:def 7

          .= ( card (G . n)) by A9, CARD_3:def 2

          .= ( card ((F ^ G) . x)) by A9, A10, FINSEQ_1:def 7;

        end;

      end;

      ( dom (( Card F) ^ ( Card G))) = ( Seg (( len ( Card F)) + ( len ( Card G)))) by FINSEQ_1:def 7

      .= ( dom (F ^ G)) by A4, A2, FINSEQ_1:def 7;

      hence thesis by A5, CARD_3:def 2;

    end;

    registration

      let X be set;

      cluster ( <*> X) -> FinSequence-yielding;

      coherence ;

    end

    registration

      let f be FinSequence;

      cluster <*f*> -> FinSequence-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom <*f*>);

        then x in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then x = 1 by TARSKI:def 1;

        hence thesis by FINSEQ_1: 40;

      end;

    end

    theorem :: PRE_POLY:26

    

     Th25: for f be Function holds f is FinSequence-yielding iff for y be set st y in ( rng f) holds y is FinSequence

    proof

      let f be Function;

      hereby

        assume

         A1: f is FinSequence-yielding;

        let y be set;

        assume y in ( rng f);

        then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        hence y is FinSequence by A1;

      end;

      assume

       A2: for y be set st y in ( rng f) holds y is FinSequence;

      let x be object;

      assume x in ( dom f);

      then (f . x) in ( rng f) by FUNCT_1:def 3;

      hence thesis by A2;

    end;

    registration

      let F,G be FinSequence-yielding FinSequence;

      cluster (F ^ G) -> FinSequence-yielding;

      coherence

      proof

        

         A1: ( rng (F ^ G)) = (( rng F) \/ ( rng G)) by FINSEQ_1: 31;

        now

          let y be set;

          assume y in ( rng (F ^ G));

          then y in ( rng F) or y in ( rng G) by A1, XBOOLE_0:def 3;

          hence y is FinSequence by Th25;

        end;

        hence thesis by Th25;

      end;

    end

    registration

      let D be set, F be empty FinSequence of (D * );

      cluster ( FlattenSeq F) -> empty;

      coherence

      proof

        F = ( <*> (D * ));

        then ( FlattenSeq F) = ( <*> D) by Th2;

        hence thesis;

      end;

    end

    theorem :: PRE_POLY:27

    

     Th26: for D be set, F be FinSequence of (D * ) holds ( len ( FlattenSeq F)) = ( Sum ( Card F))

    proof

      let D be set;

      defpred P[ FinSequence of (D * )] means ( len ( FlattenSeq $1)) = ( Sum ( Card $1));

       A1:

      now

        let F be FinSequence of (D * ), p be Element of (D * ) such that

         A2: P[F];

        ( len ( FlattenSeq (F ^ <*p*>))) = ( len (( FlattenSeq F) ^ ( FlattenSeq <*p*>))) by Th3

        .= (( Sum ( Card F)) + ( len ( FlattenSeq <*p*>))) by A2, FINSEQ_1: 22

        .= (( Sum ( Card F)) + ( len p)) by Th1

        .= ( Sum (( Card F) ^ <*( len p)*>)) by RVSUM_1: 74

        .= ( Sum (( Card F) ^ ( Card <*p*>))) by Th23

        .= ( Sum ( Card (F ^ <*p*>))) by Th24;

        hence P[(F ^ <*p*>)];

      end;

      

       A3: P[( <*> (D * ))] by RVSUM_1: 72;

      thus for F be FinSequence of (D * ) holds P[F] from FINSEQ_2:sch 2( A3, A1);

    end;

    theorem :: PRE_POLY:28

    

     Th27: for D,E be set, F be FinSequence of (D * ), G be FinSequence of (E * ) st ( Card F) = ( Card G) holds ( len ( FlattenSeq F)) = ( len ( FlattenSeq G))

    proof

      let D,E be set, F be FinSequence of (D * ), G be FinSequence of (E * );

      assume ( Card F) = ( Card G);

      

      hence ( len ( FlattenSeq F)) = ( Sum ( Card G)) by Th26

      .= ( len ( FlattenSeq G)) by Th26;

    end;

    theorem :: PRE_POLY:29

    

     Th28: for D be set, F be FinSequence of (D * ), k be set st k in ( dom ( FlattenSeq F)) holds ex i,j be Nat st i in ( dom F) & j in ( dom (F . i)) & k = (( Sum ( Card (F | (i -' 1)))) + j) & ((F . i) . j) = (( FlattenSeq F) . k)

    proof

      let D be set;

      set F = ( <*> (D * ));

      defpred P[ FinSequence of (D * )] means for k be set st k in ( dom ( FlattenSeq $1)) holds ex i,j be Nat st i in ( dom $1) & j in ( dom ($1 . i)) & k = (( Sum ( Card ($1 | (i -' 1)))) + j) & (($1 . i) . j) = (( FlattenSeq $1) . k);

      

       A1: for F be FinSequence of (D * ), p be Element of (D * ) st P[F] holds P[(F ^ <*p*>)]

      proof

        let F be FinSequence of (D * ), p be Element of (D * );

        assume

         A2: P[F];

        let k be set;

        

         A3: ( FlattenSeq (F ^ <*p*>)) = (( FlattenSeq F) ^ ( FlattenSeq <*p*>)) by Th3

        .= (( FlattenSeq F) ^ p) by Th1;

        

         A4: ( Sum ( Card F)) = ( len ( FlattenSeq F)) & ((F ^ <*p*>) | ( len F)) = F by Th26, FINSEQ_5: 23;

        assume

         A5: k in ( dom ( FlattenSeq (F ^ <*p*>)));

        then

        reconsider m = k as Element of NAT ;

        per cases ;

          suppose

           A6: not k in ( dom ( FlattenSeq F));

          take i = (( len F) + 1);

          take j = (m -' ( Sum ( Card ((F ^ <*p*>) | (i -' 1)))));

          

           A7: 1 <= (( len F) + 1) by NAT_1: 11;

          ( len (F ^ <*p*>)) = (( len F) + ( len <*p*>)) by FINSEQ_1: 22

          .= (( len F) + 1) by FINSEQ_1: 39;

          hence i in ( dom (F ^ <*p*>)) by A7, FINSEQ_3: 25;

          

           A8: ( Sum ( Card ((F ^ <*p*>) | (i -' 1)))) = ( len ( FlattenSeq F)) by A4, NAT_D: 34;

          m <= ( len (( FlattenSeq F) ^ p)) by A5, A3, FINSEQ_3: 25;

          then m <= (( len ( FlattenSeq F)) + ( len p)) by FINSEQ_1: 22;

          then

           A9: j <= ( len p) by A8, NAT_D: 53;

          1 in ( dom <*p*>) by FINSEQ_5: 6;

          

          then

           A10: ((F ^ <*p*>) . i) = ( <*p*> . 1) by FINSEQ_1:def 7

          .= p by FINSEQ_1: 40;

          1 <= m by A5, FINSEQ_3: 25;

          then

           A11: ( len ( FlattenSeq F)) < m by A6, FINSEQ_3: 25;

          then (( len ( FlattenSeq F)) + 1) <= m by NAT_1: 13;

          hence

           A12: j in ( dom ((F ^ <*p*>) . i)) by A10, A9, A8, FINSEQ_3: 25, NAT_D: 55;

          thus k = (( Sum ( Card ((F ^ <*p*>) | (i -' 1)))) + j) by A8, A11, XREAL_1: 235;

          hence thesis by A3, A8, A10, A12, FINSEQ_1:def 7;

        end;

          suppose

           A13: k in ( dom ( FlattenSeq F));

          then

          consider i,j be Nat such that

           A14: i in ( dom F) and

           A15: j in ( dom (F . i)) and

           A16: k = (( Sum ( Card (F | (i -' 1)))) + j) and

           A17: ((F . i) . j) = (( FlattenSeq F) . k) by A2;

          take i, j;

          ( dom F) c= ( dom (F ^ <*p*>)) by FINSEQ_1: 26;

          hence i in ( dom (F ^ <*p*>)) by A14;

          thus j in ( dom ((F ^ <*p*>) . i)) by A14, A15, FINSEQ_1:def 7;

          

           A18: (i -' 1) <= i by NAT_D: 35;

          i <= ( len F) by A14, FINSEQ_3: 25;

          hence k = (( Sum ( Card ((F ^ <*p*>) | (i -' 1)))) + j) by A16, A18, FINSEQ_5: 22, XXREAL_0: 2;

          ((F ^ <*p*>) . i) = (F . i) by A14, FINSEQ_1:def 7;

          hence thesis by A3, A13, A17, FINSEQ_1:def 7;

        end;

      end;

      

       A19: P[F];

      thus for F be FinSequence of (D * ) holds P[F] from FINSEQ_2:sch 2( A19, A1);

    end;

    theorem :: PRE_POLY:30

    

     Th29: for D be set, F be FinSequence of (D * ), i,j be Element of NAT st i in ( dom F) & j in ( dom (F . i)) holds (( Sum ( Card (F | (i -' 1)))) + j) in ( dom ( FlattenSeq F)) & ((F . i) . j) = (( FlattenSeq F) . (( Sum ( Card (F | (i -' 1)))) + j))

    proof

      let D be set;

      set F = ( <*> (D * ));

      defpred P[ FinSequence of (D * )] means for i,j be Element of NAT st i in ( dom $1) & j in ( dom ($1 . i)) holds (( Sum ( Card ($1 | (i -' 1)))) + j) in ( dom ( FlattenSeq $1)) & (($1 . i) . j) = (( FlattenSeq $1) . (( Sum ( Card ($1 | (i -' 1)))) + j));

      

       A1: for F be FinSequence of (D * ), p be Element of (D * ) st P[F] holds P[(F ^ <*p*>)]

      proof

        let F be FinSequence of (D * ), p be Element of (D * );

        assume

         A2: for i,j be Element of NAT st i in ( dom F) & j in ( dom (F . i)) holds (( Sum ( Card (F | (i -' 1)))) + j) in ( dom ( FlattenSeq F)) & ((F . i) . j) = (( FlattenSeq F) . (( Sum ( Card (F | (i -' 1)))) + j));

        let i,j be Element of NAT ;

        assume that

         A3: i in ( dom (F ^ <*p*>)) and

         A4: j in ( dom ((F ^ <*p*>) . i));

        

         A5: ( FlattenSeq (F ^ <*p*>)) = (( FlattenSeq F) ^ ( FlattenSeq <*p*>)) by Th3

        .= (( FlattenSeq F) ^ p) by Th1;

        per cases ;

          suppose

           A6: not i in ( dom F);

          1 <= i by A3, FINSEQ_3: 25;

          then ( len F) < i by A6, FINSEQ_3: 25;

          then

           A7: (( len F) + 1) <= i by NAT_1: 13;

          

           A8: ( len (F ^ <*p*>)) = (( len F) + ( len <*p*>)) by FINSEQ_1: 22

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

          i <= ( len (F ^ <*p*>)) by A3, FINSEQ_3: 25;

          then

           A9: i = (( len F) + 1) by A8, A7, XXREAL_0: 1;

          then (i -' 1) = ( len F) by NAT_D: 34;

          then

           A10: ((F ^ <*p*>) | (i -' 1)) = F by FINSEQ_5: 23;

          

           A11: ( Sum ( Card F)) = ( len ( FlattenSeq F)) by Th26;

          1 in ( dom <*p*>) by FINSEQ_5: 6;

          

          then

           A12: ((F ^ <*p*>) . i) = ( <*p*> . 1) by A9, FINSEQ_1:def 7

          .= p by FINSEQ_1: 40;

          hence (( Sum ( Card ((F ^ <*p*>) | (i -' 1)))) + j) in ( dom ( FlattenSeq (F ^ <*p*>))) by A4, A5, A10, A11, FINSEQ_1: 28;

          thus thesis by A4, A5, A12, A10, A11, FINSEQ_1:def 7;

        end;

          suppose

           A13: i in ( dom F);

          then

           A14: j in ( dom (F . i)) by A4, FINSEQ_1:def 7;

          then

           A15: (( Sum ( Card (F | (i -' 1)))) + j) in ( dom ( FlattenSeq F)) by A2, A13;

          

           A16: (i -' 1) <= i by NAT_D: 35;

          i <= ( len F) by A13, FINSEQ_3: 25;

          then

           A17: ((F ^ <*p*>) | (i -' 1)) = (F | (i -' 1)) by A16, FINSEQ_5: 22, XXREAL_0: 2;

          ( dom ( FlattenSeq F)) c= ( dom ( FlattenSeq (F ^ <*p*>))) by A5, FINSEQ_1: 26;

          hence (( Sum ( Card ((F ^ <*p*>) | (i -' 1)))) + j) in ( dom ( FlattenSeq (F ^ <*p*>))) by A17, A15;

          

          thus (((F ^ <*p*>) . i) . j) = ((F . i) . j) by A13, FINSEQ_1:def 7

          .= (( FlattenSeq F) . (( Sum ( Card (F | (i -' 1)))) + j)) by A2, A13, A14

          .= (( FlattenSeq (F ^ <*p*>)) . (( Sum ( Card ((F ^ <*p*>) | (i -' 1)))) + j)) by A5, A17, A15, FINSEQ_1:def 7;

        end;

      end;

      

       A18: P[F];

      thus for F be FinSequence of (D * ) holds P[F] from FINSEQ_2:sch 2( A18, A1);

    end;

    theorem :: PRE_POLY:31

    

     Th30: for X,Y be non empty set, f be FinSequence of (X * ), v be Function of X, Y holds ((( dom f) --> v) ** f) is FinSequence of (Y * )

    proof

      let X,Y be non empty set, f be FinSequence of (X * ), v be Function of X, Y;

      set F = ((( dom f) --> v) ** f);

      

       A1: ( dom F) = (( dom (( dom f) --> v)) /\ ( dom f)) by PBOOLE:def 19

      .= (( dom f) /\ ( dom f))

      .= ( dom f);

      

       A2: ( rng F) c= (Y * )

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A3: x in ( dom F) and

         A4: y = (F . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A1, A3;

        (f . x) in (X * ) by A1, A3, FINSEQ_2: 11;

        then

         A5: (f . x) is FinSequence of X by FINSEQ_1:def 11;

        y = (((( dom f) --> v) . x) * (f . x)) by A3, A4, PBOOLE:def 19

        .= (v * (f . x)) by A1, A3, FUNCOP_1: 7;

        then y is FinSequence of Y by A5, FINSEQ_2: 32;

        hence thesis by FINSEQ_1:def 11;

      end;

      ( dom F) = ( Seg ( len f)) by A1, FINSEQ_1:def 3;

      then F is FinSequence-like by FINSEQ_1:def 2;

      hence thesis by A2, FINSEQ_1:def 4;

    end;

    theorem :: PRE_POLY:32

    for X,Y be non empty set, f be FinSequence of (X * ), v be Function of X, Y holds ex F be FinSequence of (Y * ) st F = ((( dom f) --> v) ** f) & (v * ( FlattenSeq f)) = ( FlattenSeq F)

    proof

      let X,Y be non empty set, f be FinSequence of (X * ), v be Function of X, Y;

      reconsider F = ((( dom f) --> v) ** f) as FinSequence of (Y * ) by Th30;

      take F;

      thus F = ((( dom f) --> v) ** f);

      set Fl = ( FlattenSeq F);

      set fl = ( FlattenSeq f);

      reconsider vfl = (v * fl) as FinSequence of Y;

      now

        ( len fl) = ( len vfl) by FINSEQ_2: 33;

        hence

         A1: ( dom fl) = ( dom vfl) by FINSEQ_3: 29;

        

         A2: ( dom F) = (( dom (( dom f) --> v)) /\ ( dom f)) by PBOOLE:def 19

        .= (( dom f) /\ ( dom f))

        .= ( dom f);

         A3:

        now

          let k be object;

          assume

           A4: k in ( dom f);

          then

          reconsider k1 = k as Element of NAT ;

          

           A5: (F . k) = (((( dom f) --> v) . k) * (f . k)) by A2, A4, PBOOLE:def 19

          .= (v * (f . k)) by A4, FUNCOP_1: 7;

          (f . k1) in (X * ) by A4, FINSEQ_2: 11;

          then

          reconsider fk = (f . k) as FinSequence of X by FINSEQ_1:def 11;

          

          thus (( Card f) . k) = ( len fk) by A4, CARD_3:def 2

          .= ( len (F . k1)) by A5, FINSEQ_2: 33

          .= (( Card F) . k) by A2, A4, CARD_3:def 2;

        end;

        

         A6: ( dom f) = ( dom ( Card f)) & ( dom f) = ( dom ( Card F)) by A2, CARD_3:def 2;

        then

         A7: ( Card f) = ( Card F) by A3;

        ( len fl) = ( len Fl) by A6, A3, Th27, FUNCT_1: 2;

        hence ( dom fl) = ( dom Fl) by FINSEQ_3: 29;

        let k be Nat;

        assume

         A8: k in ( dom fl);

        then

        consider i,j be Nat such that

         A9: i in ( dom f) and

         A10: j in ( dom (f . i)) and

         A11: k = (( Sum ( Card (f | (i -' 1)))) + j) and

         A12: ((f . i) . j) = (fl . k) by Th28;

        (f . i) in (X * ) by A9, FINSEQ_2: 11;

        then

        reconsider fi = (f . i) as FinSequence of X by FINSEQ_1:def 11;

        (F . i) = (((( dom f) --> v) . i) * (f . i)) by A2, A9, PBOOLE:def 19

        .= (v * (f . i)) by A9, FUNCOP_1: 7;

        then ( len fi) = ( len (F . i)) by FINSEQ_2: 33;

        then

         A13: j in ( dom (F . i)) by A10, FINSEQ_3: 29;

        (f . i) in (X * ) by A9, FINSEQ_2: 11;

        then ( dom v) = X & (f . i) is FinSequence of X by FINSEQ_1:def 11, FUNCT_2:def 1;

        then ( rng (f . i)) c= ( dom v) by FINSEQ_1:def 4;

        then

         A14: j in ( dom (v * (f . i))) by A10, RELAT_1: 27;

        ( Card (F | (i -' 1))) = ( Card (F | ( Seg (i -' 1)))) by FINSEQ_1:def 15

        .= (( Card f) | ( Seg (i -' 1))) by A7, Th22

        .= ( Card (f | ( Seg (i -' 1)))) by Th22

        .= ( Card (f | (i -' 1))) by FINSEQ_1:def 15;

        

        then (Fl . k) = ((F . i) . j) by A2, A9, A11, A13, Th29

        .= ((((( dom f) --> v) . i) * (f . i)) . j) by A2, A9, PBOOLE:def 19

        .= ((v * (f . i)) . j) by A9, FUNCOP_1: 7

        .= (v . ((f . i) . j)) by A14, FUNCT_1: 12;

        hence (vfl . k) = (Fl . k) by A1, A8, A12, FUNCT_1: 12;

      end;

      hence thesis;

    end;

    begin

    registration

      let f be natural-valued Function, x be object, n be Nat;

      cluster (f +* (x,n)) -> natural-valued;

      coherence

      proof

        set F = (f +* (x,n));

        let a be object such that a in ( dom F);

        per cases ;

          suppose x in ( dom f) & x = a;

          hence thesis by FUNCT_7: 31;

        end;

          suppose x in ( dom f) & x <> a;

          then (F . a) = (f . a) by FUNCT_7: 32;

          hence thesis;

        end;

          suppose not x in ( dom f);

          then (F . a) = (f . a) by FUNCT_7:def 3;

          hence thesis;

        end;

      end;

    end

    registration

      let f be real-valued Function, x be object, n be Real;

      cluster (f +* (x,n)) -> real-valued;

      coherence

      proof

        set F = (f +* (x,n));

        let a be object such that a in ( dom F);

        per cases ;

          suppose x in ( dom f) & x = a;

          hence thesis by FUNCT_7: 31;

        end;

          suppose x in ( dom f) & x <> a;

          then (F . a) = (f . a) by FUNCT_7: 32;

          hence thesis;

        end;

          suppose not x in ( dom f);

          then (F . a) = (f . a) by FUNCT_7:def 3;

          hence thesis;

        end;

      end;

    end

    definition

      let X be set, b1,b2 be complex-valued ManySortedSet of X;

      :: original: +

      redefine

      :: PRE_POLY:def5

      func b1 + b2 -> ManySortedSet of X means

      : Def5: for x be object holds (it . x) = ((b1 . x) + (b2 . x));

      coherence ;

      compatibility

      proof

        let f be ManySortedSet of X;

        

         A1: ( dom b1) = X & ( dom b2) = X by PARTFUN1:def 2;

        then

         A2: ( dom f) = (( dom b1) /\ ( dom b2)) by PARTFUN1:def 2;

        thus f = (b1 + b2) implies for x be object holds (f . x) = ((b1 . x) + (b2 . x))

        proof

          assume

           A3: f = (b1 + b2);

          let x be object;

          per cases ;

            suppose x in X;

            hence thesis by A1, A2, A3, VALUED_1:def 1;

          end;

            suppose

             A4: not x in X;

            then (b1 . x) = 0 & (b2 . x) = 0 by A1, FUNCT_1:def 2;

            hence thesis by A1, A2, A4, FUNCT_1:def 2;

          end;

        end;

        assume for x be object holds (f . x) = ((b1 . x) + (b2 . x));

        then for c be object st c in ( dom f) holds (f . c) = ((b1 . c) + (b2 . c));

        hence thesis by A2, VALUED_1:def 1;

      end;

    end

    definition

      let X be set, b1,b2 be natural-valued ManySortedSet of X;

      :: PRE_POLY:def6

      func b1 -' b2 -> ManySortedSet of X means

      : Def6: for x be object holds (it . x) = ((b1 . x) -' (b2 . x));

      existence

      proof

        deffunc F( object) = ((b1 . $1) -' (b2 . $1));

        consider f be ManySortedSet of X such that

         A1: for i be object st i in X holds (f . i) = F(i) from PBOOLE:sch 4;

        take f;

        let x be object;

        per cases ;

          suppose x in X;

          hence thesis by A1;

        end;

          suppose

           A2: not x in X;

          

           A3: ( dom b2) = X by PARTFUN1:def 2;

          

           A4: ( dom b1) = X by PARTFUN1:def 2;

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

          

          hence (f . x) = 0 by A2, FUNCT_1:def 2

          .= ( 0 -' 0 ) by XREAL_1: 232

          .= ( 0 -' (b2 . x)) by A2, A3, FUNCT_1:def 2

          .= ((b1 . x) -' (b2 . x)) by A2, A4, FUNCT_1:def 2;

        end;

      end;

      uniqueness

      proof

        let it1,it2 be ManySortedSet of X such that

         A5: for x be object holds (it1 . x) = ((b1 . x) -' (b2 . x)) and

         A6: for x be object holds (it2 . x) = ((b1 . x) -' (b2 . x));

        now

          let x be object;

          assume x in X;

          

          thus (it1 . x) = ((b1 . x) -' (b2 . x)) by A5

          .= (it2 . x) by A6;

        end;

        hence it1 = it2;

      end;

    end

    theorem :: PRE_POLY:33

    for X be set, b,b1,b2 be real-valued ManySortedSet of X st for x be object st x in X holds (b . x) = ((b1 . x) + (b2 . x)) holds b = (b1 + b2)

    proof

      let X be set, b,b1,b2 be real-valued ManySortedSet of X;

      assume

       A1: for x be object st x in X holds (b . x) = ((b1 . x) + (b2 . x));

      now

        let x be object;

        per cases ;

          suppose x in X;

          hence (b . x) = ((b1 . x) + (b2 . x)) by A1;

        end;

          suppose

           A2: not x in X;

          

           A3: ( dom b2) = X by PARTFUN1:def 2;

          

           A4: ( dom b1) = X by PARTFUN1:def 2;

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

          

          hence (b . x) = ( 0 qua Nat + 0 qua Nat) by A2, FUNCT_1:def 2

          .= ( 0 qua Nat + (b2 . x)) by A2, A3, FUNCT_1:def 2

          .= ((b1 . x) + (b2 . x)) by A2, A4, FUNCT_1:def 2;

        end;

      end;

      hence thesis by Def5;

    end;

    theorem :: PRE_POLY:34

    

     Th33: for X be set, b,b1,b2 be natural-valued ManySortedSet of X st for x be object st x in X holds (b . x) = ((b1 . x) -' (b2 . x)) holds b = (b1 -' b2)

    proof

      let X be set, b,b1,b2 be natural-valued ManySortedSet of X;

      assume

       A1: for x be object st x in X holds (b . x) = ((b1 . x) -' (b2 . x));

      now

        let x be object;

        per cases ;

          suppose x in X;

          hence (b . x) = ((b1 . x) -' (b2 . x)) by A1;

        end;

          suppose

           A2: not x in X;

          

           A3: ( dom b2) = X by PARTFUN1:def 2;

          

           A4: ( dom b1) = X by PARTFUN1:def 2;

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

          

          hence (b . x) = 0 by A2, FUNCT_1:def 2

          .= ( 0 -' 0 ) by XREAL_1: 232

          .= ( 0 -' (b2 . x)) by A2, A3, FUNCT_1:def 2

          .= ((b1 . x) -' (b2 . x)) by A2, A4, FUNCT_1:def 2;

        end;

      end;

      hence thesis by Def6;

    end;

    registration

      let X be set, b1,b2 be natural-valued ManySortedSet of X;

      cluster (b1 + b2) -> natural-valued;

      coherence ;

      cluster (b1 -' b2) -> natural-valued;

      coherence

      proof

        set f = (b1 -' b2);

        ( rng f) c= NAT

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that x in ( dom f) and

           A1: y = (f . x) by FUNCT_1:def 3;

          (f . x) = ((b1 . x) -' (b2 . x)) by Def6;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: PRE_POLY:35

    

     Th34: for X be set, b1,b2,b3 be real-valued ManySortedSet of X holds ((b1 + b2) + b3) = (b1 + (b2 + b3))

    proof

      let X be set, b1,b2,b3 be real-valued ManySortedSet of X;

      now

        let x be object;

        assume x in X;

        

        thus (((b1 + b2) + b3) . x) = (((b1 + b2) . x) + (b3 . x)) by Def5

        .= (((b1 . x) + (b2 . x)) + (b3 . x)) by Def5

        .= ((b1 . x) + ((b2 . x) + (b3 . x)))

        .= ((b1 . x) + ((b2 + b3) . x)) by Def5

        .= ((b1 + (b2 + b3)) . x) by Def5;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:36

    for X be set, b,c,d be natural-valued ManySortedSet of X holds ((b -' c) -' d) = (b -' (c + d))

    proof

      let X be set, b,c,d be natural-valued ManySortedSet of X;

      now

        let x be object;

        assume x in X;

        

        thus (((b -' c) -' d) . x) = (((b -' c) . x) -' (d . x)) by Def6

        .= (((b . x) -' (c . x)) -' (d . x)) by Def6

        .= ((b . x) -' ((c . x) + (d . x))) by NAT_2: 30

        .= ((b . x) -' ((c + d) . x)) by Def5;

      end;

      hence thesis by Th33;

    end;

    begin

    definition

      let f be Function;

      :: PRE_POLY:def7

      func support f -> set means

      : Def7: for x be object holds x in it iff (f . x) <> 0 ;

      existence

      proof

        defpred P[ object] means (f . $1) <> 0 ;

        consider A be set such that

         A1: for x be object holds x in A iff x in ( dom f) & P[x] from XBOOLE_0:sch 1;

        take A;

        let x be object;

        thus x in A implies (f . x) <> 0 by A1;

        assume

         A2: (f . x) <> 0 ;

        then x in ( dom f) by FUNCT_1:def 2;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let A,B be set such that

         A3: for x be object holds x in A iff (f . x) <> 0 and

         A4: for x be object holds x in B iff (f . x) <> 0 ;

        for x be object holds x in A iff x in B

        proof

          let x be object;

          x in A iff (f . x) <> 0 by A3;

          hence thesis by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: PRE_POLY:37

    

     Th36: for f be Function holds ( support f) c= ( dom f)

    proof

      let f be Function, x be object;

      assume x in ( support f);

      then (f . x) <> 0 by Def7;

      hence thesis by FUNCT_1:def 2;

    end;

    definition

      let f be Function;

      :: PRE_POLY:def8

      attr f is finite-support means

      : Def8: ( support f) is finite;

    end

    registration

      cluster finite -> finite-support for Function;

      coherence

      proof

        let f be Function;

        assume f is finite;

        then ( dom f) is finite;

        hence ( support f) is finite by Th36, FINSET_1: 1;

      end;

    end

    registration

      cluster natural-valued finite-support non empty for Function;

      existence

      proof

        take f = ( 0 .--> 1);

        thus f is natural-valued;

        thus f is finite-support;

        thus thesis;

      end;

    end

    registration

      let f be finite-support Function;

      cluster ( support f) -> finite;

      coherence by Def8;

    end

    registration

      let X be set;

      cluster finite-support for Function of X, NAT ;

      existence

      proof

        set f = (X --> 0 );

        reconsider f as Function of X, NAT ;

        take f;

        now

          assume ( support f) <> {} ;

          then

          consider x be object such that

           A3: x in ( support f) by XBOOLE_0:def 1;

          (f . x) <> 0 by A3, Def7;

          hence contradiction;

        end;

        hence ( support f) is finite;

      end;

    end

    registration

      let f be finite-support Function, x,y be set;

      cluster (f +* (x,y)) -> finite-support;

      coherence

      proof

        set F = (f +* (x,y));

        ( support F) c= (( support f) \/ {x})

        proof

          let a be object;

          assume a in ( support F);

          then

           A1: (F . a) <> 0 by Def7;

          per cases ;

            suppose x in ( dom f) & a = x;

            then a in {x} by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose x in ( dom f) & a <> x;

            then (F . a) = (f . a) by FUNCT_7: 32;

            then a in ( support f) by A1, Def7;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose not x in ( dom f);

            then (F . a) = (f . a) by FUNCT_7:def 3;

            then a in ( support f) by A1, Def7;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        hence ( support (f +* (x,y))) is finite;

      end;

    end

    registration

      let X be set;

      cluster natural-valued finite-support for ManySortedSet of X;

      existence

      proof

        set f = (X --> 0 );

        reconsider f as ManySortedSet of X;

        take f;

        thus f is natural-valued;

        ( support f) = {}

        proof

          assume not thesis;

          then

          consider x be object such that

           A2: x in ( support f) by XBOOLE_0:def 1;

          (f . x) = 0 ;

          hence contradiction by A2, Def7;

        end;

        hence thesis;

      end;

    end

    theorem :: PRE_POLY:38

    

     Th37: for X be set, b1,b2 be natural-valued ManySortedSet of X holds ( support (b1 + b2)) = (( support b1) \/ ( support b2))

    proof

      let X be set, b1,b2 be natural-valued ManySortedSet of X;

      now

        let x be object;

        hereby

          assume x in (( support b1) \/ ( support b2));

          then x in ( support b1) or x in ( support b2) by XBOOLE_0:def 3;

          then (b1 . x) <> 0 or (b2 . x) <> 0 by Def7;

          then ((b1 . x) + (b2 . x)) <> 0 ;

          hence ((b1 + b2) . x) <> 0 by Def5;

        end;

        assume

         A1: ((b1 + b2) . x) <> 0 ;

        assume

         A2: not x in (( support b1) \/ ( support b2));

        then not x in ( support b1) by XBOOLE_0:def 3;

        then

         A3: (b1 . x) = 0 by Def7;

         not x in ( support b2) by A2, XBOOLE_0:def 3;

        then ((b1 . x) + (b2 . x)) = 0 by A3, Def7;

        hence contradiction by A1, Def5;

      end;

      hence thesis by Def7;

    end;

    theorem :: PRE_POLY:39

    

     Th38: for X be set, b1,b2 be natural-valued ManySortedSet of X holds ( support (b1 -' b2)) c= ( support b1)

    proof

      let X be set, b1,b2 be natural-valued ManySortedSet of X;

      thus ( support (b1 -' b2)) c= ( support b1)

      proof

        let x be object;

        assume

         A1: x in ( support (b1 -' b2));

        assume not x in ( support b1);

        then (b1 . x) = 0 by Def7;

        then ((b1 . x) -' (b2 . x)) = 0 by NAT_2: 8;

        then ((b1 -' b2) . x) = 0 by Def6;

        hence contradiction by A1, Def7;

      end;

    end;

    begin

    definition

      let X be set;

      mode bag of X is natural-valued finite-support ManySortedSet of X;

    end

    registration

      let X be finite set;

      cluster -> finite-support for ManySortedSet of X;

      coherence

      proof

        let f be ManySortedSet of X;

        ( support f) c= ( dom f) & ( dom f) = X by Th36, PARTFUN1:def 2;

        hence ( support f) is finite;

      end;

    end

    registration

      let X be set, b1,b2 be bag of X;

      cluster (b1 + b2) -> finite-support;

      coherence

      proof

        ( support (b1 + b2)) = (( support b1) \/ ( support b2)) by Th37;

        hence ( support (b1 + b2)) is finite;

      end;

      cluster (b1 -' b2) -> finite-support;

      coherence

      proof

        ( support (b1 -' b2)) c= ( support b1) by Th38;

        hence ( support (b1 -' b2)) is finite;

      end;

    end

    theorem :: PRE_POLY:40

    

     Th39: for X be set holds (X --> 0 ) is bag of X

    proof

      let X be set;

      set f = (X --> 0 );

      ( support f) = {}

      proof

        assume not thesis;

        then

        consider x be object such that

         A2: x in ( support f) by XBOOLE_0:def 1;

        (f . x) = 0 ;

        hence contradiction by A2, Def7;

      end;

      hence thesis by Def8;

    end;

    definition

      let n be Ordinal, p,q be bag of n;

      :: PRE_POLY:def9

      pred p < q means ex k be Ordinal st (p . k) < (q . k) & for l be Ordinal st l in k holds (p . l) = (q . l);

      asymmetry

      proof

        let p,q be bag of n;

        given k be Ordinal such that

         A1: (p . k) < (q . k) and

         A2: for l be Ordinal st l in k holds (p . l) = (q . l);

        given k1 be Ordinal such that

         A3: (q . k1) < (p . k1) and

         A4: for l be Ordinal st l in k1 holds (q . l) = (p . l);

        per cases by ORDINAL1: 14;

          suppose k in k1;

          hence contradiction by A1, A4;

        end;

          suppose k1 in k;

          hence contradiction by A2, A3;

        end;

          suppose k1 = k;

          hence contradiction by A1, A3;

        end;

      end;

    end

    theorem :: PRE_POLY:41

    

     Th40: for n be Ordinal, p,q,r be bag of n st p < q & q < r holds p < r

    proof

      let n be Ordinal, p,q,r be bag of n;

      assume that

       A1: p < q and

       A2: q < r;

      consider k be Ordinal such that

       A3: (p . k) < (q . k) and

       A4: for l be Ordinal st l in k holds (p . l) = (q . l) by A1;

      consider m be Ordinal such that

       A5: (q . m) < (r . m) and

       A6: for l be Ordinal st l in m holds (q . l) = (r . l) by A2;

      take n = (k /\ m);

      

       A7: n c= m & n <> m iff n c< m;

      

       A8: n c= k & n <> k iff n c< k;

      now

        per cases by ORDINAL1: 14;

          suppose k in m;

          hence (p . n) < (r . n) by A3, A6, A8, A7, ORDINAL1: 11, ORDINAL3: 13, XBOOLE_1: 17;

        end;

          suppose m in k;

          hence (p . n) < (r . n) by A4, A5, A8, A7, ORDINAL1: 11, ORDINAL3: 13, XBOOLE_1: 17;

        end;

          suppose m = k;

          hence (p . n) < (r . n) by A3, A5, XXREAL_0: 2;

        end;

      end;

      hence (p . n) < (r . n);

      let l be Ordinal;

      

       A9: n c= m by XBOOLE_1: 17;

      assume

       A10: l in n;

      n c= k by XBOOLE_1: 17;

      

      hence (p . l) = (q . l) by A4, A10

      .= (r . l) by A6, A9, A10;

    end;

    definition

      let n be Ordinal, p,q be bag of n;

      :: PRE_POLY:def10

      pred p <=' q means p < q or p = q;

      reflexivity ;

    end

    theorem :: PRE_POLY:42

    

     Th41: for n be Ordinal, p,q,r be bag of n st p <=' q & q <=' r holds p <=' r by Th40;

    theorem :: PRE_POLY:43

    for n be Ordinal, p,q,r be bag of n st p < q & q <=' r holds p < r by Th40;

    theorem :: PRE_POLY:44

    for n be Ordinal, p,q,r be bag of n st p <=' q & q < r holds p < r by Th40;

    theorem :: PRE_POLY:45

    

     Th44: for n be Ordinal, p,q be bag of n holds p <=' q or q <=' p

    proof

      let n be Ordinal, p,q be bag of n;

      assume

       A1: not p <=' q;

      then

      consider i be object such that

       A2: i in n and

       A3: (p . i) <> (q . i) by PBOOLE: 3;

      

       A4: not p < q by A1;

      defpred P[ set] means (p . $1) <> (q . $1);

      

       A5: ex i be Ordinal st P[i] by A2, A3;

      consider m be Ordinal such that

       A6: P[m] and

       A7: for n be Ordinal st P[n] holds m c= n from ORDINAL1:sch 1( A5);

      

       A8: for l be Ordinal st l in m holds (q . l) = (p . l) by A7, ORDINAL1: 5;

      per cases by A6, XXREAL_0: 1;

        suppose (p . m) < (q . m);

        hence thesis by A4, A8;

      end;

        suppose (p . m) > (q . m);

        then q < p by A8;

        hence thesis;

      end;

    end;

    definition

      let X be set, d,b be bag of X;

      :: PRE_POLY:def11

      pred d divides b means for k be object holds (d . k) <= (b . k);

      reflexivity ;

    end

    theorem :: PRE_POLY:46

    

     Th45: for n be set, d,b be bag of n st for k be object st k in n holds (d . k) <= (b . k) holds d divides b

    proof

      let n be set, d,b be bag of n;

      assume

       A1: for k be object st k in n holds (d . k) <= (b . k);

      let k be object;

      per cases ;

        suppose k in ( dom d);

        then k in n;

        hence thesis by A1;

      end;

        suppose not k in ( dom d);

        hence thesis by FUNCT_1:def 2;

      end;

    end;

    theorem :: PRE_POLY:47

    

     Th46: for n be set, b1,b2 be bag of n st b1 divides b2 holds ((b2 -' b1) + b1) = b2

    proof

      let n be set, b1,b2 be bag of n such that

       A1: b1 divides b2;

      now

        let k be object;

        assume k in n;

        

         A2: (b1 . k) <= (b2 . k) by A1;

        

        thus (((b2 -' b1) + b1) . k) = (((b2 -' b1) . k) + (b1 . k)) by Def5

        .= (((b2 . k) -' (b1 . k)) + (b1 . k)) by Def6

        .= (((b2 . k) + (b1 . k)) -' (b1 . k)) by A2, NAT_D: 38

        .= (b2 . k) by NAT_D: 34;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:48

    

     Th47: for X be set, b1,b2 be bag of X holds ((b2 + b1) -' b1) = b2

    proof

      let X be set, b1,b2 be bag of X;

      now

        let k be object;

        assume k in X;

        

        thus (((b2 + b1) -' b1) . k) = (((b2 + b1) . k) -' (b1 . k)) by Def6

        .= (((b2 . k) + (b1 . k)) -' (b1 . k)) by Def5

        .= (b2 . k) by NAT_D: 34;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:49

    

     Th48: for n be Ordinal, d,b be bag of n st d divides b holds d <=' b

    proof

      let n be Ordinal, d,b be bag of n;

      assume that

       A1: d divides b and

       A2: not d < b;

      now

        defpred P[ set] means (d . $1) < (b . $1);

        let p be object;

        assume p in n;

        then

        reconsider p9 = p as Ordinal;

        assume

         A3: (d . p) <> (b . p);

        (d . p9) <= (b . p9) by A1;

        then (d . p9) < (b . p9) by A3, XXREAL_0: 1;

        then

         A4: ex p be Ordinal st P[p];

        consider k be Ordinal such that

         A5: P[k] and

         A6: for m be Ordinal st P[m] holds k c= m from ORDINAL1:sch 1( A4);

        now

          let l be Ordinal;

          assume l in k;

          then

           A7: (b . l) <= (d . l) by A6, ORDINAL1: 5;

          (d . l) <= (b . l) by A1;

          hence (d . l) = (b . l) by A7, XXREAL_0: 1;

        end;

        hence contradiction by A2, A5;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:50

    

     Th49: for n be set, b,b1,b2 be bag of n st b = (b1 + b2) holds b1 divides b

    proof

      let n be set, b,b1,b2 be bag of n;

      assume

       A1: b = (b1 + b2);

      now

        let k be object;

        assume k in n;

        (b . k) = ((b1 . k) + (b2 . k)) by A1, Def5;

        hence (b1 . k) <= (b . k) by NAT_1: 11;

      end;

      hence thesis by Th45;

    end;

    definition

      let X be set;

      :: PRE_POLY:def12

      func Bags X -> set means

      : Def12: for x be set holds x in it iff x is bag of X;

      existence

      proof

        defpred P[ object] means $1 is bag of X;

        consider A be set such that

         A1: for x be object holds x in A iff x in ( Funcs (X, NAT )) & P[x] from XBOOLE_0:sch 1;

        take A;

        let x be set;

        thus x in A implies x is bag of X by A1;

        assume

         A2: x is bag of X;

        then

        reconsider b = x as bag of X;

        ( dom b) = X & ( rng b) c= NAT by PARTFUN1:def 2, VALUED_0:def 6;

        then x in ( Funcs (X, NAT )) by FUNCT_2:def 2;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let A,B be set such that

         A3: for x be set holds x in A iff x is bag of X and

         A4: for x be set holds x in B iff x is bag of X;

        now

          let x be object;

          x in A iff x is bag of X by A3;

          hence x in A iff x in B by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let X be set;

      :: original: Bags

      redefine

      func Bags X -> Subset of ( Bags X) ;

      coherence

      proof

        ( Bags X) c= ( Bags X);

        hence thesis;

      end;

    end

    theorem :: PRE_POLY:51

    ( Bags {} ) = { {} }

    proof

      now

        let x be set;

        hereby

          assume x in { {} };

          then x = {} by TARSKI:def 1;

          hence x is bag of {} by PARTFUN1:def 2, RELAT_1: 38, RELAT_1:def 18;

        end;

        assume x is bag of {} ;

        then

        reconsider x9 = x as ManySortedSet of {} ;

        x9 = {} ;

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

      end;

      hence thesis by Def12;

    end;

    registration

      let X be set;

      cluster ( Bags X) -> non empty;

      coherence

      proof

        (X --> 0 ) is bag of X by Th39;

        hence thesis by Def12;

      end;

    end

    registration

      let X be set;

      cluster -> functional for Subset of ( Bags X);

      coherence by Def12;

    end

    registration

      let X be set, B be Subset of ( Bags X);

      cluster -> X -defined for Element of B;

      coherence

      proof

        let E be Element of B;

        per cases ;

          suppose B is non empty;

          then

          reconsider B as non empty Subset of ( Bags X);

          reconsider E as Element of B;

          E is bag of X by Def12;

          hence thesis;

        end;

          suppose B is empty;

          then E is empty by SUBSET_1:def 1;

          hence thesis by RELAT_1: 171;

        end;

      end;

    end

    registration

      let X be set, B be non empty Subset of ( Bags X);

      cluster -> total natural-valued finite-support for Element of B;

      coherence by Def12;

    end

    notation

      let X be set;

      synonym EmptyBag X for EmptyMS X;

    end

    definition

      let X be set;

      :: original: EmptyBag

      redefine

      func EmptyBag X -> Element of ( Bags X) ;

      coherence

      proof

        (X --> 0 ) is bag of X by Th39;

        hence thesis by Def12;

      end;

      ::$Canceled

    end

    ::$Canceled

    theorem :: PRE_POLY:53

    for X be set, b be bag of X holds (b + ( EmptyBag X)) = b

    proof

      let X be set, b be bag of X;

      now

        let x be object;

        assume x in X;

        

        thus ((b + ( EmptyBag X)) . x) = ((b . x) + (( EmptyBag X) . x) qua Nat) by Def5

        .= (b . x);

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:54

    

     Th52: for X be set, b be bag of X holds (b -' ( EmptyBag X)) = b

    proof

      let X be set, b be bag of X;

      now

        let x be object;

        assume x in X;

        

        thus ((b -' ( EmptyBag X)) . x) = ((b . x) -' (( EmptyBag X) . x)) by Def6

        .= (b . x) by NAT_D: 40;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:55

    for X be set, b be bag of X holds (( EmptyBag X) -' b) = ( EmptyBag X)

    proof

      let X be set, b be bag of X;

      now

        let x be object;

        assume x in X;

        

        thus ((( EmptyBag X) -' b) . x) = ((( EmptyBag X) . x) -' (b . x)) by Def6

        .= (( EmptyBag X) . x) by NAT_2: 8;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:56

    

     Th54: for X be set, b be bag of X holds (b -' b) = ( EmptyBag X)

    proof

      let X be set, b be bag of X;

      now

        let x be object;

        assume x in X;

        

        thus ((b -' b) . x) = ((b . x) -' (b . x)) by Def6

        .= 0 by XREAL_1: 232

        .= (( EmptyBag X) . x);

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:57

    

     Th55: for n be set, b1,b2 be bag of n st b1 divides b2 & (b2 -' b1) = ( EmptyBag n) holds b2 = b1

    proof

      let n be set, b1,b2 be bag of n such that

       A1: b1 divides b2 and

       A2: (b2 -' b1) = ( EmptyBag n);

      now

        let k be object;

        assume k in n;

         0 = ((b2 -' b1) . k) by A2

        .= ((b2 . k) -' (b1 . k)) by Def6;

        then

         A3: (b2 . k) <= (b1 . k) by NAT_D: 36;

        (b1 . k) <= (b2 . k) by A1;

        hence (b2 . k) = (b1 . k) by A3, XXREAL_0: 1;

      end;

      hence thesis;

    end;

    theorem :: PRE_POLY:58

    for n be set, b be bag of n st b divides ( EmptyBag n) holds ( EmptyBag n) = b;

    theorem :: PRE_POLY:59

    

     Th57: for n be set, b be bag of n holds ( EmptyBag n) divides b;

    theorem :: PRE_POLY:60

    for n be Ordinal, b be bag of n holds ( EmptyBag n) <=' b by Th48, Th57;

    definition

      let n be Ordinal;

      :: PRE_POLY:def14

      func BagOrder n -> Order of ( Bags n) means

      : Def13: for p,q be bag of n holds [p, q] in it iff p <=' q;

      existence

      proof

        defpred P[ object, object] means ex b1,b2 be Element of ( Bags n) st $1 = b1 & $2 = b2 & b1 <=' b2;

        consider BO be Relation of ( Bags n), ( Bags n) such that

         A1: for x,y be object holds [x, y] in BO iff x in ( Bags n) & y in ( Bags n) & P[x, y] from RELSET_1:sch 1;

        

         A2: BO is_antisymmetric_in ( Bags n)

        proof

          let x,y be object;

          assume that x in ( Bags n) and y in ( Bags n) and

           A3: [x, y] in BO and

           A4: [y, x] in BO;

          

           A5: ex b19,b29 be Element of ( Bags n) st y = b19 & x = b29 & b19 <=' b29 by A1, A4;

          consider b1,b2 be Element of ( Bags n) such that

           A6: x = b1 & y = b2 and

           A7: b1 <=' b2 by A1, A3;

          b1 < b2 or b1 = b2 by A7;

          hence thesis by A6, A5;

        end;

        

         A8: BO is_reflexive_in ( Bags n) by A1;

        then

         A9: ( dom BO) = ( Bags n) & ( field BO) = ( Bags n) by ORDERS_1: 13;

        BO is_transitive_in ( Bags n)

        proof

          let x,y,z be object such that x in ( Bags n) and y in ( Bags n) and z in ( Bags n) and

           A10: [x, y] in BO and

           A11: [y, z] in BO;

          consider b1,b2 be Element of ( Bags n) such that

           A12: x = b1 and

           A13: y = b2 & b1 <=' b2 by A1, A10;

          consider b19,b29 be Element of ( Bags n) such that

           A14: y = b19 and

           A15: z = b29 and

           A16: b19 <=' b29 by A1, A11;

          reconsider B1 = b1, B29 = b29 as bag of n;

          B1 <=' B29 by A13, A14, A16, Th41;

          hence thesis by A1, A12, A15;

        end;

        then

        reconsider BO as Order of ( Bags n) by A8, A2, A9, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

        take BO;

        let p,q be bag of n;

        hereby

          assume [p, q] in BO;

          then ex b1,b2 be Element of ( Bags n) st p = b1 & q = b2 & b1 <=' b2 by A1;

          hence p <=' q;

        end;

        p in ( Bags n) & q in ( Bags n) by Def12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let B1,B2 be Order of ( Bags n) such that

         A17: for p,q be bag of n holds [p, q] in B1 iff p <=' q and

         A18: for p,q be bag of n holds [p, q] in B2 iff p <=' q;

        let a,b be object;

        hereby

          assume

           A19: [a, b] in B1;

          then

          consider b1,b2 be object such that

           A20: [a, b] = [b1, b2] and

           A21: b1 in ( Bags n) & b2 in ( Bags n) by RELSET_1: 2;

          reconsider b1, b2 as bag of n by A21;

          b1 <=' b2 by A17, A19, A20;

          hence [a, b] in B2 by A18, A20;

        end;

        assume

         A22: [a, b] in B2;

        then

        consider b1,b2 be object such that

         A23: [a, b] = [b1, b2] and

         A24: b1 in ( Bags n) & b2 in ( Bags n) by RELSET_1: 2;

        reconsider b1, b2 as bag of n by A24;

        b1 <=' b2 by A18, A22, A23;

        hence thesis by A17, A23;

      end;

    end

    

     Lm1: for n be Ordinal holds ( BagOrder n) is_reflexive_in ( Bags n) by Def13;

    

     Lm2: for n be Ordinal holds ( BagOrder n) is_antisymmetric_in ( Bags n)

    proof

      let n be Ordinal;

      set BO = ( BagOrder n);

      let x,y be object;

      assume that

       A1: x in ( Bags n) & y in ( Bags n) and

       A2: [x, y] in BO and

       A3: [y, x] in BO;

      reconsider b1 = x, b2 = y as bag of n by A1;

      b1 <=' b2 by A2, Def13;

      then

       A4: b1 < b2 or b1 = b2;

      reconsider b19 = y, b29 = x as bag of n by A1;

      b19 <=' b29 by A3, Def13;

      hence thesis by A4;

    end;

    

     Lm3: for n be Ordinal holds ( BagOrder n) is_transitive_in ( Bags n)

    proof

      let n be Ordinal;

      set BO = ( BagOrder n);

      let x,y,z be object such that

       A1: x in ( Bags n) and

       A2: y in ( Bags n) and

       A3: z in ( Bags n) and

       A4: [x, y] in BO & [y, z] in BO;

      reconsider b19 = y, b29 = z as bag of n by A2, A3;

      reconsider b1 = x, b2 = y as bag of n by A1, A2;

      reconsider B1 = b1, B29 = b29 as bag of n;

      b1 <=' b2 & b19 <=' b29 by A4, Def13;

      then B1 <=' B29 by Th41;

      hence thesis by Def13;

    end;

    

     Lm4: for n be Ordinal holds ( BagOrder n) linearly_orders ( Bags n)

    proof

      let n be Ordinal;

      set BO = ( BagOrder n);

      

       A1: BO is_transitive_in ( Bags n) by Lm3;

      

       A2: BO is_connected_in ( Bags n)

      proof

        let x,y be object;

        assume that

         A3: x in ( Bags n) & y in ( Bags n) and x <> y and

         A4: not [x, y] in BO;

        reconsider p = x, q = y as bag of n by A3;

         not p <=' q by A4, Def13;

        then q <=' p by Th44;

        hence thesis by Def13;

      end;

      BO is_reflexive_in ( Bags n) & BO is_antisymmetric_in ( Bags n) by Lm1, Lm2;

      hence thesis by A1, A2, ORDERS_1:def 9;

    end;

    registration

      let n be Ordinal;

      cluster ( BagOrder n) -> being_linear-order;

      coherence

      proof

        set BO = ( BagOrder n);

        BO linearly_orders ( Bags n) by Lm4;

        then ( field BO) = ( Bags n) & BO is_connected_in ( Bags n) by ORDERS_1: 15, ORDERS_1:def 9;

        then BO is connected;

        hence thesis by ORDERS_1:def 6;

      end;

    end

    definition

      let X be set, f be Function of X, NAT ;

      :: PRE_POLY:def15

      func NatMinor f -> Subset of ( Funcs (X, NAT )) means

      : Def14: for g be natural-valued ManySortedSet of X holds g in it iff for x be set st x in X holds (g . x) <= (f . x);

      existence

      proof

        defpred P[ set] means ex g be natural-valued ManySortedSet of X st $1 = g & for x be set st x in X holds (g . x) <= (f . x);

        consider IT be Subset of ( Funcs (X, NAT )) such that

         A1: for h be set holds h in IT iff h in ( Funcs (X, NAT )) & P[h] from SUBSET_1:sch 1;

        take IT;

        let g be natural-valued ManySortedSet of X;

        hereby

          assume g in IT;

          then ex g1 be natural-valued ManySortedSet of X st g1 = g & for x be set st x in X holds (g1 . x) <= (f . x) by A1;

          hence for x be set st x in X holds (g . x) <= (f . x);

        end;

        ( dom g) = X & ( rng g) c= NAT by PARTFUN1:def 2, VALUED_0:def 6;

        then g is Function of X, NAT by RELSET_1: 4;

        then

         A2: g in ( Funcs (X, NAT )) by FUNCT_2: 8;

        assume for x be set st x in X holds (g . x) <= (f . x);

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of ( Funcs (X, NAT )) such that

         A3: for g be natural-valued ManySortedSet of X holds g in it1 iff for x be set st x in X holds (g . x) <= (f . x) and

         A4: for g be natural-valued ManySortedSet of X holds g in it2 iff for x be set st x in X holds (g . x) <= (f . x);

        now

          let h be Element of ( Funcs (X, NAT ));

          hereby

            assume h in it1;

            then for x be set st x in X holds (h . x) <= (f . x) by A3;

            hence h in it2 by A4;

          end;

          assume h in it2;

          then for x be set st x in X holds (h . x) <= (f . x) by A4;

          hence h in it1 by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    theorem :: PRE_POLY:61

    

     Th59: for X be set, f be Function of X, NAT holds f in ( NatMinor f)

    proof

      let X be set, f be Function of X, NAT ;

      for x be set st x in X holds (f . x) <= (f . x);

      hence thesis by Def14;

    end;

    registration

      let X be set, f be Function of X, NAT ;

      cluster ( NatMinor f) -> non empty functional;

      coherence by Th59;

    end

    registration

      let X be set, f be Function of X, NAT ;

      cluster -> natural-valued for Element of ( NatMinor f);

      coherence by FUNCT_2: 92;

    end

    theorem :: PRE_POLY:62

    

     Th60: for X be set, f be finite-support Function of X, NAT holds ( NatMinor f) c= ( Bags X)

    proof

      let X be set, f be finite-support Function of X, NAT ;

      let x be object;

      assume x in ( NatMinor f);

      then

      reconsider x9 = x as Element of ( NatMinor f);

      

       A1: ( dom x9) = X by FUNCT_2: 92;

      then

       A2: x9 is ManySortedSet of X by PARTFUN1:def 2, RELAT_1:def 18;

      ( support x9) c= ( support f)

      proof

        let a be object;

        

         A3: ( support x9) c= ( dom x9) by Th36;

        assume

         A4: a in ( support x9);

        then (x9 . a) <> 0 by Def7;

        then (f . a) <> 0 by A1, A2, A4, A3, Def14;

        hence thesis by Def7;

      end;

      then x is bag of X by A1, Def8, PARTFUN1:def 2, RELAT_1:def 18;

      hence thesis by Def12;

    end;

    definition

      let X be set, f be finite-support Function of X, NAT ;

      :: original: support

      redefine

      func support f -> Element of ( Fin X) ;

      coherence

      proof

        ( dom f) = X by FUNCT_2:def 1;

        then ( support f) c= X by Th36;

        hence thesis by FINSUB_1:def 5;

      end;

    end

    theorem :: PRE_POLY:63

    

     Th61: for X be non empty set, f be finite-support Function of X, NAT holds ( card ( NatMinor f)) = ( multnat $$ (( support f),( addnat [:] (f,1))))

    proof

      let X be non empty set;

      defpred P[ Element of ( Fin X)] means for f be Function of X, NAT st for x be Element of X st not x in $1 holds (f . x) = 0 holds ( card ( NatMinor f)) = ( multnat $$ ($1,( addnat [:] (f,1))));

      let f be finite-support Function of X, NAT ;

      

       A1: for x be Element of X holds not x in ( support f) implies (f . x) = 0 by Def7;

      

       A2: for B be Element of ( Fin X), b be Element of X holds P[B] & not b in B implies P[(B \/ {.b.})]

      proof

        let B be Element of ( Fin X), b be Element of X such that

         A3: P[B] and

         A4: not b in B;

        let f be Function of X, NAT such that

         A5: for x be Element of X st not x in (B \/ {b}) holds (f . x) = 0 ;

        reconsider g = (f +* (b, 0 )) as Function of X, NAT ;

        (g | B) = (f | B) by A4, FUNCT_7: 92;

        then (( addnat [:] (g,1)) | B) = (( addnat [:] (f,1)) | B) by FUNCOP_1: 28;

        then

         A6: ( multnat $$ (B,( addnat [:] (g,1)))) = ( multnat $$ (B,( addnat [:] (f,1)))) by SETWOP_2: 7;

        

         A7: ( dom f) = X by FUNCT_2:def 1;

        for x be Element of X st not x in B holds (g . x) = 0

        proof

          let x be Element of X such that

           A8: not x in B;

          per cases ;

            suppose x = b;

            hence thesis by A7, FUNCT_7: 31;

          end;

            suppose

             A9: x <> b;

             A10:

            now

              assume x in (B \/ {b});

              then x in B or x in {b} by XBOOLE_0:def 3;

              hence contradiction by A8, A9, TARSKI:def 1;

            end;

            

            thus (g . x) = (f . x) by A9, FUNCT_7: 32

            .= 0 by A5, A10;

          end;

        end;

        then

         A11: ( card ( NatMinor g)) = ( multnat $$ (B,( addnat [:] (g,1)))) by A3;

        then

        reconsider ng = ( NatMinor g) as functional finite non empty set;

        reconsider fb1 = ((f . b) + 1) as non zero Nat;

        ( dom ( addnat [:] (f,1))) = X by FUNCT_2:def 1;

        

        then

         A12: (( addnat [:] (f,1)) . b) = ( addnat . ((f . b),1)) by FUNCOP_1: 27

        .= ((f . b) + 1) by BINOP_2:def 23;

        set cng = ( card ng);

        

         A13: (f . b) < ((f . b) + 1) by XREAL_1: 29;

        ( [:ng, ((f . b) + 1):],( NatMinor f)) are_equipotent

        proof

          deffunc F( Element of ng, Element of fb1) = ($1 +* (b,$2));

          

           A14: for p be Element of ng, l be Element of fb1 holds F(p,l) in ( NatMinor f)

          proof

            let p be Element of ng, l be Element of fb1;

            reconsider q = p as Element of ( NatMinor g);

            fb1 c= NAT & l in fb1;

            then

            reconsider k = l as Element of NAT ;

            p in ( NatMinor g);

            then

             A15: ( dom p) = X by FUNCT_2: 92;

            then ( dom (p +* (b,l))) = X by FUNCT_7: 30;

            then

            reconsider pbl = (q +* (b,k)) as natural-valued ManySortedSet of X by PARTFUN1:def 2, RELAT_1:def 18;

            for x be set st x in X holds (pbl . x) <= (f . x)

            proof

              let x be set;

              assume

               A16: x in X;

              per cases ;

                suppose

                 A17: x = b;

                k in ( Segm fb1);

                then

                 A18: k < fb1 by NAT_1: 44;

                (pbl . x) = k by A15, A17, FUNCT_7: 31;

                hence thesis by A17, A18, NAT_1: 13;

              end;

                suppose

                 A19: x <> b;

                q is ManySortedSet of X by A15, PARTFUN1:def 2, RELAT_1:def 18;

                then

                 A20: (q . x) <= (g . x) by A16, Def14;

                (pbl . x) = (q . x) by A19, FUNCT_7: 32;

                hence thesis by A19, A20, FUNCT_7: 32;

              end;

            end;

            hence thesis by Def14;

          end;

          consider r be Function of [:ng, fb1:], ( NatMinor f) such that

           A21: for p be Element of ng, l be Element of fb1 holds (r . (p,l)) = F(p,l) from FUNCT_7:sch 1( A14);

          take r;

          thus r is one-to-one

          proof

            let x1,x2 be object;

            assume that

             A22: x1 in ( dom r) and

             A23: x2 in ( dom r) and

             A24: (r . x1) = (r . x2);

            consider p2,l2 be object such that

             A25: x2 = [p2, l2] by A23, RELAT_1:def 1;

            reconsider p2 as Element of ( NatMinor g) by A23, A25, ZFMISC_1: 87;

            

             A26: ( dom p2) = X by FUNCT_2: 92;

            

             A27: l2 in fb1 by A23, A25, ZFMISC_1: 87;

            consider p1,l1 be object such that

             A28: x1 = [p1, l1] by A22, RELAT_1:def 1;

            reconsider p1 as Element of ( NatMinor g) by A22, A28, ZFMISC_1: 87;

            

             A29: ( dom p1) = X by FUNCT_2: 92;

            then

            reconsider p19 = p1, p29 = p2 as natural-valued ManySortedSet of X by A26, PARTFUN1:def 2, RELAT_1:def 18;

            l1 in fb1 by A22, A28, ZFMISC_1: 87;

            

            then

             A30: (p1 +* (b,l1)) = (r . (p1,l1)) by A21

            .= (r . (p2,l2)) by A24, A28, A25

            .= (p2 +* (b,l2)) by A21, A27;

             A31:

            now

              let x be object;

              assume x in X;

              per cases ;

                suppose

                 A32: x = b;

                

                 A33: (g . b) = 0 by A7, FUNCT_7: 31;

                

                hence (p19 . x) = 0 by A32, Def14

                .= (p29 . x) by A32, A33, Def14;

              end;

                suppose

                 A34: x <> b;

                

                hence (p19 . x) = ((p1 +* (b,l1)) . x) by FUNCT_7: 32

                .= (p29 . x) by A30, A34, FUNCT_7: 32;

              end;

            end;

            l1 = ((p1 +* (b,l1)) . b) by A29, FUNCT_7: 31

            .= l2 by A30, A26, FUNCT_7: 31;

            hence thesis by A28, A25, A31, PBOOLE: 3;

          end;

          thus

           A35: ( dom r) = [:ng, ((f . b) + 1):] by FUNCT_2:def 1;

          thus ( rng r) c= ( NatMinor f);

          thus ( NatMinor f) c= ( rng r)

          proof

            let x be object;

            assume x in ( NatMinor f);

            then

            reconsider e = x as Element of ( NatMinor f);

            

             A36: ( dom e) = X by FUNCT_2: 92;

            then ( dom (e +* (b, 0 ))) = X by FUNCT_7: 30;

            then

            reconsider eb0 = (e +* (b, 0 )) as natural-valued ManySortedSet of X by PARTFUN1:def 2, RELAT_1:def 18;

            

             A37: e is ManySortedSet of X by A36, PARTFUN1:def 2, RELAT_1:def 18;

            now

              let x be set;

              assume

               A38: x in X;

              per cases ;

                suppose x = b;

                hence (eb0 . x) <= (g . x) by A36, FUNCT_7: 31;

              end;

                suppose

                 A39: x <> b;

                then

                 A40: (eb0 . x) = (e . x) by FUNCT_7: 32;

                (e . x) <= (f . x) by A37, A38, Def14;

                hence (eb0 . x) <= (g . x) by A39, A40, FUNCT_7: 32;

              end;

            end;

            then

            reconsider eb0 as Element of ( NatMinor g) by Def14;

            (e . b) <= (f . b) by A37, Def14;

            then (e . b) < fb1 by A13, XXREAL_0: 2;

            then

             A41: (e . b) in ( Segm fb1) by NAT_1: 44;

            then

             A42: [eb0, (e . b)] in ( dom r) by A35, ZFMISC_1: 87;

            e = (e +* (b,(e . b))) by FUNCT_7: 35

            .= (eb0 +* (b,(e . b))) by FUNCT_7: 34;

            then e = (r . (eb0,(e . b))) by A21, A41;

            hence thesis by A42, FUNCT_1:def 3;

          end;

        end;

        

        hence ( card ( NatMinor f)) = ( card [:ng, ((f . b) + 1):]) by CARD_1: 5

        .= (cng * ( card ((f . b) + 1))) by CARD_2: 46

        .= (cng * ((f . b) + 1))

        .= ( multnat . (( multnat $$ (B,( addnat [:] (f,1)))),((f . b) + 1))) by A11, A6, BINOP_2:def 24

        .= ( multnat $$ ((B \/ {.b.}),( addnat [:] (f,1)))) by A4, A12, SETWOP_2: 2;

      end;

      

       A43: P[( {}. X)]

      proof

        let f be Function of X, NAT such that

         A44: for x be Element of X st not x in ( {}. X) holds (f . x) = 0 ;

        now

          let x be object;

          hereby

            assume

             A45: x in ( NatMinor f);

            then

            reconsider x9 = x as Function of X, NAT by FUNCT_2: 66;

            now

              let c be Element of X;

              (f . c) = 0 by A44;

              hence (x9 . c) = (f . c) by A45, Def14;

            end;

            hence x = f by FUNCT_2: 63;

          end;

          thus x = f implies x in ( NatMinor f) by Th59;

        end;

        then ( NatMinor f) = {f} by TARSKI:def 1;

        

        hence ( card ( NatMinor f)) = 1 by CARD_1: 30

        .= ( multnat $$ (( {}. X),( addnat [:] (f,1)))) by BINOP_2: 10, SETWISEO: 31;

      end;

      for B be Element of ( Fin X) holds P[B] from SETWISEO:sch 2( A43, A2);

      hence thesis by A1;

    end;

    registration

      let X be set, f be finite-support Function of X, NAT ;

      cluster ( NatMinor f) -> finite;

      coherence

      proof

        per cases ;

          suppose X is empty;

          then ( NatMinor f) c= ( Funcs ( {} , NAT ));

          then ( NatMinor f) c= { {} } by FUNCT_5: 57;

          hence thesis;

        end;

          suppose not X is empty;

          then

          reconsider X as non empty set;

          reconsider f as finite-support Function of X, NAT ;

          ( card ( NatMinor f)) = ( multnat $$ (( support f),( addnat [:] (f,1)))) by Th61;

          hence thesis;

        end;

      end;

    end

    definition

      let n be Ordinal, b be bag of n;

      :: PRE_POLY:def16

      func divisors b -> FinSequence of ( Bags n) means

      : Def15: ex S be non empty finite Subset of ( Bags n) st it = ( SgmX (( BagOrder n),S)) & for p be bag of n holds p in S iff p divides b;

      existence

      proof

        ( dom b) = n & ( rng b) c= NAT by PARTFUN1:def 2, VALUED_0:def 6;

        then

        reconsider f = b as finite-support Function of n, NAT by RELSET_1: 4;

        reconsider S = ( NatMinor f) as non empty finite Subset of ( Bags n) by Th60;

        take IT = ( SgmX (( BagOrder n),S));

        take S;

        thus IT = ( SgmX (( BagOrder n),S));

        let p be bag of n;

        thus p in S implies p divides b

        proof

          assume p in S;

          then for x be object st x in n holds (p . x) <= (b . x) by Def14;

          hence thesis by Th45;

        end;

        assume p divides b;

        then for x be set st x in n holds (p . x) <= (b . x);

        hence thesis by Def14;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of ( Bags n);

        given S1 be non empty finite Subset of ( Bags n) such that

         A1: it1 = ( SgmX (( BagOrder n),S1)) and

         A2: for p be bag of n holds p in S1 iff p divides b;

        given S2 be non empty finite Subset of ( Bags n) such that

         A3: it2 = ( SgmX (( BagOrder n),S2)) and

         A4: for p be bag of n holds p in S2 iff p divides b;

        for x be object holds x in S1 iff x in S2 by A2, A4;

        hence thesis by A1, A3, TARSKI: 2;

      end;

    end

    registration

      let n be Ordinal, b be bag of n;

      cluster ( divisors b) -> non empty one-to-one;

      coherence

      proof

        ex S be non empty finite Subset of ( Bags n) st ( divisors b) = ( SgmX (( BagOrder n),S)) & for p be bag of n holds p in S iff p divides b by Def15;

        hence thesis;

      end;

    end

    theorem :: PRE_POLY:64

    

     Th62: for n be Ordinal, i be Element of NAT , b be bag of n st i in ( dom ( divisors b)) holds (( divisors b) /. i) qua Element of ( Bags n) divides b

    proof

      let n be Ordinal, i be Element of NAT , b be bag of n;

      assume i in ( dom ( divisors b));

      then

       A1: (( divisors b) /. i) = (( divisors b) . i) & (( divisors b) . i) in ( rng ( divisors b)) by FUNCT_1:def 3, PARTFUN1:def 6;

      reconsider pid = (( divisors b) /. i) as bag of n;

      consider S be non empty finite Subset of ( Bags n) such that

       A2: ( divisors b) = ( SgmX (( BagOrder n),S)) and

       A3: for p be bag of n holds p in S iff p divides b by Def15;

      ( BagOrder n) linearly_orders S by Lm4, ORDERS_1: 38;

      then pid in S by A2, A1, Def2;

      hence thesis by A3;

    end;

    theorem :: PRE_POLY:65

    

     Th63: for n be Ordinal, b be bag of n holds (( divisors b) /. 1) = ( EmptyBag n) & (( divisors b) /. ( len ( divisors b))) = b

    proof

      let n be Ordinal, b be bag of n;

      consider S be non empty finite Subset of ( Bags n) such that

       A1: ( divisors b) = ( SgmX (( BagOrder n),S)) and

       A2: for p be bag of n holds p in S iff p divides b by Def15;

       A3:

      now

        let y be Element of ( Bags n);

        assume y in S;

        then y divides b by A2;

        then y <=' b by Th48;

        hence [y, b] in ( BagOrder n) by Def13;

      end;

       A4:

      now

        let y be Element of ( Bags n);

        assume y in S;

        ( EmptyBag n) <=' y by Th48, Th57;

        hence [( EmptyBag n), y] in ( BagOrder n) by Def13;

      end;

      

       A5: ( BagOrder n) linearly_orders S by Lm4, ORDERS_1: 38;

      ( EmptyBag n) divides b;

      then ( EmptyBag n) in S by A2;

      hence (( divisors b) /. 1) = ( EmptyBag n) by A1, A5, A4, Th19;

      b in S by A2;

      hence thesis by A1, A5, A3, Th20;

    end;

    theorem :: PRE_POLY:66

    

     Th64: for n be Ordinal, i be Nat, b,b1,b2 be bag of n st i > 1 & i < ( len ( divisors b)) holds (( divisors b) /. i) <> ( EmptyBag n) & (( divisors b) /. i) <> b

    proof

      let n be Ordinal, i be Nat, b,b1,b2 be bag of n;

      

       A1: 1 in ( dom ( divisors b)) & ( len ( divisors b)) in ( dom ( divisors b)) by FINSEQ_5: 6;

      

       A2: (( divisors b) /. 1) = ( EmptyBag n) & (( divisors b) /. ( len ( divisors b))) = b by Th63;

      assume

       A3: i > 1 & i < ( len ( divisors b));

      then i in ( dom ( divisors b)) by FINSEQ_3: 25;

      hence thesis by A2, A1, A3, PARTFUN2: 10;

    end;

    theorem :: PRE_POLY:67

    

     Th65: for n be Ordinal holds ( divisors ( EmptyBag n)) = <*( EmptyBag n)*>

    proof

      let n be Ordinal;

      consider S be non empty finite Subset of ( Bags n) such that

       A1: ( divisors ( EmptyBag n)) = ( SgmX (( BagOrder n),S)) and

       A2: for p be bag of n holds p in S iff p divides ( EmptyBag n) by Def15;

      

       A3: S c= {( EmptyBag n)}

      proof

        let x be object;

        assume

         A4: x in S;

        then

        reconsider b = x as bag of n;

        b divides ( EmptyBag n) by A2, A4;

        then b = ( EmptyBag n);

        hence thesis by TARSKI:def 1;

      end;

      

       A5: ( BagOrder n) linearly_orders S by Lm4, ORDERS_1: 38;

      ( EmptyBag n) in S by A2;

      then {( EmptyBag n)} c= S by ZFMISC_1: 31;

      then S = {( EmptyBag n)} by A3;

      then

       A6: ( rng ( divisors ( EmptyBag n))) = {( EmptyBag n)} by A1, A5, Def2;

      ( len ( divisors ( EmptyBag n))) = ( card ( rng ( divisors ( EmptyBag n)))) by Th18

      .= 1 by A6, CARD_1: 30;

      hence thesis by A6, FINSEQ_1: 39;

    end;

    definition

      let n be Ordinal, b be bag of n;

      :: PRE_POLY:def17

      func decomp b -> FinSequence of (2 -tuples_on ( Bags n)) means

      : Def16: ( dom it ) = ( dom ( divisors b)) & for i be Element of NAT , p be bag of n st i in ( dom it ) & p = (( divisors b) /. i) holds (it /. i) = <*p, (b -' p)*>;

      existence

      proof

        defpred P[ Nat, set] means for p be bag of n st p = (( divisors b) /. $1) holds $2 = <*p, (b -' p)*>;

        

         A1: for k be Nat st k in ( Seg ( len ( divisors b))) holds ex d be Element of (2 -tuples_on ( Bags n)) st P[k, d]

        proof

          let k be Nat such that k in ( Seg ( len ( divisors b)));

          reconsider p = (( divisors b) /. k) as bag of n;

          reconsider b1 = p, b2 = (b -' p) as Element of ( Bags n) by Def12;

          ( len <*p, (b -' p)*>) = 2 by FINSEQ_1: 44;

          then

          reconsider d = <*b1, b2*> as Element of (2 -tuples_on ( Bags n)) by FINSEQ_2: 92;

          take d;

          thus thesis;

        end;

        consider f be FinSequence of (2 -tuples_on ( Bags n)) such that

         A2: ( len f) = ( len ( divisors b)) and

         A3: for n be Nat st n in ( Seg ( len ( divisors b))) holds P[n, (f /. n)] from FINSEQ_4:sch 1( A1);

        take f;

        thus ( dom f) = ( dom ( divisors b)) by A2, FINSEQ_3: 29;

        let i be Element of NAT , p be bag of n such that

         A4: i in ( dom f) and

         A5: p = (( divisors b) /. i);

        i in ( Seg ( len ( divisors b))) by A2, A4, FINSEQ_1:def 3;

        hence thesis by A3, A5;

      end;

      uniqueness

      proof

        let F,G be FinSequence of (2 -tuples_on ( Bags n)) such that

         A6: ( dom F) = ( dom ( divisors b)) and

         A7: for i be Element of NAT , p be bag of n st i in ( dom F) & p = (( divisors b) /. i) holds (F /. i) = <*p, (b -' p)*> and

         A8: ( dom G) = ( dom ( divisors b)) and

         A9: for i be Element of NAT , p be bag of n st i in ( dom G) & p = (( divisors b) /. i) holds (G /. i) = <*p, (b -' p)*>;

        now

          let i be Nat;

          reconsider p = (( divisors b) /. i) as bag of n;

          assume

           A10: i in ( dom F);

          

          hence (F /. i) = <*p, (b -' p)*> by A7

          .= (G /. i) by A6, A8, A9, A10;

        end;

        hence thesis by A6, A8, FINSEQ_5: 12;

      end;

    end

    theorem :: PRE_POLY:68

    

     Th66: for n be Ordinal, i be Element of NAT , b be bag of n st i in ( dom ( decomp b)) holds ex b1,b2 be bag of n st (( decomp b) /. i) = <*b1, b2*> & b = (b1 + b2)

    proof

      let n be Ordinal, i be Element of NAT , b be bag of n;

      reconsider p = (( divisors b) /. i) as bag of n;

      assume

       A1: i in ( dom ( decomp b));

      take p, (b -' p);

      thus (( decomp b) /. i) = <*p, (b -' p)*> by A1, Def16;

      i in ( dom ( divisors b)) by A1, Def16;

      hence thesis by Th46, Th62;

    end;

    theorem :: PRE_POLY:69

    

     Th67: for n be Ordinal, b,b1,b2 be bag of n st b = (b1 + b2) holds ex i be Element of NAT st i in ( dom ( decomp b)) & (( decomp b) /. i) = <*b1, b2*>

    proof

      let n be Ordinal, b,b1,b2 be bag of n;

      consider S be non empty finite Subset of ( Bags n) such that

       A1: ( divisors b) = ( SgmX (( BagOrder n),S)) and

       A2: for p be bag of n holds p in S iff p divides b by Def15;

      

       A3: ( BagOrder n) linearly_orders S by Lm4, ORDERS_1: 38;

      assume

       A4: b = (b1 + b2);

      then b1 divides b by Th49;

      then b1 in S by A2;

      then b1 in ( rng ( divisors b)) by A1, A3, Def2;

      then

      consider i be Element of NAT such that

       A5: i in ( dom ( divisors b)) and

       A6: (( divisors b) /. i) = b1 by PARTFUN2: 2;

      take i;

      thus i in ( dom ( decomp b)) by A5, Def16;

      then (( decomp b) /. i) = <*b1, (b -' b1)*> by A6, Def16;

      hence thesis by A4, Th47;

    end;

    theorem :: PRE_POLY:70

    

     Th68: for n be Ordinal, i be Element of NAT , b,b1,b2 be bag of n st i in ( dom ( decomp b)) & (( decomp b) /. i) = <*b1, b2*> holds b1 = (( divisors b) /. i)

    proof

      let n be Ordinal, i be Element of NAT , b,b1,b2 be bag of n;

      reconsider p = (( divisors b) /. i) as bag of n;

      assume i in ( dom ( decomp b)) & (( decomp b) /. i) = <*b1, b2*>;

      then <*b1, b2*> = <*p, (b -' p)*> by Def16;

      hence thesis by FINSEQ_1: 77;

    end;

    registration

      let n be Ordinal, b be bag of n;

      cluster ( decomp b) -> non empty one-to-one FinSequence-yielding;

      coherence

      proof

        

         A1: ( dom ( divisors b)) = ( dom ( decomp b)) by Def16;

        hence ( decomp b) is non empty;

        now

          let k,m be Element of NAT ;

          assume

           A2: k in ( dom ( decomp b));

          assume

           A3: m in ( dom ( decomp b));

          then

          consider bm1,bm2 be bag of n such that

           A4: (( decomp b) /. m) = <*bm1, bm2*> and b = (bm1 + bm2) by Th66;

          assume (( decomp b) /. k) = (( decomp b) /. m);

          

          then (( divisors b) /. k) = bm1 by A2, A4, Th68

          .= (( divisors b) /. m) by A3, A4, Th68;

          hence k = m by A1, A2, A3, PARTFUN2: 10;

        end;

        hence ( decomp b) is one-to-one by PARTFUN2: 9;

        let x be object;

        assume x in ( dom ( decomp b));

        thus thesis;

      end;

    end

    registration

      let n be Ordinal, b be Element of ( Bags n);

      cluster ( decomp b) -> non empty one-to-one FinSequence-yielding;

      coherence ;

    end

    theorem :: PRE_POLY:71

    for n be Ordinal, b be bag of n holds (( decomp b) /. 1) = <*( EmptyBag n), b*> & (( decomp b) /. ( len ( decomp b))) = <*b, ( EmptyBag n)*>

    proof

      let n be Ordinal, b be bag of n;

      reconsider p = (( divisors b) /. 1) as bag of n;

      p = ( EmptyBag n) & 1 in ( dom ( decomp b)) by Th63, FINSEQ_5: 6;

      

      hence (( decomp b) /. 1) = <*( EmptyBag n), (b -' ( EmptyBag n))*> by Def16

      .= <*( EmptyBag n), b*> by Th52;

      reconsider p = (( divisors b) /. ( len ( decomp b))) as bag of n;

      ( dom ( decomp b)) = ( dom ( divisors b)) by Def16;

      then ( len ( decomp b)) = ( len ( divisors b)) by FINSEQ_3: 29;

      then

       A1: p = b by Th63;

      ( len ( decomp b)) in ( dom ( decomp b)) by FINSEQ_5: 6;

      

      hence (( decomp b) /. ( len ( decomp b))) = <*b, (b -' b)*> by A1, Def16

      .= <*b, ( EmptyBag n)*> by Th54;

    end;

    theorem :: PRE_POLY:72

    for n be Ordinal, i be Nat, b,b1,b2 be bag of n st i > 1 & i < ( len ( decomp b)) & (( decomp b) /. i) = <*b1, b2*> holds b1 <> ( EmptyBag n) & b2 <> ( EmptyBag n)

    proof

      let n be Ordinal, i be Nat, b,b1,b2 be bag of n such that

       A1: i > 1 & i < ( len ( decomp b)) and

       A2: (( decomp b) /. i) = <*b1, b2*>;

      reconsider p = (( divisors b) /. i) as bag of n;

      

       A3: i in ( dom ( decomp b)) by A1, FINSEQ_3: 25;

      then

       A4: (( decomp b) /. i) = <*p, (b -' p)*> by Def16;

      then

       A5: b2 = (b -' p) by A2, FINSEQ_1: 77;

      

       A6: ( dom ( decomp b)) = ( dom ( divisors b)) by Def16;

      then

       A7: ( len ( decomp b)) = ( len ( divisors b)) by FINSEQ_3: 29;

      b1 = p by A2, A4, FINSEQ_1: 77;

      hence b1 <> ( EmptyBag n) by A1, A7, Th64;

      assume b2 = ( EmptyBag n);

      then p = b by A6, A3, A5, Th55, Th62;

      hence contradiction by A1, A7, Th64;

    end;

    theorem :: PRE_POLY:73

    for n be Ordinal holds ( decomp ( EmptyBag n)) = <* <*( EmptyBag n), ( EmptyBag n)*>*>

    proof

      let n be Ordinal;

      ( len <*( EmptyBag n), ( EmptyBag n)*>) = 2 by FINSEQ_1: 44;

      then

      reconsider E = <*( EmptyBag n), ( EmptyBag n)*> as Element of (2 -tuples_on ( Bags n)) by FINSEQ_2: 92;

      reconsider e = <*E*> as FinSequence of (2 -tuples_on ( Bags n));

      

       A1: ( dom e) = ( Seg 1) by FINSEQ_1: 38;

      

       A2: <*( EmptyBag n)*> = ( divisors ( EmptyBag n)) by Th65;

      

       A3: for i be Element of NAT , p be bag of n st i in ( dom e) & p = (( divisors ( EmptyBag n)) /. i) holds (e /. i) = <*p, (( EmptyBag n) -' p)*>

      proof

        let i be Element of NAT , p be bag of n such that

         A4: i in ( dom e) and

         A5: p = (( divisors ( EmptyBag n)) /. i);

        

         A6: i = 1 by A1, A4, FINSEQ_1: 2, TARSKI:def 1;

        then

         A7: (( divisors ( EmptyBag n)) /. i) = ( EmptyBag n) by A2, FINSEQ_4: 16;

        

        thus (e /. i) = E by A6, FINSEQ_4: 16

        .= <*p, (( EmptyBag n) -' p)*> by A5, A7, Th52;

      end;

      ( dom e) = ( dom ( divisors ( EmptyBag n))) by A2, A1, FINSEQ_1: 38;

      hence thesis by A3, Def16;

    end;

    theorem :: PRE_POLY:74

    for n be Ordinal, b be bag of n, f,g be FinSequence of ((3 -tuples_on ( Bags n)) * ) st ( dom f) = ( dom ( decomp b)) & ( dom g) = ( dom ( decomp b)) & (for k be Nat st k in ( dom f) holds (f . k) = (( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 1) qua Element of ( Bags n)) ^^ (( len ( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 1) qua Element of ( Bags n))) |-> <*((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 2)*>))) & (for k be Nat st k in ( dom g) holds (g . k) = ((( len ( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 2) qua Element of ( Bags n))) |-> <*((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 1)*>) ^^ ( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 2) qua Element of ( Bags n)))) holds ex p be Permutation of ( dom ( FlattenSeq f)) st ( FlattenSeq g) = (( FlattenSeq f) * p)

    proof

      let n be Ordinal, b be bag of n, f,g be FinSequence of ((3 -tuples_on ( Bags n)) * ) such that

       A1: ( dom f) = ( dom ( decomp b)) and

       A2: ( dom g) = ( dom ( decomp b)) and

       A3: for k be Nat st k in ( dom f) holds (f . k) = (( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 1) qua Element of ( Bags n)) ^^ (( len ( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 1) qua Element of ( Bags n))) |-> <*((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 2)*>)) and

       A4: for k be Nat st k in ( dom g) holds (g . k) = ((( len ( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 2) qua Element of ( Bags n))) |-> <*((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 1)*>) ^^ ( decomp ((( decomp b) /. k) qua Element of (2 -tuples_on ( Bags n)) /. 2) qua Element of ( Bags n)));

      set Ff = ( FlattenSeq f), Fg = ( FlattenSeq g), db = ( decomp b);

      

       A5: Fg is one-to-one

      proof

        let k1,k2 be object such that

         A6: k1 in ( dom Fg) and

         A7: k2 in ( dom Fg) and

         A8: (Fg . k1) = (Fg . k2);

        consider i1,j1 be Nat such that

         A9: i1 in ( dom g) and

         A10: j1 in ( dom (g . i1)) and

         A11: k1 = (( Sum ( Card (g | (i1 -' 1)))) + j1) and

         A12: ((g . i1) . j1) = (Fg . k1) by A6, Th28;

        reconsider dbi1 = (db /. i1) as Element of (2 -tuples_on ( Bags n));

        set ddbi11 = ( decomp (dbi1 /. 2) qua Element of ( Bags n));

        

         A13: (g . i1) = ((( len ddbi11) |-> <*(dbi1 /. 1)*>) ^^ ddbi11) by A4, A9;

        

        then

         A14: ( dom (g . i1)) = (( dom ddbi11) /\ ( dom (( len ddbi11) |-> <*(dbi1 /. 1)*>))) by Def4

        .= (( dom ddbi11) /\ ( Seg ( len ddbi11)))

        .= (( dom ddbi11) /\ ( dom ddbi11)) by FINSEQ_1:def 3

        .= ( dom ddbi11);

        then

         A15: (ddbi11 /. j1) = (ddbi11 . j1) by A10, PARTFUN1:def 6;

        ( dom ddbi11) = ( Seg ( len ddbi11)) by FINSEQ_1:def 3;

        then

         A16: ((( len ddbi11) |-> <*(dbi1 /. 1)*>) . j1) = <*(dbi1 /. 1)*> by A10, A14, FUNCOP_1: 7;

        consider b11,b12 be bag of n such that

         A17: (db /. i1) = <*b11, b12*> and b = (b11 + b12) by A2, A9, Th66;

        reconsider b119 = b11, b129 = b12 as Element of ( Bags n) by Def12;

        

         A18: b119 = b11 & b129 = b12;

        then (dbi1 /. 2) = b12 by A17, FINSEQ_4: 17;

        then

        consider b111,b112 be bag of n such that

         A19: (ddbi11 /. j1) = <*b111, b112*> and

         A20: b12 = (b111 + b112) by A10, A14, Th66;

        (dbi1 /. 1) = b11 by A17, A18, FINSEQ_4: 17;

        

        then

         A21: ((g . i1) . j1) = ( <*b11*> ^ <*b111, b112*>) by A10, A13, A19, A15, A16, Def4

        .= <*b11, b111, b112*> by FINSEQ_1: 43;

        consider i2,j2 be Nat such that

         A22: i2 in ( dom g) and

         A23: j2 in ( dom (g . i2)) and

         A24: k2 = (( Sum ( Card (g | (i2 -' 1)))) + j2) and

         A25: ((g . i2) . j2) = (Fg . k2) by A7, Th28;

        reconsider dbi2 = (db /. i2) as Element of (2 -tuples_on ( Bags n));

        set ddbi21 = ( decomp (dbi2 /. 2) qua Element of ( Bags n));

        

         A26: (g . i2) = ((( len ddbi21) |-> <*(dbi2 /. 1)*>) ^^ ddbi21) by A4, A22;

        

        then

         A27: ( dom (g . i2)) = (( dom ddbi21) /\ ( dom (( len ddbi21) |-> <*(dbi2 /. 1)*>))) by Def4

        .= (( dom ddbi21) /\ ( Seg ( len ddbi21)))

        .= (( dom ddbi21) /\ ( dom ddbi21)) by FINSEQ_1:def 3

        .= ( dom ddbi21);

        then

         A28: (ddbi21 /. j2) = (ddbi21 . j2) by A23, PARTFUN1:def 6;

        ( dom ddbi21) = ( Seg ( len ddbi21)) by FINSEQ_1:def 3;

        then

         A29: ((( len ddbi21) |-> <*(dbi2 /. 1)*>) . j2) = <*(dbi2 /. 1)*> by A23, A27, FUNCOP_1: 7;

        consider b21,b22 be bag of n such that

         A30: (db /. i2) = <*b21, b22*> and b = (b21 + b22) by A2, A22, Th66;

        reconsider b219 = b21, b229 = b22 as Element of ( Bags n) by Def12;

        

         A31: b219 = b21 & b229 = b22;

        then (dbi2 /. 2) = b22 by A30, FINSEQ_4: 17;

        then

        consider b211,b212 be bag of n such that

         A32: (ddbi21 /. j2) = <*b211, b212*> and

         A33: b22 = (b211 + b212) by A23, A27, Th66;

        (dbi2 /. 1) = b21 by A30, A31, FINSEQ_4: 17;

        

        then

         A34: ((g . i2) . j2) = ( <*b21*> ^ <*b211, b212*>) by A23, A26, A32, A28, A29, Def4

        .= <*b21, b211, b212*> by FINSEQ_1: 43;

        then

         A35: b111 = b211 & b112 = b212 by A8, A12, A25, A21, FINSEQ_1: 78;

        

         A36: (db /. i2) = (db . i2) by A2, A22, PARTFUN1:def 6;

        

         A37: (db /. i1) = (db . i1) by A2, A9, PARTFUN1:def 6;

        b11 = b21 by A8, A12, A25, A21, A34, FINSEQ_1: 78;

        then i1 = i2 by A2, A9, A22, A37, A17, A20, A36, A30, A33, A35, FUNCT_1:def 4;

        hence thesis by A10, A11, A23, A24, A19, A15, A27, A32, A28, A35, FUNCT_1:def 4;

      end;

      now

        let y be object;

        hereby

          assume y in ( rng Ff);

          then

          consider k be object such that

           A38: k in ( dom Ff) and

           A39: y = (Ff . k) by FUNCT_1:def 3;

          reconsider k as Element of NAT by A38;

          consider i,j be Nat such that

           A40: i in ( dom f) and

           A41: j in ( dom (f . i)) and k = (( Sum ( Card (f | (i -' 1)))) + j) and

           A42: ((f . i) . j) = (Ff . k) by A38, Th28;

          reconsider dbi = (db /. i) as Element of (2 -tuples_on ( Bags n));

          set ddbi1 = ( decomp (dbi /. 1) qua Element of ( Bags n));

          

           A43: (f . i) = (ddbi1 ^^ (( len ddbi1) |-> <*(dbi /. 2)*>)) by A3, A40;

          

          then

           A44: ( dom (f . i)) = (( dom ddbi1) /\ ( dom (( len ddbi1) |-> <*(dbi /. 2)*>))) by Def4

          .= (( dom ddbi1) /\ ( Seg ( len ddbi1)))

          .= (( dom ddbi1) /\ ( dom ddbi1)) by FINSEQ_1:def 3

          .= ( dom ddbi1);

          ( dom ddbi1) = ( Seg ( len ddbi1)) by FINSEQ_1:def 3;

          then

           A45: ((( len ddbi1) |-> <*(dbi /. 2)*>) . j) = <*(dbi /. 2)*> by A41, A44, FUNCOP_1: 7;

          consider b1,b2 be bag of n such that

           A46: (db /. i) = <*b1, b2*> and

           A47: b = (b1 + b2) by A1, A40, Th66;

          reconsider b19 = b1, b29 = b2 as Element of ( Bags n) by Def12;

          

           A48: b19 = b1 & b29 = b2;

          then

           A49: (dbi /. 2) = b2 by A46, FINSEQ_4: 17;

          (dbi /. 1) = b1 by A46, A48, FINSEQ_4: 17;

          then

          consider b11,b12 be bag of n such that

           A50: (ddbi1 /. j) = <*b11, b12*> and

           A51: b1 = (b11 + b12) by A41, A44, Th66;

          b = (b11 + (b12 + b2)) by A47, A51, Th34;

          then

          consider i9 be Element of NAT such that

           A52: i9 in ( dom ( decomp b)) and

           A53: (( decomp b) /. i9) = <*b11, (b12 + b2)*> by Th67;

          set b3 = (b12 + b2);

          reconsider b119 = b11, b39 = b3 as Element of ( Bags n) by Def12;

          consider j9 be Element of NAT such that

           A54: j9 in ( dom ( decomp b3)) and

           A55: (( decomp b3) /. j9) = <*b12, b2*> by Th67;

          reconsider dbi9 = (( decomp b) /. i9) as Element of (2 -tuples_on ( Bags n));

          set ddbi92 = ( decomp (dbi9 /. 2) qua Element of ( Bags n));

          

           A56: (( decomp b) /. i9) = <*b119, b39*> by A53;

          then

           A57: (dbi9 /. 1) = b11 & ddbi92 = ( decomp b3) by FINSEQ_4: 17;

          

           A58: (g . i9) = ((( len ddbi92) |-> <*(dbi9 /. 1)*>) ^^ ddbi92) by A2, A4, A52;

          

          then

           A59: ( dom (g . i9)) = (( dom (( len ddbi92) |-> <*(dbi9 /. 1)*>)) /\ ( dom ddbi92)) by Def4

          .= (( Seg ( len ddbi92)) /\ ( dom ddbi92))

          .= (( dom ddbi92) /\ ( dom ddbi92)) by FINSEQ_1:def 3

          .= ( dom ddbi92);

          then

           A60: j9 in ( dom (g . i9)) by A54, A56, FINSEQ_4: 17;

          then

           A61: j9 in ( Seg ( len ddbi92)) by A59, FINSEQ_1:def 3;

          

           A62: (( decomp b3) /. j9) = (( decomp b3) . j9) by A54, PARTFUN1:def 6;

          set m = (( Sum ( Card (g | (i9 -' 1)))) + j9);

          

           A63: m in ( dom Fg) & (Fg . m) = ((g . i9) . j9) by A2, A52, A60, Th29;

          

           A64: ((g . i9) . j9) = (((( len ddbi92) |-> <*(dbi9 /. 1)*>) . j9) ^ (ddbi92 . j9)) by A58, A60, Def4

          .= ( <*b11*> ^ <*b12, b2*>) by A55, A57, A61, A62, FUNCOP_1: 7

          .= <*b11, b12, b2*> by FINSEQ_1: 43;

          (ddbi1 /. j) = (ddbi1 . j) by A41, A44, PARTFUN1:def 6;

          

          then ((f . i) . j) = ( <*b11, b12*> ^ <*b2*>) by A41, A43, A49, A50, A45, Def4

          .= <*b11, b12, b2*> by FINSEQ_1: 43;

          hence y in ( rng Fg) by A39, A42, A64, A63, FUNCT_1:def 3;

        end;

        assume y in ( rng Fg);

        then

        consider k be object such that

         A65: k in ( dom Fg) and

         A66: y = (Fg . k) by FUNCT_1:def 3;

        reconsider k as Element of NAT by A65;

        consider i,j be Nat such that

         A67: i in ( dom g) and

         A68: j in ( dom (g . i)) and k = (( Sum ( Card (g | (i -' 1)))) + j) and

         A69: ((g . i) . j) = (Fg . k) by A65, Th28;

        reconsider dbi = (db /. i) as Element of (2 -tuples_on ( Bags n));

        set ddbi1 = ( decomp (dbi /. 2) qua Element of ( Bags n));

        

         A70: (g . i) = ((( len ddbi1) |-> <*(dbi /. 1)*>) ^^ ddbi1) by A4, A67;

        

        then

         A71: ( dom (g . i)) = (( dom ddbi1) /\ ( dom (( len ddbi1) |-> <*(dbi /. 1)*>))) by Def4

        .= (( dom ddbi1) /\ ( Seg ( len ddbi1)))

        .= (( dom ddbi1) /\ ( dom ddbi1)) by FINSEQ_1:def 3

        .= ( dom ddbi1);

        ( dom ddbi1) = ( Seg ( len ddbi1)) by FINSEQ_1:def 3;

        then

         A72: ((( len ddbi1) |-> <*(dbi /. 1)*>) . j) = <*(dbi /. 1)*> by A68, A71, FUNCOP_1: 7;

        consider b1,b2 be bag of n such that

         A73: (db /. i) = <*b1, b2*> and

         A74: b = (b1 + b2) by A2, A67, Th66;

        reconsider b19 = b1, b29 = b2 as Element of ( Bags n) by Def12;

        

         A75: b19 = b1 & b29 = b2;

        then

         A76: (dbi /. 1) = b1 by A73, FINSEQ_4: 17;

        (dbi /. 2) = b2 by A73, A75, FINSEQ_4: 17;

        then

        consider b11,b12 be bag of n such that

         A77: (ddbi1 /. j) = <*b11, b12*> and

         A78: b2 = (b11 + b12) by A68, A71, Th66;

        (ddbi1 /. j) = (ddbi1 . j) by A68, A71, PARTFUN1:def 6;

        

        then

         A79: ((g . i) . j) = ( <*b1*> ^ <*b11, b12*>) by A68, A70, A76, A77, A72, Def4

        .= <*b1, b11, b12*> by FINSEQ_1: 43;

        set b3 = (b1 + b11);

        reconsider b39 = b3, b129 = b12 as Element of ( Bags n) by Def12;

        consider j9 be Element of NAT such that

         A80: j9 in ( dom ( decomp b3)) and

         A81: (( decomp b3) /. j9) = <*b1, b11*> by Th67;

        

         A82: (( decomp b3) /. j9) = (( decomp b3) . j9) by A80, PARTFUN1:def 6;

        b = ((b1 + b11) + b12) by A74, A78, Th34;

        then

        consider i9 be Element of NAT such that

         A83: i9 in ( dom ( decomp b)) and

         A84: (( decomp b) /. i9) = <*(b1 + b11), b12*> by Th67;

        reconsider dbi9 = (( decomp b) /. i9) as Element of (2 -tuples_on ( Bags n));

        set ddbi92 = ( decomp (dbi9 /. 1) qua Element of ( Bags n));

        set m = (( Sum ( Card (f | (i9 -' 1)))) + j9);

        

         A85: (( decomp b) /. i9) = <*b39, b129*> by A84;

        then

         A86: (dbi9 /. 1) = b3 by FINSEQ_4: 17;

        then

         A87: j9 in ( Seg ( len ddbi92)) by A80, FINSEQ_1:def 3;

        

         A88: (f . i9) = (ddbi92 ^^ (( len ddbi92) |-> <*(dbi9 /. 2)*>)) by A1, A3, A83;

        

        then

         A89: ( dom (f . i9)) = (( dom (( len ddbi92) |-> <*(dbi9 /. 2)*>)) /\ ( dom ddbi92)) by Def4

        .= (( Seg ( len ddbi92)) /\ ( dom ddbi92))

        .= (( dom ddbi92) /\ ( dom ddbi92)) by FINSEQ_1:def 3

        .= ( dom ddbi92);

        then

         A90: m in ( dom Ff) & (Ff . m) = ((f . i9) . j9) by A1, A83, A80, A86, Th29;

        

         A91: (dbi9 /. 2) = b12 by A85, FINSEQ_4: 17;

        ((f . i9) . j9) = ((ddbi92 . j9) ^ ((( len ddbi92) |-> <*(dbi9 /. 2)*>) . j9)) by A80, A88, A86, A89, Def4

        .= ( <*b1, b11*> ^ <*b12*>) by A81, A91, A86, A87, A82, FUNCOP_1: 7

        .= <*b1, b11, b12*> by FINSEQ_1: 43;

        hence y in ( rng Ff) by A66, A69, A79, A90, FUNCT_1:def 3;

      end;

      then

       A92: ( rng Ff) = ( rng Fg) by TARSKI: 2;

      Ff is one-to-one

      proof

        let k1,k2 be object such that

         A93: k1 in ( dom Ff) and

         A94: k2 in ( dom Ff) and

         A95: (Ff . k1) = (Ff . k2);

        consider i1,j1 be Nat such that

         A96: i1 in ( dom f) and

         A97: j1 in ( dom (f . i1)) and

         A98: k1 = (( Sum ( Card (f | (i1 -' 1)))) + j1) and

         A99: ((f . i1) . j1) = (Ff . k1) by A93, Th28;

        reconsider dbi1 = (db /. i1) as Element of (2 -tuples_on ( Bags n));

        set ddbi11 = ( decomp (dbi1 /. 1) qua Element of ( Bags n));

        

         A100: (f . i1) = (ddbi11 ^^ (( len ddbi11) |-> <*(dbi1 /. 2)*>)) by A3, A96;

        

        then

         A101: ( dom (f . i1)) = (( dom ddbi11) /\ ( dom (( len ddbi11) |-> <*(dbi1 /. 2)*>))) by Def4

        .= (( dom ddbi11) /\ ( Seg ( len ddbi11)))

        .= (( dom ddbi11) /\ ( dom ddbi11)) by FINSEQ_1:def 3

        .= ( dom ddbi11);

        then

         A102: (ddbi11 /. j1) = (ddbi11 . j1) by A97, PARTFUN1:def 6;

        ( dom ddbi11) = ( Seg ( len ddbi11)) by FINSEQ_1:def 3;

        then

         A103: ((( len ddbi11) |-> <*(dbi1 /. 2)*>) . j1) = <*(dbi1 /. 2)*> by A97, A101, FUNCOP_1: 7;

        consider b11,b12 be bag of n such that

         A104: (db /. i1) = <*b11, b12*> and b = (b11 + b12) by A1, A96, Th66;

        reconsider b119 = b11, b129 = b12 as Element of ( Bags n) by Def12;

        

         A105: b119 = b11 & b129 = b12;

        then (dbi1 /. 1) = b11 by A104, FINSEQ_4: 17;

        then

        consider b111,b112 be bag of n such that

         A106: (ddbi11 /. j1) = <*b111, b112*> and

         A107: b11 = (b111 + b112) by A97, A101, Th66;

        (dbi1 /. 2) = b12 by A104, A105, FINSEQ_4: 17;

        

        then

         A108: ((f . i1) . j1) = ( <*b111, b112*> ^ <*b12*>) by A97, A100, A106, A102, A103, Def4

        .= <*b111, b112, b12*> by FINSEQ_1: 43;

        consider i2,j2 be Nat such that

         A109: i2 in ( dom f) and

         A110: j2 in ( dom (f . i2)) and

         A111: k2 = (( Sum ( Card (f | (i2 -' 1)))) + j2) and

         A112: ((f . i2) . j2) = (Ff . k2) by A94, Th28;

        reconsider dbi2 = (db /. i2) as Element of (2 -tuples_on ( Bags n));

        set ddbi21 = ( decomp (dbi2 /. 1) qua Element of ( Bags n));

        

         A113: (f . i2) = (ddbi21 ^^ (( len ddbi21) |-> <*(dbi2 /. 2)*>)) by A3, A109;

        

        then

         A114: ( dom (f . i2)) = (( dom ddbi21) /\ ( dom (( len ddbi21) |-> <*(dbi2 /. 2)*>))) by Def4

        .= (( dom ddbi21) /\ ( Seg ( len ddbi21)))

        .= (( dom ddbi21) /\ ( dom ddbi21)) by FINSEQ_1:def 3

        .= ( dom ddbi21);

        then

         A115: (ddbi21 /. j2) = (ddbi21 . j2) by A110, PARTFUN1:def 6;

        ( dom ddbi21) = ( Seg ( len ddbi21)) by FINSEQ_1:def 3;

        then

         A116: ((( len ddbi21) |-> <*(dbi2 /. 2)*>) . j2) = <*(dbi2 /. 2)*> by A110, A114, FUNCOP_1: 7;

        consider b21,b22 be bag of n such that

         A117: (db /. i2) = <*b21, b22*> and b = (b21 + b22) by A1, A109, Th66;

        reconsider b219 = b21, b229 = b22 as Element of ( Bags n) by Def12;

        

         A118: b219 = b21 & b229 = b22;

        then (dbi2 /. 1) = b21 by A117, FINSEQ_4: 17;

        then

        consider b211,b212 be bag of n such that

         A119: (ddbi21 /. j2) = <*b211, b212*> and

         A120: b21 = (b211 + b212) by A110, A114, Th66;

        (dbi2 /. 2) = b22 by A117, A118, FINSEQ_4: 17;

        

        then

         A121: ((f . i2) . j2) = ( <*b211, b212*> ^ <*b22*>) by A110, A113, A119, A115, A116, Def4

        .= <*b211, b212, b22*> by FINSEQ_1: 43;

        then

         A122: b111 = b211 & b112 = b212 by A95, A99, A112, A108, FINSEQ_1: 78;

        

         A123: (db /. i2) = (db . i2) by A1, A109, PARTFUN1:def 6;

        

         A124: (db /. i1) = (db . i1) by A1, A96, PARTFUN1:def 6;

        b12 = b22 by A95, A99, A112, A108, A121, FINSEQ_1: 78;

        then i1 = i2 by A1, A96, A109, A124, A104, A107, A123, A117, A120, A122, FUNCT_1:def 4;

        hence thesis by A97, A98, A110, A111, A106, A102, A114, A119, A115, A122, FUNCT_1:def 4;

      end;

      then (Ff,Fg) are_fiberwise_equipotent by A92, A5, RFINSEQ: 26;

      hence thesis by RFINSEQ: 4;

    end;

    theorem :: PRE_POLY:75

    for X be set, b1,b2 be real-valued ManySortedSet of X holds ( support (b1 + b2)) c= (( support b1) \/ ( support b2))

    proof

      let X be set, b1,b2 be real-valued ManySortedSet of X;

      let x be object;

      assume x in ( support (b1 + b2));

      then

       A1: ((b1 + b2) . x) <> 0 by Def7;

      assume

       A2: not x in (( support b1) \/ ( support b2));

      then not x in ( support b1) by XBOOLE_0:def 3;

      then

       A3: (b1 . x) = 0 by Def7;

       not x in ( support b2) by A2, XBOOLE_0:def 3;

      then ((b1 . x) + (b2 . x)) = 0 by A3, Def7;

      hence contradiction by A1, Def5;

    end;

    registration

      let D be non empty set;

      let n be Nat;

      cluster -> FinSequence-yielding for FinSequence of (n -tuples_on D);

      coherence ;

    end

    registration

      let k be Nat;

      let D be non empty set, M be FinSequence of (k -tuples_on D);

      let x be set;

      cluster (M /. x) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let k be Element of NAT ;

      let D be non empty set, M be FinSequence of (k -tuples_on D);

      let x be set;

      cluster (M /. x) -> D -valued FinSequence-like;

      coherence ;

    end

    begin

    theorem :: PRE_POLY:76

    for X be set, A be empty Subset of X, R be Order of X st R linearly_orders A holds ( SgmX (R,A)) = {}

    proof

      let X be set, A be empty Subset of X, R be Order of X;

      assume R linearly_orders A;

      then ( rng ( SgmX (R,A))) = {} by Def2;

      hence thesis;

    end;

    theorem :: PRE_POLY:77

    

     Th75: for X be set, A be finite Subset of X, R be Order of X st R linearly_orders A holds for i,j be Element of NAT st i in ( dom ( SgmX (R,A))) & j in ( dom ( SgmX (R,A))) holds (( SgmX (R,A)) /. i) = (( SgmX (R,A)) /. j) implies i = j

    proof

      let X be set, A be finite Subset of X, R be Order of X;

      assume

       A1: R linearly_orders A;

      let i,j be Element of NAT such that

       A2: i in ( dom ( SgmX (R,A))) and

       A3: j in ( dom ( SgmX (R,A))) and

       A4: (( SgmX (R,A)) /. i) = (( SgmX (R,A)) /. j);

      assume i <> j;

      then i < j or j < i by XXREAL_0: 1;

      hence thesis by A1, A2, A3, A4, Def2;

    end;

    

     Lm5: for D be set, p be FinSequence of D st ( dom p) <> {} holds 1 in ( dom p)

    proof

      let D be set, p be FinSequence of D;

      assume ( dom p) <> {} ;

      then p <> {} ;

      hence thesis by FINSEQ_5: 6;

    end;

    

     Lm6: for X be set, A be finite Subset of X, a be Element of X, R be Order of X st R linearly_orders ( {a} \/ A) holds R linearly_orders A

    proof

      let X be set, A be finite Subset of X, a be Element of X, R be Order of X;

      for x be object holds x in A implies x in ( {a} \/ A) by XBOOLE_0:def 3;

      then

       A1: A c= ( {a} \/ A);

      assume R linearly_orders ( {a} \/ A);

      hence thesis by A1, ORDERS_1: 38;

    end;

    theorem :: PRE_POLY:78

    

     Th76: for X be set, A be finite Subset of X, a be Element of X st not a in A holds for B be finite Subset of X st B = ( {a} \/ A) holds for R be Order of X st R linearly_orders B holds for k be Element of NAT st k in ( dom ( SgmX (R,B))) & (( SgmX (R,B)) /. k) = a holds for i be Element of NAT st 1 <= i & i <= (k - 1) holds (( SgmX (R,B)) /. i) = (( SgmX (R,A)) /. i)

    proof

      let X be set, A be finite Subset of X, a be Element of X;

      assume

       A1: not a in A;

      let B be finite Subset of X;

      assume

       A2: B = ( {a} \/ A);

      let R be Order of X;

      assume

       A3: R linearly_orders B;

      then

       A4: R linearly_orders A by A2, Lm6;

      ( field R) = X by ORDERS_1: 12;

      then

       A5: R is_antisymmetric_in X by RELAT_2:def 12;

      set sgb = ( SgmX (R,B)), sga = ( SgmX (R,A));

      consider lensga be Nat such that

       A6: ( dom sga) = ( Seg lensga) by FINSEQ_1:def 2;

      consider lensgb be Nat such that

       A7: ( dom sgb) = ( Seg lensgb) by FINSEQ_1:def 2;

      reconsider lensga, lensgb as Element of NAT by ORDINAL1:def 12;

      lensgb = ( len sgb) by A7, FINSEQ_1:def 3

      .= ( card B) by A3, Th10

      .= (( card A) + 1) by A1, A2, CARD_2: 41

      .= (( len sga) + 1) by A2, A3, Lm6, Th10

      .= (lensga + 1) by A6, FINSEQ_1:def 3;

      then

       A8: lensga <= lensgb by NAT_1: 11;

      defpred P[ Nat] means (sgb /. $1) = (sga /. $1);

      let k be Element of NAT ;

      assume that

       A9: k in ( dom ( SgmX (R,B))) and

       A10: (( SgmX (R,B)) /. k) = a;

      k in ( Seg ( len sgb)) by A9, FINSEQ_1:def 3;

      then

       A11: 1 <= k by FINSEQ_1: 1;

      then (1 - 1) <= (k - 1) by XREAL_1: 9;

      then

      reconsider k9 = (k - 1) as Element of NAT by INT_1: 3;

      

       A12: ((k - 1) + 1) = (k + 0 qua Nat);

      

       A13: for j be Element of NAT st 1 <= j & j < k9 holds (for j9 be Element of NAT st 1 <= j9 & j9 <= j holds P[j9]) implies P[(j + 1)]

      proof

        let i9 be Element of NAT ;

        assume that

         A14: 1 <= i9 and

         A15: i9 < k9;

        

         A16: 1 <= (i9 + 1) by A14, XREAL_1: 29;

        

         A17: (i9 + 1) < k by A12, A15, XREAL_1: 6;

        then

         A18: (i9 + 1) in ( dom sgb) by A9, A16, FINSEQ_3: 156;

        (sgb /. (i9 + 1)) = (sgb . (i9 + 1)) by A9, A17, A16, FINSEQ_3: 156, PARTFUN1:def 6;

        then (sgb /. (i9 + 1)) in ( rng sgb) by A18, FUNCT_1:def 3;

        then

         A19: (sgb /. (i9 + 1)) in B by A3, Def2;

        (sgb /. (i9 + 1)) <> a by A3, A9, A10, A17, A18, Def2;

        then not (sgb /. (i9 + 1)) in {a} by TARSKI:def 1;

        then (sgb /. (i9 + 1)) in A by A2, A19, XBOOLE_0:def 3;

        then (sgb /. (i9 + 1)) in ( rng sga) by A4, Def2;

        then

        consider l be object such that

         A20: l in ( dom sga) and

         A21: (sga . l) = (sgb /. (i9 + 1)) by FUNCT_1:def 3;

        reconsider l as Element of NAT by A20;

        

         A22: 1 <= l by A6, A20, FINSEQ_1: 1;

        l <= lensga by A6, A20, FINSEQ_1: 1;

        then l <= lensgb by A8, XXREAL_0: 2;

        then

         A23: l in ( dom sgb) by A7, A22, FINSEQ_1: 1;

        assume

         A24: for j9 be Element of NAT st 1 <= j9 & j9 <= i9 holds P[j9];

        assume

         A25: (sgb /. (i9 + 1)) <> (sga /. (i9 + 1));

        then

         A26: l <> (i9 + 1) by A20, A21, PARTFUN1:def 6;

        per cases ;

          suppose l < (i9 + 1);

          then l <= i9 by NAT_1: 13;

          

          then (sgb /. l) = (sga /. l) by A24, A22

          .= (sgb /. (i9 + 1)) by A20, A21, PARTFUN1:def 6;

          hence thesis by A3, A18, A26, A23, Th75;

        end;

          suppose

           A27: (i9 + 1) <= l;

          then

           A28: (i9 + 1) in ( dom sga) by A16, A20, FINSEQ_3: 156;

          (sga /. (i9 + 1)) = (sga . (i9 + 1)) by A16, A20, A27, FINSEQ_3: 156, PARTFUN1:def 6;

          then (sga /. (i9 + 1)) in ( rng sga) by A28, FUNCT_1:def 3;

          then (sga /. (i9 + 1)) in A by A4, Def2;

          then (sga /. (i9 + 1)) in B by A2, XBOOLE_0:def 3;

          then (sga /. (i9 + 1)) in ( rng sgb) by A3, Def2;

          then

          consider l9 be object such that

           A29: l9 in ( dom sgb) and

           A30: (sgb . l9) = (sga /. (i9 + 1)) by FUNCT_1:def 3;

          reconsider l9 as Element of NAT by A29;

          (i9 + 1) < l by A26, A27, XXREAL_0: 1;

          then [(sga /. (i9 + 1)), (sga /. l)] in R by A4, A20, A28, Def2;

          then [(sgb /. l9), (sga /. l)] in R by A29, A30, PARTFUN1:def 6;

          then

           A31: [(sgb /. l9), (sgb /. (i9 + 1))] in R by A20, A21, PARTFUN1:def 6;

          (sgb /. l9) = (sgb . l9) by A29, PARTFUN1:def 6;

          then (sgb /. l9) in ( rng sgb) by A29, FUNCT_1:def 3;

          then

           A32: (sgb /. l9) in B by A3, Def2;

          

           A33: 1 <= l9 by A7, A29, FINSEQ_1: 1;

          

           A34: (i9 + 1) < l9

          proof

            assume

             A35: l9 <= (i9 + 1);

            now

              per cases by A35, XXREAL_0: 1;

                case l9 = (i9 + 1);

                hence thesis by A25, A29, A30, PARTFUN1:def 6;

              end;

                case

                 A36: l9 < (i9 + 1);

                then l9 <= i9 by NAT_1: 13;

                

                then

                 A37: (sga /. l9) = (sgb /. l9) by A24, A33

                .= (sga /. (i9 + 1)) by A29, A30, PARTFUN1:def 6;

                l9 in ( dom sga) by A28, A33, A36, FINSEQ_3: 156;

                hence thesis by A2, A3, A28, A36, A37, Lm6, Th75;

              end;

            end;

            hence thesis;

          end;

          then [(sgb /. (i9 + 1)), (sgb /. l9)] in R by A3, A18, A29, Def2;

          then (sgb /. l9) = (sgb /. (i9 + 1)) by A5, A31, A32;

          hence thesis by A3, A18, A29, A34, Th75;

        end;

      end;

      let i be Element of NAT ;

      assume that

       A38: 1 <= i and

       A39: i <= (k - 1);

      

       A40: 1 in ( dom sgb) by A9, Lm5;

      

       A41: P[1]

      proof

        (sgb /. 1) = (sgb . 1) by A9, Lm5, PARTFUN1:def 6;

        then (sgb /. 1) in ( rng sgb) by A40, FUNCT_1:def 3;

        then

         A42: (sgb /. 1) in B by A3, Def2;

        k <> 1 by A38, A39, XXREAL_0: 2;

        then 1 < k by A11, XXREAL_0: 1;

        then (sgb /. 1) <> a by A3, A9, A10, A40, Def2;

        then not (sgb /. 1) in {a} by TARSKI:def 1;

        then (sgb /. 1) in A by A2, A42, XBOOLE_0:def 3;

        then (sgb /. 1) in ( rng sga) by A4, Def2;

        then

        consider l be object such that

         A43: l in ( dom sga) and

         A44: (sga . l) = (sgb /. 1) by FUNCT_1:def 3;

        

         A45: (sga /. 1) = (sga . 1) by A43, Lm5, PARTFUN1:def 6;

        assume

         A46: (sgb /. 1) <> (sga /. 1);

        reconsider l as Element of NAT by A43;

        

         A47: 1 in ( dom sga) by A43, Lm5;

        1 <= l by A6, A43, FINSEQ_1: 1;

        then 1 < l by A46, A44, A45, XXREAL_0: 1;

        then [(sga /. 1), (sga /. l)] in R by A4, A43, A47, Def2;

        then

         A48: [(sga /. 1), (sgb /. 1)] in R by A43, A44, PARTFUN1:def 6;

         not (sga /. 1) in B

        proof

          

           A49: (sgb /. 1) = (sgb . 1) by A9, Lm5, PARTFUN1:def 6;

          assume (sga /. 1) in B;

          then (sga /. 1) in ( rng sgb) by A3, Def2;

          then

          consider l9 be object such that

           A50: l9 in ( dom sgb) and

           A51: (sgb . l9) = (sga /. 1) by FUNCT_1:def 3;

          reconsider l9 as Element of NAT by A50;

          1 <= l9 by A7, A50, FINSEQ_1: 1;

          then 1 < l9 by A46, A51, A49, XXREAL_0: 1;

          then [(sgb /. 1), (sgb /. l9)] in R by A3, A40, A50, Def2;

          then [(sgb /. 1), (sga /. 1)] in R by A50, A51, PARTFUN1:def 6;

          hence thesis by A5, A46, A42, A48;

        end;

        then

         A52: not (sga /. 1) in A by A2, XBOOLE_0:def 3;

        (sga /. 1) in ( rng sga) by A47, A45, FUNCT_1:def 3;

        hence thesis by A4, A52, Def2;

      end;

      for j be Element of NAT st 1 <= j & j <= k9 holds P[j] from INT_1:sch 8( A41, A13);

      hence thesis by A38, A39;

    end;

    theorem :: PRE_POLY:79

    

     Th77: for X be set, A be finite Subset of X, a be Element of X st not a in A holds for B be finite Subset of X st B = ( {a} \/ A) holds for R be Order of X st R linearly_orders B holds for k be Element of NAT st k in ( dom ( SgmX (R,B))) & (( SgmX (R,B)) /. k) = a holds for i be Element of NAT st k <= i & i <= ( len ( SgmX (R,A))) holds (( SgmX (R,B)) /. (i + 1)) = (( SgmX (R,A)) /. i)

    proof

      let X be set, A be finite Subset of X, a be Element of X;

      assume

       A1: not a in A;

      let B be finite Subset of X;

      assume

       A2: B = ( {a} \/ A);

      let R be Order of X;

      assume

       A3: R linearly_orders B;

      then

       A4: R linearly_orders A by A2, Lm6;

      ( field R) = X by ORDERS_1: 12;

      then

       A5: R is_antisymmetric_in X by RELAT_2:def 12;

      set sgb = ( SgmX (R,B)), sga = ( SgmX (R,A));

      consider lensga be Nat such that

       A6: ( dom sga) = ( Seg lensga) by FINSEQ_1:def 2;

      defpred P[ Nat] means (sgb /. ($1 + 1)) = (sga /. $1);

      consider lensgb be Nat such that

       A7: ( dom sgb) = ( Seg lensgb) by FINSEQ_1:def 2;

      let k be Element of NAT ;

      assume that

       A8: k in ( dom ( SgmX (R,B))) and

       A9: (( SgmX (R,B)) /. k) = a;

      k in ( Seg ( len sgb)) by A8, FINSEQ_1:def 3;

      then

       A10: 1 <= k by FINSEQ_1: 1;

      then (1 - 1) <= (k - 1) by XREAL_1: 9;

      then

      reconsider k9 = (k - 1) as Element of NAT by INT_1: 3;

      reconsider lensga, lensgb as Element of NAT by ORDINAL1:def 12;

      

       A11: (k9 + 1) = (k + 0 qua Nat);

      

       A12: lensgb = ( len sgb) by A7, FINSEQ_1:def 3

      .= ( card B) by A3, Th10

      .= (( card A) + 1) by A1, A2, CARD_2: 41

      .= (( len sga) + 1) by A2, A3, Lm6, Th10

      .= (lensga + 1) by A6, FINSEQ_1:def 3;

      

       A13: for j be Element of NAT st k <= j & j < ( len sga) holds (for j9 be Element of NAT st k <= j9 & j9 <= j holds P[j9]) implies P[(j + 1)]

      proof

        let j be Element of NAT ;

        assume that

         A14: k <= j and

         A15: j < ( len sga);

        

         A16: ((j + 1) + 1) = (j + (1 + 1));

        

         A17: 1 <= (j + 2) by NAT_1: 12;

        ( len sgb) = ( card B) by A3, Th10

        .= (( card A) + 1) by A1, A2, CARD_2: 41

        .= (( len sga) + 1) by A2, A3, Lm6, Th10;

        then (j + 1) < ( len sgb) by A15, XREAL_1: 6;

        then (j + 2) <= ( len sgb) by A16, NAT_1: 13;

        then (j + 2) <= lensgb by A7, FINSEQ_1:def 3;

        then

         A18: (j + 2) in ( dom sgb) by A7, A17, FINSEQ_1: 1;

        now

          assume (sgb /. (j + 2)) = a;

          then (j + 2) = k by A3, A8, A9, A18, Th75;

          hence contradiction by A14, NAT_1: 19;

        end;

        then

         A19: not (sgb /. (j + 2)) in {a} by TARSKI:def 1;

        (sgb /. (j + 2)) = (sgb . (j + 2)) by A18, PARTFUN1:def 6;

        then (sgb /. (j + 2)) in ( rng sgb) by A18, FUNCT_1:def 3;

        then (sgb /. (j + 2)) in B by A3, Def2;

        then (sgb /. (j + 2)) in A by A2, A19, XBOOLE_0:def 3;

        then (sgb /. (j + 2)) in ( rng sga) by A4, Def2;

        then

        consider l be object such that

         A20: l in ( dom sga) and

         A21: (sga . l) = (sgb /. (j + 2)) by FUNCT_1:def 3;

        reconsider l as Element of NAT by A20;

        

         A22: (sga /. l) = (sga . l) by A20, PARTFUN1:def 6;

        

         A23: 1 <= l by A6, A20, FINSEQ_1: 1;

        (j + 1) <= ( len sga) by A15, NAT_1: 13;

        then

         A24: (j + 1) <= lensga by A6, FINSEQ_1:def 3;

        1 <= (j + 1) by NAT_1: 12;

        then

         A25: (j + 1) in ( dom sga) by A6, A24, FINSEQ_1: 1;

        then

         A26: (sga /. (j + 1)) = (sga . (j + 1)) by PARTFUN1:def 6;

        assume

         A27: for j9 be Element of NAT st k <= j9 & j9 <= j holds P[j9];

        l <= lensga by A6, A20, FINSEQ_1: 1;

        then

         A28: (l + 1) <= lensgb by A12, XREAL_1: 6;

        1 <= (l + 1) by NAT_1: 12;

        then

         A29: (l + 1) in ( dom sgb) by A7, A28, FINSEQ_1: 1;

        l <= (l + 1) by XREAL_1: 29;

        then

         A30: l in ( dom sgb) by A23, A29, FINSEQ_3: 156;

        assume

         A31: (sgb /. ((j + 1) + 1)) <> (sga /. (j + 1));

        then

         A32: l <> (j + 1) by A20, A21, PARTFUN1:def 6;

        per cases ;

          suppose

           A33: l <= (j + 1);

          then l < (j + 1) by A32, XXREAL_0: 1;

          then

           A34: l <= j by NAT_1: 13;

          now

            per cases ;

              case k <= l;

              then (sgb /. (l + 1)) = (sga /. l) by A27, A34;

              then (j + 2) = (l + 1) by A3, A18, A20, A21, A29, Th75, PARTFUN1:def 6;

              hence thesis by A31, A20, A21, PARTFUN1:def 6;

            end;

              case l < k;

              then l <= k9 by A11, NAT_1: 13;

              then

               A35: (sgb /. l) = (sga /. l) by A1, A2, A3, A8, A9, A23, Th76;

              (j + 1) < ((j + 1) + 1) by XREAL_1: 29;

              hence thesis by A3, A18, A20, A21, A30, A33, A35, Th75, PARTFUN1:def 6;

            end;

          end;

          hence thesis;

        end;

          suppose

           A36: l > (j + 1);

          

           A37: for i9 be Element of NAT st 1 <= i9 & i9 <= (j + 2) holds (sga /. (j + 1)) <> (sgb /. i9)

          proof

            let i9 be Element of NAT ;

            assume that

             A38: 1 <= i9 and

             A39: i9 <= (j + 2);

            assume

             A40: (sga /. (j + 1)) = (sgb /. i9);

            per cases ;

              suppose i9 = (j + 2);

              hence contradiction by A31, A40;

            end;

              suppose

               A41: i9 <> (j + 2);

              then i9 < (j + 2) by A39, XXREAL_0: 1;

              then

               A42: i9 <= (j + 1) by A16, NAT_1: 13;

              then i9 <= lensga by A24, XXREAL_0: 2;

              then

               A43: i9 in ( dom sga) by A6, A38, FINSEQ_1: 1;

              now

                per cases ;

                  case

                   A44: i9 <= k;

                  now

                    per cases ;

                      case i9 = k;

                      then (sga . (j + 1)) = a by A9, A25, A40, PARTFUN1:def 6;

                      then a in ( rng sga) by A25, FUNCT_1:def 3;

                      hence contradiction by A1, A4, Def2;

                    end;

                      case i9 <> k;

                      then i9 < k by A44, XXREAL_0: 1;

                      then i9 <= k9 by A11, NAT_1: 13;

                      then (sgb /. i9) = (sga /. i9) by A1, A2, A3, A8, A9, A38, Th76;

                      then

                       A45: i9 = (j + 1) by A2, A3, A25, A40, A43, Lm6, Th75;

                      i9 <= j by A14, A44, XXREAL_0: 2;

                      hence contradiction by A45, XREAL_1: 29;

                    end;

                  end;

                  hence contradiction;

                end;

                  case

                   A46: k < i9;

                  

                   A47: (i9 - 1) <= ((j + 1) - 1) by A42, XREAL_1: 9;

                  

                   A48: (i9 - 1) <= i9 by XREAL_1: 146;

                  1 <= i9 by A10, A46, XXREAL_0: 2;

                  then (1 - 1) <= (i9 - 1) by XREAL_1: 9;

                  then

                   A49: (i9 - 1) is Element of NAT by INT_1: 3;

                  

                   A50: ((i9 - 1) + 1) = (i9 + 0 qua Nat);

                  then k <= (i9 - 1) by A46, A49, NAT_1: 13;

                  then 1 <= (i9 - 1) by A10, XXREAL_0: 2;

                  then

                   A51: (i9 - 1) in ( dom sga) by A43, A49, A48, FINSEQ_3: 156;

                  k <= (i9 - 1) by A46, A49, A50, NAT_1: 13;

                  then (sga /. (i9 - 1)) = (sga /. (j + 1)) by A27, A40, A49, A50, A47;

                  hence contradiction by A2, A3, A16, A25, A41, A50, A51, Lm6, Th75;

                end;

              end;

              hence thesis;

            end;

          end;

          (sga /. (j + 1)) in ( rng sga) by A25, A26, FUNCT_1:def 3;

          then

           A52: (sga /. (j + 1)) in A by A4, Def2;

          then (sga /. (j + 1)) in B by A2, XBOOLE_0:def 3;

          then (sga /. (j + 1)) in ( rng sgb) by A3, Def2;

          then

          consider l9 be object such that

           A53: l9 in ( dom sgb) and

           A54: (sgb . l9) = (sga /. (j + 1)) by FUNCT_1:def 3;

          reconsider l9 as Element of NAT by A53;

          

           A55: (sgb /. l9) = (sgb . l9) by A53, PARTFUN1:def 6;

          

           A56: 1 <= (j + 1) by NAT_1: 12;

          (j + 1) <= ( len sga) by A15, NAT_1: 13;

          then (j + 1) in ( Seg ( len sga)) by A56, FINSEQ_1: 1;

          then (j + 1) in ( dom sga) by FINSEQ_1:def 3;

          then

           A57: [(sga /. (j + 1)), (sga /. l)] in R by A4, A20, A36, Def2;

          1 <= l9 by A7, A53, FINSEQ_1: 1;

          then l9 > (j + 2) by A37, A54, A55;

          then [(sga /. l), (sga /. (j + 1))] in R by A3, A18, A21, A22, A53, A54, A55, Def2;

          then (sga /. l) = (sga /. (j + 1)) by A5, A57, A52;

          hence thesis by A2, A3, A25, A20, A36, Lm6, Th75;

        end;

      end;

      let i be Element of NAT ;

      assume that

       A58: k <= i and

       A59: i <= ( len ( SgmX (R,A)));

      k <= ( len sga) by A58, A59, XXREAL_0: 2;

      then

       A60: k <= lensga by A6, FINSEQ_1:def 3;

      then

       A61: k in ( dom sga) by A10, A6, FINSEQ_1: 1;

      

       A62: lensga <= lensgb by A12, NAT_1: 11;

      

       A63: P[k]

      proof

        

         A64: (sga /. k) = (sga . k) by A61, PARTFUN1:def 6;

        then (sga /. k) in ( rng sga) by A61, FUNCT_1:def 3;

        then (sga /. k) in A by A4, Def2;

        then (sga /. k) in B by A2, XBOOLE_0:def 3;

        then (sga /. k) in ( rng sgb) by A3, Def2;

        then

        consider l be object such that

         A65: l in ( dom sgb) and

         A66: (sgb . l) = (sga /. k) by FUNCT_1:def 3;

        reconsider l as Element of NAT by A65;

        

         A67: (sgb /. l) = (sgb . l) by A65, PARTFUN1:def 6;

        

         A68: 1 <= l by A7, A65, FINSEQ_1: 1;

        assume

         A69: not P[k];

        then

         A70: l <> (k + 1) by A65, A66, PARTFUN1:def 6;

        per cases by XXREAL_0: 1;

          suppose l = k;

          then (sga . k) = a by A8, A9, A64, A66, PARTFUN1:def 6;

          then a in ( rng sga) by A61, FUNCT_1:def 3;

          hence thesis by A1, A4, Def2;

        end;

          suppose

           A71: l < k;

          then l <= lensga by A60, XXREAL_0: 2;

          then

           A72: l in ( dom sga) by A6, A68, FINSEQ_1: 1;

          l <= k9 by A11, A71, NAT_1: 13;

          then (sga /. l) = (sga /. k) by A1, A2, A3, A8, A9, A66, A68, A67, Th76;

          hence thesis by A2, A3, A61, A71, A72, Lm6, Th75;

        end;

          suppose k < l;

          then

           A73: (k + 1) <= l by NAT_1: 13;

          

           A74: 1 <= (k + 1) by NAT_1: 12;

          then

           A75: (k + 1) in ( dom sgb) by A65, A73, FINSEQ_3: 156;

          now

            assume (sgb /. (k + 1)) = a;

            then (k + 1) = k by A3, A8, A9, A75, Th75;

            hence contradiction;

          end;

          then

           A76: not (sgb /. (k + 1)) in {a} by TARSKI:def 1;

          (k + 1) < l by A70, A73, XXREAL_0: 1;

          then

           A77: [(sgb /. (k + 1)), (sgb /. l)] in R by A3, A65, A75, Def2;

          (sgb /. l) in ( rng sgb) by A65, A67, FUNCT_1:def 3;

          then

           A78: (sgb /. l) in B by A3, Def2;

          (sgb /. (k + 1)) = (sgb . (k + 1)) by A65, A73, A74, FINSEQ_3: 156, PARTFUN1:def 6;

          then (sgb /. (k + 1)) in ( rng sgb) by A75, FUNCT_1:def 3;

          then (sgb /. (k + 1)) in B by A3, Def2;

          then (sgb /. (k + 1)) in A by A2, A76, XBOOLE_0:def 3;

          then (sgb /. (k + 1)) in ( rng sga) by A4, Def2;

          then

          consider l9 be object such that

           A79: l9 in ( dom sga) and

           A80: (sga . l9) = (sgb /. (k + 1)) by FUNCT_1:def 3;

          reconsider l9 as Element of NAT by A79;

          

           A81: (sga /. l9) = (sga . l9) by A79, PARTFUN1:def 6;

          

           A82: 1 <= l9 by A6, A79, FINSEQ_1: 1;

          l9 <= lensga by A6, A79, FINSEQ_1: 1;

          then l9 <= lensgb by A62, XXREAL_0: 2;

          then

           A83: l9 in ( dom sgb) by A7, A82, FINSEQ_1: 1;

          now

            assume

             A84: l9 < k;

            then l9 <= k9 by A11, NAT_1: 13;

            then (sgb /. l9) = (sga /. l9) by A1, A2, A3, A8, A9, A82, Th76;

            then l9 = (k + 1) by A3, A75, A79, A80, A83, Th75, PARTFUN1:def 6;

            hence contradiction by A84, XREAL_1: 29;

          end;

          then l9 > k by A69, A80, A81, XXREAL_0: 1;

          then [(sgb /. l), (sgb /. (k + 1))] in R by A4, A61, A66, A67, A79, A80, A81, Def2;

          then (sgb /. l) = (sgb /. (k + 1)) by A5, A77, A78;

          hence thesis by A69, A65, A66, PARTFUN1:def 6;

        end;

      end;

      for j be Element of NAT st k <= j & j <= ( len sga) holds P[j] from INT_1:sch 8( A63, A13);

      hence thesis by A58, A59;

    end;

    theorem :: PRE_POLY:80

    for X be non empty set, A be finite Subset of X, a be Element of X st not a in A holds for B be finite Subset of X st B = ( {a} \/ A) holds for R be Order of X st R linearly_orders B holds for k be Element of NAT st (k + 1) in ( dom ( SgmX (R,B))) & (( SgmX (R,B)) /. (k + 1)) = a holds ( SgmX (R,B)) = ( Ins (( SgmX (R,A)),k,a))

    proof

      let X be non empty set, A be finite Subset of X, a be Element of X;

      assume

       A1: not a in A;

      let B be finite Subset of X;

      assume

       A2: B = ( {a} \/ A);

      let R be Order of X;

      assume

       A3: R linearly_orders B;

      let k be Element of NAT ;

      assume that

       A4: (k + 1) in ( dom ( SgmX (R,B))) and

       A5: (( SgmX (R,B)) /. (k + 1)) = a;

      set sgb = ( SgmX (R,B)), sga = ( Ins (( SgmX (R,A)),k,a));

      

       A6: ( dom sgb) = ( Seg ( len sgb)) by FINSEQ_1:def 3;

      then (k + 1) <= ( len sgb) by A4, FINSEQ_1: 1;

      then

       A7: ((k + 1) - 1) <= (( len sgb) - 1) by XREAL_1: 9;

      

       A8: ((k + 1) - 1) = (k + 0 qua Nat);

      

       A9: ( len sgb) = ( card B) by A3, Th10

      .= (( card A) + 1) by A1, A2, CARD_2: 41

      .= (( len ( SgmX (R,A))) + 1) by A2, A3, Lm6, Th10;

      

      then

       A10: ( dom sgb) = ( Seg ( len sga)) by A6, FINSEQ_5: 69

      .= ( dom sga) by FINSEQ_1:def 3;

      

       A11: for i be Nat st 1 <= i & i <= ( len sgb) holds (sgb . i) = (sga . i)

      proof

        let i be Nat;

        assume that

         A12: 1 <= i and

         A13: i <= ( len sgb);

        

         A14: i in ( Seg ( len sgb)) by A12, A13, FINSEQ_1: 1;

        

         A15: i in ( dom sgb) by FINSEQ_3: 25, A12, A13;

        

         A16: i in ( dom sga) by A10, A14, FINSEQ_1:def 3;

        per cases ;

          suppose

           A17: i = (k + 1);

          then a = (sgb . i) by A5, PARTFUN1:def 6, A15;

          

          hence (sgb . i) = (sga . (k + 1)) by A9, A7, FINSEQ_5: 73

          .= (sga . i) by A17;

        end;

          suppose

           A18: i <> (k + 1);

          now

            per cases ;

              case i < (k + 1);

              then

               A19: i <= k by NAT_1: 13;

              (( SgmX (R,A)) | ( Seg k)) is FinSequence by FINSEQ_1: 15;

              then ( dom (( SgmX (R,A)) | ( Seg k))) = ( Seg k) by A9, A7, FINSEQ_1: 17;

              then

               SS: i in ( dom (( SgmX (R,A)) | ( Seg k))) by A12, A19, FINSEQ_1: 1;

              then

               A20: i in ( dom (( SgmX (R,A)) | k)) by FINSEQ_1:def 15;

              

               A: i in ( dom ( SgmX (R,A))) by RELAT_1: 57, SS;

              

              thus (sgb . i) = (sgb /. i) by A15, PARTFUN1:def 6

              .= (( SgmX (R,A)) /. i) by A1, A2, A3, A4, A5, A8, A12, A14, A19, Th76

              .= (( SgmX (R,A)) . i) by PARTFUN1:def 6, A

              .= (sga . i) by A20, FINSEQ_5: 72;

            end;

              case

               A21: (k + 1) <= i;

              then

               a21: (k + 1) < i by A18, XXREAL_0: 1;

              (1 - 1) <= (i - 1) by A12, XREAL_1: 9;

              then

              reconsider i9 = (i - 1) as Element of NAT by INT_1: 3;

              

               A22: (i9 + 1) = (i + 0 qua Nat);

              

               F: 1 <= (k + 1) by FINSEQ_3: 25, A4;

              (k + 1) < (i9 + 1) by a21;

              then 1 < (i9 + 1) by F, XXREAL_0: 2;

              then (1 + 1) <= (i9 + 1) by NAT_1: 13;

              then

               F1: 1 <= i9 by XREAL_1: 6;

              

               Z2: (i9 + 1) in ( dom sga) by A16;

              then (i9 + 1) <= ( len sga) by FINSEQ_3: 25;

              then (i9 + 1) <= (( len ( SgmX (R,A))) + 1) by FINSEQ_5: 69;

              then i9 <= ( len ( SgmX (R,A))) by XREAL_1: 6;

              then

               F2: i9 in ( dom ( SgmX (R,A))) by FINSEQ_3: 25, F1;

              (k + 1) < i by A18, A21, XXREAL_0: 1;

              then

               A23: (k + 1) <= i9 by A22, NAT_1: 13;

              

               A24: i9 <= (( len sgb) - 1) by A13, XREAL_1: 9;

              

              thus (sgb . i) = (sgb /. (i9 + 1)) by A15, PARTFUN1:def 6

              .= (( SgmX (R,A)) /. i9) by A1, A2, A3, A4, A5, A9, A24, A23, Th77

              .= (( SgmX (R,A)) . i9) by PARTFUN1:def 6, F2

              .= (sga . (i9 + 1)) by A9, A24, A23, FINSEQ_5: 74

              .= (sga /. (i9 + 1)) by Z2, PARTFUN1:def 6

              .= (sga . i) by A16, PARTFUN1:def 6;

            end;

          end;

          hence thesis;

        end;

      end;

      ( len sgb) = ( len sga) by A9, FINSEQ_5: 69;

      hence thesis by A11, FINSEQ_1: 14;

    end;

    theorem :: PRE_POLY:81

    for X be set, b be bag of X st ( support b) = {} holds b = ( EmptyBag X) by Def7;

    

     Lm7: for X be set, b be bag of X holds b is PartFunc of X, NAT

    proof

      let X be set, b be bag of X;

      for u be object holds u in b implies u in [:X, NAT :]

      proof

        let u be object;

        

         A1: ( rng b) c= NAT by VALUED_0:def 6;

        assume

         A2: u in b;

        then

        consider u1,u2 be object such that

         A3: u = [u1, u2] by RELAT_1:def 1;

        u1 in ( dom b) by A2, A3, XTUPLE_0:def 12;

        then

         A4: u1 in X;

        u2 in ( rng b) by A2, A3, XTUPLE_0:def 13;

        hence thesis by A3, A4, A1, ZFMISC_1:def 2;

      end;

      hence thesis by TARSKI:def 3;

    end;

    definition

      let X be set, b be bag of X;

      :: original: empty-yielding

      redefine

      :: PRE_POLY:def18

      attr b is empty-yielding means b = ( EmptyBag X);

      compatibility ;

    end

    registration

      let X be non empty set;

      cluster non empty-yielding for bag of X;

      existence

      proof

        set x = the Element of X;

        set b = (( EmptyBag X) +* (x,1));

        take b;

        ( dom ( EmptyBag X)) = X;

        then

         A1: (b . x) = ((( EmptyBag X) +* (x .--> 1)) . x) by FUNCT_7:def 3;

        x in ( dom (x .--> 1)) by TARSKI:def 1;

        

        then (b . x) = ((x .--> 1) . x) by A1, FUNCT_4: 13

        .= 1 by FUNCOP_1: 72;

        then (b . x) <> (( EmptyBag X) . x);

        hence thesis;

      end;

    end

    definition

      let X be set, b be bag of X;

      :: original: support

      redefine

      func support b -> finite Subset of X ;

      coherence

      proof

        

         A1: ( support b) c= ( dom b) by Th36;

        for x be object holds x in ( support b) implies x in X

        proof

          let x be object;

          assume x in ( support b);

          then x in ( dom b) by A1;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    

     Lm8: for X be set, A be Subset of X, O be Order of X holds O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A

    proof

      let X be set, A be Subset of X, O be Order of X;

      

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

      then O is_antisymmetric_in X by RELAT_2:def 12;

      then

       A2: for x,y be object holds x in A & y in A & [x, y] in O & [y, x] in O implies x = y;

      O is_transitive_in X by A1, RELAT_2:def 16;

      then

       A3: for x,y,z be object holds x in A & y in A & z in A & [x, y] in O & [y, z] in O implies [x, z] in O;

      O is_reflexive_in X by A1, RELAT_2:def 9;

      then for x be object holds x in A implies [x, x] in O;

      hence thesis by A2, A3;

    end;

    theorem :: PRE_POLY:82

    for n be Ordinal, b be bag of n holds ( RelIncl n) linearly_orders ( support b)

    proof

      let n be Ordinal, b be bag of n;

      set R = ( RelIncl n), s = ( support b);

      for x,y be object holds x in s & y in s & x <> y implies [x, y] in R or [y, x] in R

      proof

        let x,y be object;

        assume that

         A1: x in s and

         A2: y in s and x <> y;

        assume

         A3: not [x, y] in R;

        reconsider x, y as Ordinal by A1, A2;

        y c= x by A1, A2, A3, WELLORD2:def 1;

        hence thesis by A1, A2, WELLORD2:def 1;

      end;

      then

       A4: R is_connected_in s;

      

       A5: R is_antisymmetric_in s by Lm8;

      

       A6: R is_transitive_in s by Lm8;

      R is_reflexive_in s by Lm8;

      hence thesis by A4, A5, A6, ORDERS_1:def 9;

    end;

    definition

      let X be set;

      let x be FinSequence of X, b be bag of X;

      :: original: *

      redefine

      func b * x -> PartFunc of NAT , NAT ;

      coherence

      proof

        reconsider b as PartFunc of X, NAT by Lm7;

        (b * x) c= [: NAT , NAT :];

        hence thesis;

      end;

    end

    registration

      let X be set;

      cluster ( support ( EmptyBag X)) -> empty;

      coherence

      proof

        set S = ( support ( EmptyBag X));

        assume not ( support ( EmptyBag X)) is empty;

        then (( EmptyBag X) . the Element of S) <> 0 by Def7;

        hence thesis;

      end;

    end