polynom6.miz



    begin

    reserve o1,o2 for Ordinal;

    notation

      let L1,L2 be non empty doubleLoopStr;

      synonym L1,L2 are_isomorphic for L1 is_ringisomorph_to L2;

    end

    definition

      let L1,L2 be non empty doubleLoopStr;

      :: original: is_ringisomorph_to

      redefine

      pred L1 is_ringisomorph_to L2;

      reflexivity

      proof

        let L1 be non empty doubleLoopStr;

        take ( id L1);

        thus ( id L1) is RingHomomorphism;

        thus ( id L1) is one-to-one;

        

        thus ( rng ( id L1)) = ( [#] L1) by TOPGRP_1: 1

        .= the carrier of L1;

      end;

    end

    theorem :: POLYNOM6:1

    

     Th1: for B be set st for x be set holds x in B iff ex o be Ordinal st x = (o1 +^ o) & o in o2 holds (o1 +^ o2) = (o1 \/ B)

    proof

      let B be set;

      assume

       A1: for x be set holds x in B iff ex o be Ordinal st x = (o1 +^ o) & o in o2;

      for x be object holds x in (o1 +^ o2) iff x in (o1 \/ B)

      proof

        let x be object;

        

         A2: x in (o1 \/ B) implies x in (o1 +^ o2)

        proof

          assume

           A3: x in (o1 \/ B);

          per cases by A3, XBOOLE_0:def 3;

            suppose

             A4: x in o1;

            o1 c= (o1 +^ o2) by ORDINAL3: 24;

            hence thesis by A4;

          end;

            suppose x in B;

            then ex o be Ordinal st x = (o1 +^ o) & o in o2 by A1;

            hence thesis by ORDINAL2: 32;

          end;

        end;

        per cases ;

          suppose x in o1;

          hence x in (o1 +^ o2) implies x in (o1 \/ B) by XBOOLE_0:def 3;

          thus thesis by A2;

        end;

          suppose

           A5: not x in o1;

          thus x in (o1 +^ o2) implies x in (o1 \/ B)

          proof

            assume

             A6: x in (o1 +^ o2);

            per cases ;

              suppose o2 = {} ;

              hence thesis by A5, A6, ORDINAL2: 27;

            end;

              suppose

               A7: o2 <> {} ;

              reconsider o = x as Ordinal by A6;

              o1 c= o by A5, ORDINAL1: 16;

              then

               A8: o = (o1 +^ (o -^ o1)) by ORDINAL3:def 5;

              (o -^ o1) in o2 by A6, A7, ORDINAL3: 60;

              then x in B by A1, A8;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

          thus thesis by A2;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let o1 be Ordinal, o2 be non empty Ordinal;

      cluster (o1 +^ o2) -> non empty;

      coherence by ORDINAL3: 26;

      cluster (o2 +^ o1) -> non empty;

      coherence by ORDINAL3: 26;

    end

    theorem :: POLYNOM6:2

    

     Th2: for n be Ordinal, a,b be bag of n st a < b holds ex o be Ordinal st o in n & (a . o) < (b . o) & for l be Ordinal st l in o holds (a . l) = (b . l)

    proof

      let n be Ordinal, a,b be bag of n;

      assume a < b;

      then

      consider o be Ordinal such that

       A1: (a . o) < (b . o) and

       A2: for l be Ordinal st l in o holds (a . l) = (b . l) by PRE_POLY:def 9;

      take o;

      now

        assume

         A3: not o in n;

        then

         A4: not o in ( dom b) by PARTFUN1:def 2;

        n = ( dom a) by PARTFUN1:def 2;

        then (a . o) = 0 by A3, FUNCT_1:def 2;

        hence contradiction by A1, A4, FUNCT_1:def 2;

      end;

      hence o in n;

      thus (a . o) < (b . o) by A1;

      thus thesis by A2;

    end;

    begin

    definition

      let o1,o2 be Ordinal;

      let a be Element of ( Bags o1), b be Element of ( Bags o2);

      :: POLYNOM6:def1

      func a +^ b -> Element of ( Bags (o1 +^ o2)) means

      : Def1: for o be Ordinal holds (o in o1 implies (it . o) = (a . o)) & (o in ((o1 +^ o2) \ o1) implies (it . o) = (b . (o -^ o1)));

      existence

      proof

        per cases ;

          suppose

           A1: o2 = {} ;

          then

          reconsider a9 = a as Element of ( Bags (o1 +^ o2)) by ORDINAL2: 27;

          take a9;

          let o be Ordinal;

          thus o in o1 implies (a9 . o) = (a . o);

          (o1 +^ o2) = o1 by A1, ORDINAL2: 27;

          hence thesis by XBOOLE_1: 37;

        end;

          suppose o2 <> {} ;

          then

          reconsider o29 = o2 as non empty Ordinal;

          defpred P[ object, object] means ex o be Ordinal st o = $1 & (o in o1 implies $2 = (a . o)) & (o in ((o1 +^ o2) \ o1) implies $2 = (b . (o -^ o1)));

          deffunc F( Element of o29) = (o1 +^ $1);

          set B = { F(o) where o be Element of o29 : o in ( support b) }, C = the set of all (o1 +^ o) where o be Element of o29;

          

           A2: for i be object st i in (o1 +^ o2) holds ex j be object st P[i, j]

          proof

            let i be object such that

             A3: i in (o1 +^ o2);

            reconsider o = i as Ordinal by A3;

            

             A4: o in o1 iff not o in ((o1 +^ o2) \ o1) by A3, XBOOLE_0:def 5;

            per cases by A3, XBOOLE_0:def 5;

              suppose

               A5: o in o1;

              take (a . o), o;

              thus thesis by A5, XBOOLE_0:def 5;

            end;

              suppose

               A6: o in ((o1 +^ o2) \ o1);

              take (b . (o -^ o1));

              thus thesis by A4, A6;

            end;

          end;

          consider f be ManySortedSet of (o1 +^ o2) such that

           A7: for i be object st i in (o1 +^ o2) holds P[i, (f . i)] from PBOOLE:sch 3( A2);

          

           A8: ( support f) c= (( support a) \/ B)

          proof

            let x be object;

            assume x in ( support f);

            then

             A9: (f . x) <> 0 by PRE_POLY:def 7;

            then x in ( dom f) by FUNCT_1:def 2;

            then

             A10: x in (o1 +^ o2) by PARTFUN1:def 2;

            for x be set holds x in C iff ex o be Ordinal st x = (o1 +^ o) & o in o2

            proof

              let x be set;

              thus x in C implies ex o be Ordinal st x = (o1 +^ o) & o in o2

              proof

                assume x in C;

                then ex o9 be Element of o29 st x = (o1 +^ o9);

                hence thesis;

              end;

              thus thesis;

            end;

            then

             A11: x in (o1 \/ C) by A10, Th1;

            per cases by A11, XBOOLE_0:def 3;

              suppose

               A12: x in o1;

               P[x, (f . x)] by A7, A10;

              then x in ( support a) by A9, A12, PRE_POLY:def 7;

              hence thesis by XBOOLE_0:def 3;

            end;

              suppose x in C;

              then ex o9 be Element of o29 st x = (o1 +^ o9);

              then

              consider o99 be Ordinal such that

               A13: x = (o1 +^ o99) and

               A14: o99 in o2;

              reconsider o = x as Ordinal by A13;

              

               A15: o1 c= o by A13, ORDINAL3: 24;

               A16:

              now

                per cases ;

                  suppose o = o1;

                  hence not o in o1;

                end;

                  suppose o <> o1;

                  then o1 c< o by A15;

                  hence not o in o1 by ORDINAL1: 11;

                end;

              end;

              

               A17: P[x, (f . x)] by A7, A10;

              x in (o1 +^ o2) & o99 = (o -^ o1) by A13, A14, ORDINAL2: 32, ORDINAL3: 52;

              then o99 in ( support b) by A9, A16, A17, PRE_POLY:def 7, XBOOLE_0:def 5;

              then x in B by A13;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

          

           A18: ( support b) is finite;

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

          then

           A19: f is finite-support by A8, PRE_POLY:def 8;

          f is natural-valued

          proof

            let x be object;

            assume x in ( dom f);

            then

             A20: x in (o1 +^ o2) by PARTFUN1:def 2;

            then

            reconsider o = x as Ordinal;

            

             A21: ex o9 be Ordinal st o9 = x & (o9 in o1 implies (f . x) = (a . o9)) & (o9 in ((o1 +^ o2) \ o1) implies (f . x) = (b . (o9 -^ o1))) by A7, A20;

            per cases by A20, XBOOLE_0:def 5;

              suppose o in o1;

              hence thesis by A21;

            end;

              suppose o in ((o1 +^ o2) \ o1);

              hence thesis by A21;

            end;

          end;

          then

          reconsider f as Element of ( Bags (o1 +^ o2)) by A19, PRE_POLY:def 12;

          take f;

          let o be Ordinal;

          thus o in o1 implies (f . o) = (a . o)

          proof

            assume

             A22: o in o1;

            o1 c= (o1 +^ o2) by ORDINAL3: 24;

            then ex p be Ordinal st p = o & (p in o1 implies (f . o) = (a . p)) & (p in ((o1 +^ o2) \ o1) implies (f . o) = (b . (p -^ o1))) by A7, A22;

            hence thesis by A22;

          end;

          assume

           A23: o in ((o1 +^ o2) \ o1);

          then ex p be Ordinal st p = o & (p in o1 implies (f . o) = (a . p)) & (p in ((o1 +^ o2) \ o1) implies (f . o) = (b . (p -^ o1))) by A7;

          hence thesis by A23;

        end;

      end;

      uniqueness

      proof

        let a1,a2 be Element of ( Bags (o1 +^ o2)) such that

         A24: for o be Ordinal holds (o in o1 implies (a1 . o) = (a . o)) & (o in ((o1 +^ o2) \ o1) implies (a1 . o) = (b . (o -^ o1))) and

         A25: for o be Ordinal holds (o in o1 implies (a2 . o) = (a . o)) & (o in ((o1 +^ o2) \ o1) implies (a2 . o) = (b . (o -^ o1)));

        

         A26: ( dom a1) = (o1 +^ o2) by PARTFUN1:def 2;

        

         A27: for c be object st c in ( dom a1) holds (a1 . c) = (a2 . c)

        proof

          let c be object such that

           A28: c in ( dom a1);

          reconsider o = c as Ordinal by A26, A28;

          

           A29: o1 c= (o1 +^ o2) by ORDINAL3: 24;

          

           A30: (((o1 +^ o2) \ o1) \/ o1) = ((o1 +^ o2) \/ o1) by XBOOLE_1: 39

          .= (o1 +^ o2) by A29, XBOOLE_1: 12;

          per cases by A26, A28, A30, XBOOLE_0:def 3;

            suppose

             A31: o in o1;

            

            hence (a1 . c) = (a . o) by A24

            .= (a2 . c) by A25, A31;

          end;

            suppose

             A32: o in ((o1 +^ o2) \ o1);

            

            hence (a1 . c) = (b . (o -^ o1)) by A24

            .= (a2 . c) by A25, A32;

          end;

        end;

        ( dom a1) = ( dom a2) by A26, PARTFUN1:def 2;

        hence a1 = a2 by A27;

      end;

    end

    theorem :: POLYNOM6:3

    

     Th3: for a be Element of ( Bags o1), b be Element of ( Bags o2) st o2 = {} holds (a +^ b) = a

    proof

      let a be Element of ( Bags o1), b be Element of ( Bags o2);

      assume o2 = {} ;

      then

      reconsider ab = (a +^ b) as Element of ( Bags o1) by ORDINAL2: 27;

      for i be object st i in o1 holds (ab . i) = (a . i) by Def1;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: POLYNOM6:4

    for a be Element of ( Bags o1), b be Element of ( Bags o2) st o1 = {} holds (a +^ b) = b

    proof

      let a be Element of ( Bags o1), b be Element of ( Bags o2);

      assume

       A1: o1 = {} ;

      then

      reconsider ab = (a +^ b) as Element of ( Bags o2) by ORDINAL2: 30;

      now

        let i be object;

        assume

         A2: i in o2;

        then

        reconsider i9 = i as Ordinal;

        

         A3: (i9 -^ o1) = i9 by A1, ORDINAL3: 56;

        i in ((o1 +^ o2) \ o1) by A1, A2, ORDINAL2: 30;

        hence (ab . i) = (b . i) by A3, Def1;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: POLYNOM6:5

    

     Th5: for b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) holds (b1 +^ b2) = ( EmptyBag (o1 +^ o2)) iff b1 = ( EmptyBag o1) & b2 = ( EmptyBag o2)

    proof

      let b1 be Element of ( Bags o1), b2 be Element of ( Bags o2);

      hereby

        assume

         A1: (b1 +^ b2) = ( EmptyBag (o1 +^ o2));

        

         A2: for z be object st z in ( dom b1) holds (b1 . z) = 0

        proof

          let z be object;

          

           A3: ( dom b1) = o1 by PARTFUN1:def 2;

          assume

           A4: z in ( dom b1);

          then

          reconsider o = z as Ordinal by A3;

          (b1 . o) = ((b1 +^ b2) . o) by A4, A3, Def1

          .= 0 by A1, PBOOLE: 5;

          hence thesis;

        end;

        ( dom b1) = o1 by PARTFUN1:def 2;

        then b1 = (o1 --> 0 ) by A2, FUNCOP_1: 11;

        hence b1 = ( EmptyBag o1) by PBOOLE:def 3;

        

         A5: for z be object st z in ( dom b2) holds (b2 . z) = 0

        proof

          let z be object;

          

           A6: ( dom b2) = o2 by PARTFUN1:def 2;

          assume

           A7: z in ( dom b2);

          then

          reconsider o = z as Ordinal by A6;

          o1 c= (o1 +^ o) by ORDINAL3: 24;

          then

           A8: not (o1 +^ o) in o1 by ORDINAL1: 5;

          (o1 +^ o) in (o1 +^ o2) by A7, A6, ORDINAL2: 32;

          then (o1 +^ o) in ((o1 +^ o2) \ o1) by A8, XBOOLE_0:def 5;

          then ((b1 +^ b2) . (o1 +^ o)) = (b2 . ((o1 +^ o) -^ o1)) by Def1;

          then (b2 . ((o1 +^ o) -^ o1)) = 0 by A1, PBOOLE: 5;

          hence thesis by ORDINAL3: 52;

        end;

        ( dom b2) = o2 by PARTFUN1:def 2;

        then b2 = (o2 --> 0 ) by A5, FUNCOP_1: 11;

        hence b2 = ( EmptyBag o2) by PBOOLE:def 3;

      end;

      thus b1 = ( EmptyBag o1) & b2 = ( EmptyBag o2) implies (b1 +^ b2) = ( EmptyBag (o1 +^ o2))

      proof

        assume that

         A9: b1 = ( EmptyBag o1) and

         A10: b2 = ( EmptyBag o2);

        

         A11: for z be object st z in ( dom (b1 +^ b2)) holds ((b1 +^ b2) . z) = 0

        proof

          let z be object;

          

           A12: ( dom (b1 +^ b2)) = (o1 +^ o2) by PARTFUN1:def 2;

          assume

           A13: z in ( dom (b1 +^ b2));

          then

          reconsider o = z as Ordinal by A12;

          

           A14: o in ((o1 +^ o2) \ o1) implies (b2 . (o -^ o1)) = 0 & ((b1 +^ b2) . o) = (b2 . (o -^ o1)) by A10, Def1, PBOOLE: 5;

          o in o1 implies (b1 . o) = 0 & ((b1 +^ b2) . o) = (b1 . o) by A9, Def1, PBOOLE: 5;

          hence thesis by A13, A12, A14, XBOOLE_0:def 5;

        end;

        ( dom (b1 +^ b2)) = (o1 +^ o2) by PARTFUN1:def 2;

        then (b1 +^ b2) = ((o1 +^ o2) --> 0 ) by A11, FUNCOP_1: 11;

        hence thesis by PBOOLE:def 3;

      end;

    end;

    theorem :: POLYNOM6:6

    

     Th6: for c be Element of ( Bags (o1 +^ o2)) holds ex c1 be Element of ( Bags o1), c2 be Element of ( Bags o2) st c = (c1 +^ c2)

    proof

      let c be Element of ( Bags (o1 +^ o2));

      per cases ;

        suppose

         A1: o2 is empty;

        then

        reconsider c2 = {} as Element of ( Bags o2) by PRE_POLY: 51, TARSKI:def 1;

        reconsider c1 = c as Element of ( Bags o1) by A1, ORDINAL2: 27;

        take c1;

        take c2;

        thus thesis by A1, Th3;

      end;

        suppose

         A2: o2 is non empty;

        then

        reconsider o29 = o2 as non empty Ordinal;

        

         A3: ( support (c | o1)) c= ( support c)

        proof

          let x be object;

          assume x in ( support (c | o1));

          then

           A4: ((c | o1) . x) <> 0 by PRE_POLY:def 7;

          then x in ( dom (c | o1)) by FUNCT_1:def 2;

          then [x, ((c | o1) . x)] in (c | o1) by FUNCT_1: 1;

          then [x, ((c | o1) . x)] in c by RELAT_1:def 11;

          then ((c | o1) . x) = (c . x) by FUNCT_1: 1;

          hence thesis by A4, PRE_POLY:def 7;

        end;

        ( dom c) = (o1 +^ o2) by PARTFUN1:def 2;

        then o1 c= ( dom c) by ORDINAL3: 24;

        then ( dom (c | o1)) = o1 by RELAT_1: 62;

        then (c | o1) is bag of o1 by A3, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

        then

        reconsider c1 = (c | o1) as Element of ( Bags o1) by PRE_POLY:def 12;

        deffunc F( Element of (o1 +^ o29)) = ($1 -^ o1);

        defpred P[ object, object] means for x1 be Element of o2 st x1 = $1 holds $2 = (c . (o1 +^ x1));

        take c1;

        set B = { (o9 -^ o1) where o9 be Element of (o1 +^ o29) : o1 c= o9 & o9 in ( support c) }, C = { F(o9) where o9 be Element of (o1 +^ o29) : o9 in ( support c) };

        

         A5: B c= C

        proof

          let x be object;

          assume x in B;

          then ex o9 be Element of (o1 +^ o29) st x = (o9 -^ o1) & o1 c= o9 & o9 in ( support c);

          hence thesis;

        end;

        

         A6: for i be object st i in o2 holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in o2;

          then

          reconsider x1 = i as Element of o2;

          take (c . (o1 +^ x1));

          thus thesis;

        end;

        consider f be ManySortedSet of o2 such that

         A7: for i be object st i in o2 holds P[i, (f . i)] from PBOOLE:sch 3( A6);

        

         A8: ( support f) c= B

        proof

          let x be object;

          assume x in ( support f);

          then

           A9: (f . x) <> 0 by PRE_POLY:def 7;

          then x in ( dom f) by FUNCT_1:def 2;

          then

          reconsider o9 = x as Element of o29 by PARTFUN1:def 2;

          (c . (o1 +^ o9)) <> 0 by A7, A9;

          then

           A10: (o1 +^ o9) in ( support c) by PRE_POLY:def 7;

          reconsider o99 = (o1 +^ o9) as Element of (o1 +^ o29) by ORDINAL2: 32;

          o9 = (o99 -^ o1) & o1 c= o99 by ORDINAL3: 24, ORDINAL3: 52;

          hence thesis by A10;

        end;

        

         A11: f is natural-valued

        proof

          let x be object;

          assume

           A12: x in ( dom f);

          then

          reconsider o = x as Element of o2 by PARTFUN1:def 2;

          x in o2 by A12, PARTFUN1:def 2;

          then (f . x) = (c . (o1 +^ o)) by A7;

          hence thesis;

        end;

        

         A13: ( support c) is finite;

        C is finite from FRAENKEL:sch 21( A13);

        then f is finite-support by A5, A8, PRE_POLY:def 8;

        then

        reconsider c2 = f as Element of ( Bags o2) by A11, PRE_POLY:def 12;

        take c2;

        now

          let i be object;

          assume

           A14: i in (o1 +^ o2);

          per cases by A14, XBOOLE_0:def 5;

            suppose

             A15: i in o1;

            then

            reconsider i9 = i as Ordinal;

            ( dom c1) = o1 by PARTFUN1:def 2;

            

            then (c . i9) = (c1 . i9) by A15, FUNCT_1: 47

            .= ((c1 +^ c2) . i9) by A15, Def1;

            hence (c . i) = ((c1 +^ c2) . i);

          end;

            suppose

             A16: i in ((o1 +^ o2) \ o1);

            then

            reconsider i9 = i as Ordinal;

            

             A17: (i9 -^ o1) in o2 by A2, A16, ORDINAL3: 60;

             not i9 in o1 by A16, XBOOLE_0:def 5;

            then o1 c= i9 by ORDINAL1: 16;

            

            then (c . i9) = (c . (o1 +^ (i9 -^ o1))) by ORDINAL3:def 5

            .= (c2 . (i9 -^ o1)) by A7, A17

            .= ((c1 +^ c2) . i9) by A16, Def1;

            hence (c . i) = ((c1 +^ c2) . i);

          end;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end;

    theorem :: POLYNOM6:7

    

     Th7: for b1,c1 be Element of ( Bags o1) holds for b2,c2 be Element of ( Bags o2) st (b1 +^ b2) = (c1 +^ c2) holds b1 = c1 & b2 = c2

    proof

      let b1,c1 be Element of ( Bags o1), b2,c2 be Element of ( Bags o2);

      assume

       A1: (b1 +^ b2) = (c1 +^ c2);

      now

        let i be object;

        assume

         A2: i in o1;

        then

        reconsider i9 = i as Ordinal;

        ((b1 +^ b2) . i9) = (b1 . i9) by A2, Def1;

        hence (b1 . i) = (c1 . i) by A1, A2, Def1;

      end;

      hence b1 = c1 by PBOOLE: 3;

      now

        let i be object;

        assume

         A3: i in o2;

        then

        reconsider i9 = i as Ordinal;

        

         A4: i9 = ((o1 +^ i9) -^ o1) by ORDINAL3: 52;

        o1 c= (o1 +^ i9) by ORDINAL3: 24;

        then

         A5: not (o1 +^ i9) in o1 by ORDINAL1: 5;

        (o1 +^ i9) in (o1 +^ o2) by A3, ORDINAL2: 32;

        then

         A6: (o1 +^ i9) in ((o1 +^ o2) \ o1) by A5, XBOOLE_0:def 5;

        then ((b1 +^ b2) . (o1 +^ i9)) = (b2 . ((o1 +^ i9) -^ o1)) by Def1;

        hence (b2 . i) = (c2 . i) by A1, A6, A4, Def1;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: POLYNOM6:8

    

     Th8: for n be Ordinal, L be Abelian add-associative right_zeroed right_complementable distributive associative non empty doubleLoopStr, p,q,r be Series of n, L holds ((p + q) *' r) = ((p *' r) + (q *' r))

    proof

      let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable distributive associative non empty doubleLoopStr, p,q,r be Series of n, L;

      set cL = the carrier of L;

      now

        let b be Element of ( Bags n);

        consider s be FinSequence of cL such that

         A1: (((p + q) *' r) . b) = ( Sum s) and

         A2: ( len s) = ( len ( decomp b)) and

         A3: for k be Element of NAT st k in ( dom s) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (s /. k) = (((p + q) . b1) * (r . b2)) by POLYNOM1:def 10;

        consider u be FinSequence of cL such that

         A4: ((q *' r) . b) = ( Sum u) and

         A5: ( len u) = ( len ( decomp b)) and

         A6: for k be Element of NAT st k in ( dom u) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (u /. k) = ((q . b1) * (r . b2)) by POLYNOM1:def 10;

        consider t be FinSequence of cL such that

         A7: ((p *' r) . b) = ( Sum t) and

         A8: ( len t) = ( len ( decomp b)) and

         A9: for k be Element of NAT st k in ( dom t) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (t /. k) = ((p . b1) * (r . b2)) by POLYNOM1:def 10;

        reconsider t, u as Element of (( len s) -tuples_on cL) by A2, A8, A5, FINSEQ_2: 92;

        

         A10: ( dom u) = ( dom s) by A2, A5, FINSEQ_3: 29;

        

         A11: ( dom t) = ( dom s) by A2, A8, FINSEQ_3: 29;

        then

         A12: ( dom (t + u)) = ( dom s) by A10, POLYNOM1: 1;

         A13:

        now

          let i be Nat;

          assume

           A14: i in ( dom s);

          then

          consider sb1,sb2 be bag of n such that

           A15: (( decomp b) /. i) = <*sb1, sb2*> and

           A16: (s /. i) = (((p + q) . sb1) * (r . sb2)) by A3;

          

           A17: (t /. i) = (t . i) & (u /. i) = (u . i) by A11, A10, A14, PARTFUN1:def 6;

          consider ub1,ub2 be bag of n such that

           A18: (( decomp b) /. i) = <*ub1, ub2*> and

           A19: (u /. i) = ((q . ub1) * (r . ub2)) by A6, A10, A14;

          

           A20: sb1 = ub1 & sb2 = ub2 by A15, A18, FINSEQ_1: 77;

          consider tb1,tb2 be bag of n such that

           A21: (( decomp b) /. i) = <*tb1, tb2*> and

           A22: (t /. i) = ((p . tb1) * (r . tb2)) by A9, A11, A14;

          

           A23: sb1 = tb1 & sb2 = tb2 by A15, A21, FINSEQ_1: 77;

          (s /. i) = (s . i) by A14, PARTFUN1:def 6;

          

          hence (s . i) = (((p . sb1) + (q . sb1)) * (r . sb2)) by A16, POLYNOM1: 15

          .= (((p . sb1) * (r . sb2)) + ((q . sb1) * (r . sb2))) by VECTSP_1:def 7

          .= ((t + u) . i) by A12, A14, A22, A19, A23, A20, A17, FVSUM_1: 17;

        end;

        ( len (t + u)) = ( len s) by A12, FINSEQ_3: 29;

        then s = (t + u) by A13, FINSEQ_2: 9;

        

        hence (((p + q) *' r) . b) = (( Sum t) + ( Sum u)) by A1, FVSUM_1: 76

        .= (((p *' r) + (q *' r)) . b) by A7, A4, POLYNOM1: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    registration

      let n be Ordinal, L be right_zeroed Abelian add-associative right_complementable well-unital distributive associative non trivial non empty doubleLoopStr;

      cluster ( Polynom-Ring (n,L)) -> non trivial distributive;

      coherence

      proof

        thus ( Polynom-Ring (n,L)) is non trivial

        proof

          take ( 1_ ( Polynom-Ring (n,L)));

          

           A1: ( 1_ ( Polynom-Ring (n,L))) = ( 1_ (n,L)) & (( 0_ (n,L)) . ( EmptyBag n)) = ( 0. L) by POLYNOM1: 22, POLYNOM1: 31;

          ( 0. L) <> ( 1_ L) & ( 0. ( Polynom-Ring (n,L))) = ( 0_ (n,L)) by POLYNOM1:def 11;

          hence thesis by A1, POLYNOM1: 25;

        end;

        thus ( Polynom-Ring (n,L)) is distributive

        proof

          let x,y,z be Element of ( Polynom-Ring (n,L));

          reconsider u = x, v = y, w = z as Polynomial of n, L by POLYNOM1:def 11;

          reconsider x9 = x, y9 = y, z9 = z as Element of ( Polynom-Ring (n,L));

          

           A2: (u *' v) = (x9 * y9) & (u *' w) = (x9 * z9) by POLYNOM1:def 11;

          (y9 + z9) = (v + w) by POLYNOM1:def 11;

          

          hence (x * (y + z)) = (u *' (v + w)) by POLYNOM1:def 11

          .= ((u *' v) + (u *' w)) by POLYNOM1: 26

          .= ((x * y) + (x * z)) by A2, POLYNOM1:def 11;

          

           A3: (v *' u) = (y9 * x9) & (w *' u) = (z9 * x9) by POLYNOM1:def 11;

          (y9 + z9) = (v + w) by POLYNOM1:def 11;

          

          hence ((y + z) * x) = ((v + w) *' u) by POLYNOM1:def 11

          .= ((v *' u) + (w *' u)) by Th8

          .= ((y * x) + (z * x)) by A3, POLYNOM1:def 11;

        end;

      end;

    end

    definition

      let o1,o2 be non empty Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr;

      let P be Polynomial of o1, ( Polynom-Ring (o2,L));

      :: POLYNOM6:def2

      func Compress P -> Polynomial of (o1 +^ o2), L means

      : Def2: for b be Element of ( Bags (o1 +^ o2)) holds ex b1 be Element of ( Bags o1), b2 be Element of ( Bags o2), Q1 be Polynomial of o2, L st Q1 = (P . b1) & b = (b1 +^ b2) & (it . b) = (Q1 . b2);

      existence

      proof

        deffunc F( Element of ( Bags o1)) = { ($1 +^ b2) where b2 be Element of ( Bags o2) : ex Q be Polynomial of o2, L st Q = (P . $1) & b2 in ( Support Q) };

        defpred P[ Element of ( Bags (o1 +^ o2)), Element of L] means ex b1 be Element of ( Bags o1), b2 be Element of ( Bags o2), Q1 be Polynomial of o2, L st Q1 = (P . b1) & $1 = (b1 +^ b2) & $2 = (Q1 . b2);

        set A = { F(b1) where b1 be Element of ( Bags o1) : b1 in ( Support P) };

        

         A1: for B be set st B in A holds B is finite

        proof

          let B be set;

          assume B in A;

          then

          consider b1 be Element of ( Bags o1) such that

           A2: B = { (b1 +^ b2) where b2 be Element of ( Bags o2) : ex Q be Polynomial of o2, L st Q = (P . b1) & b2 in ( Support Q) } and b1 in ( Support P);

          deffunc F( Element of ( Bags o2)) = (b1 +^ $1);

          reconsider Q0 = (P . b1) as Polynomial of o2, L by POLYNOM1:def 11;

          set B0 = { F(b2) where b2 be Element of ( Bags o2) : b2 in ( Support Q0) };

          

           A3: B c= B0

          proof

            let x be object;

            assume x in B;

            then ex b2 be Element of ( Bags o2) st x = (b1 +^ b2) & ex Q be Polynomial of o2, L st Q = (P . b1) & b2 in ( Support Q) by A2;

            hence thesis;

          end;

          

           A4: ( Support Q0) is finite;

          B0 is finite from FRAENKEL:sch 21( A4);

          hence thesis by A3;

        end;

        

         A5: for b be Element of ( Bags (o1 +^ o2)) holds ex u be Element of L st P[b, u]

        proof

          let b be Element of ( Bags (o1 +^ o2));

          consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) such that

           A6: b = (b1 +^ b2) by Th6;

          reconsider Q1 = (P . b1) as Polynomial of o2, L by POLYNOM1:def 11;

          take (Q1 . b2), b1, b2, Q1;

          thus thesis by A6;

        end;

        consider f be Function of ( Bags (o1 +^ o2)), the carrier of L such that

         A7: for b be Element of ( Bags (o1 +^ o2)) holds P[b, (f . b)] from FUNCT_2:sch 3( A5);

        reconsider f as Series of (o1 +^ o2), L;

        

         A8: ( Support f) = ( union A)

        proof

          thus ( Support f) c= ( union A)

          proof

            let x be object;

            assume

             A9: x in ( Support f);

            then

             A10: (f . x) <> ( 0. L) by POLYNOM1:def 4;

            consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) such that

             A11: x = (b1 +^ b2) by A9, Th6;

            consider Y be set such that

             A12: Y = { (b1 +^ b29) where b29 be Element of ( Bags o2) : ex Q be Polynomial of o2, L st Q = (P . b1) & b29 in ( Support Q) };

            consider b19 be Element of ( Bags o1), b29 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

             A13: Q1 = (P . b19) and

             A14: (b1 +^ b2) = (b19 +^ b29) and

             A15: (f . (b1 +^ b2)) = (Q1 . b29) by A7;

            

             A16: b1 = b19 by A14, Th7;

            now

              assume (P . b1) = ( 0. ( Polynom-Ring (o2,L)));

              then Q1 = ( 0_ (o2,L)) by A13, A16, POLYNOM1:def 11;

              hence contradiction by A10, A11, A15, POLYNOM1: 22;

            end;

            then b1 in ( Support P) by POLYNOM1:def 4;

            then

             A17: Y in A by A12;

            b2 = b29 by A14, Th7;

            then b2 in ( Support Q1) by A10, A11, A15, POLYNOM1:def 4;

            then x in Y by A11, A12, A13, A16;

            hence thesis by A17, TARSKI:def 4;

          end;

          let x be object;

          assume x in ( union A);

          then

          consider Y be set such that

           A18: x in Y and

           A19: Y in A by TARSKI:def 4;

          consider b1 be Element of ( Bags o1) such that

           A20: Y = { (b1 +^ b2) where b2 be Element of ( Bags o2) : ex Q be Polynomial of o2, L st Q = (P . b1) & b2 in ( Support Q) } and b1 in ( Support P) by A19;

          consider b2 be Element of ( Bags o2) such that

           A21: x = (b1 +^ b2) and

           A22: ex Q be Polynomial of o2, L st Q = (P . b1) & b2 in ( Support Q) by A18, A20;

          consider Q be Polynomial of o2, L such that

           A23: Q = (P . b1) and

           A24: b2 in ( Support Q) by A22;

          

           A25: (Q . b2) <> ( 0. L) by A24, POLYNOM1:def 4;

          consider b19 be Element of ( Bags o1), b29 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

           A26: Q1 = (P . b19) and

           A27: (b1 +^ b2) = (b19 +^ b29) and

           A28: (f . (b1 +^ b2)) = (Q1 . b29) by A7;

          

           A29: (f . (b1 +^ b2)) = (Q1 . b2) by A27, A28, Th7;

          Q1 = Q by A23, A26, A27, Th7;

          hence thesis by A21, A25, A29, POLYNOM1:def 4;

        end;

        

         A30: ( Support P) is finite by POLYNOM1:def 5;

        A is finite from FRAENKEL:sch 21( A30);

        then ( union A) is finite by A1, FINSET_1: 7;

        then

        reconsider f as Polynomial of (o1 +^ o2), L by A8, POLYNOM1:def 5;

        take f;

        let b be Element of ( Bags (o1 +^ o2));

        consider b19 be Element of ( Bags o1), b29 be Element of ( Bags o2), Q19 be Polynomial of o2, L such that

         A31: Q19 = (P . b19) and

         A32: b = (b19 +^ b29) and

         A33: (f . b) = (Q19 . b29) by A7;

        consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) such that

         A34: b = (b1 +^ b2) by Th6;

        reconsider Q1 = (P . b1) as Polynomial of o2, L by POLYNOM1:def 11;

        take b1, b2;

        take Q1;

        thus Q1 = (P . b1);

        thus b = (b1 +^ b2) by A34;

        b1 = b19 by A34, A32, Th7;

        hence thesis by A34, A31, A32, A33, Th7;

      end;

      uniqueness

      proof

        let w1,w2 be Polynomial of (o1 +^ o2), L such that

         A35: for b be Element of ( Bags (o1 +^ o2)) holds ex b1 be Element of ( Bags o1), b2 be Element of ( Bags o2), Q1 be Polynomial of o2, L st Q1 = (P . b1) & b = (b1 +^ b2) & (w1 . b) = (Q1 . b2) and

         A36: for b be Element of ( Bags (o1 +^ o2)) holds ex b1 be Element of ( Bags o1), b2 be Element of ( Bags o2), Q1 be Polynomial of o2, L st Q1 = (P . b1) & b = (b1 +^ b2) & (w2 . b) = (Q1 . b2);

        for c be Element of ( Bags (o1 +^ o2)) holds (w1 . c) = (w2 . c)

        proof

          let c be Element of ( Bags (o1 +^ o2));

          consider c1 be Element of ( Bags o1), c2 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

           A37: Q1 = (P . c1) and

           A38: c = (c1 +^ c2) and

           A39: (w1 . c) = (Q1 . c2) by A35;

          consider d1 be Element of ( Bags o1), d2 be Element of ( Bags o2), S1 be Polynomial of o2, L such that

           A40: S1 = (P . d1) and

           A41: c = (d1 +^ d2) and

           A42: (w2 . c) = (S1 . d2) by A36;

          c2 = d2 by A38, A41, Th7;

          hence thesis by A37, A38, A39, A40, A41, A42, Th7;

        end;

        hence w1 = w2 by FUNCT_2: 63;

      end;

    end

    theorem :: POLYNOM6:9

    

     Th9: for b1,c1 be Element of ( Bags o1), b2,c2 be Element of ( Bags o2) st b1 divides c1 & b2 divides c2 holds (b1 +^ b2) divides (c1 +^ c2)

    proof

      let b1,c1 be Element of ( Bags o1), b2,c2 be Element of ( Bags o2);

      assume that

       A1: b1 divides c1 and

       A2: b2 divides c2;

      now

        reconsider b19 = b1, c19 = c1 as bag of o1;

        let k be object;

        

         A3: (b19 . k) <= (c19 . k) by A1, PRE_POLY:def 11;

        assume

         A4: k in (o1 +^ o2);

        per cases by A4, XBOOLE_0:def 5;

          suppose

           A5: k in o1;

          then

          reconsider k9 = k as Ordinal;

          ((b1 +^ b2) . k9) = (b1 . k9) by A5, Def1;

          hence ((b1 +^ b2) . k) <= ((c1 +^ c2) . k) by A3, A5, Def1;

        end;

          suppose

           A6: k in ((o1 +^ o2) \ o1);

          then

          reconsider k9 = k as Ordinal;

          ((b1 +^ b2) . k9) = (b2 . (k9 -^ o1)) & ((c1 +^ c2) . k9) = (c2 . (k9 -^ o1)) by A6, Def1;

          hence ((b1 +^ b2) . k) <= ((c1 +^ c2) . k) by A2, PRE_POLY:def 11;

        end;

      end;

      hence thesis by PRE_POLY: 46;

    end;

    theorem :: POLYNOM6:10

    

     Th10: for b be bag of (o1 +^ o2), b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) st b divides (b1 +^ b2) holds ex c1 be Element of ( Bags o1), c2 be Element of ( Bags o2) st c1 divides b1 & c2 divides b2 & b = (c1 +^ c2)

    proof

      let b be bag of (o1 +^ o2), b1 be Element of ( Bags o1), b2 be Element of ( Bags o2);

      reconsider b9 = b as Element of ( Bags (o1 +^ o2)) by PRE_POLY:def 12;

      consider c1 be Element of ( Bags o1), c2 be Element of ( Bags o2) such that

       A1: b9 = (c1 +^ c2) by Th6;

      reconsider c19 = c1, b19 = b1 as bag of o1;

      reconsider c29 = c2, b29 = b2 as bag of o2;

      assume

       A2: b divides (b1 +^ b2);

      

       A3: for k be object st k in o2 holds (c29 . k) <= (b29 . k)

      proof

        let k be object;

        assume

         A4: k in o2;

        then

        reconsider k9 = k as Ordinal;

        set x = (o1 +^ k9);

        o1 c= (o1 +^ k9) by ORDINAL3: 24;

        then

         A5: not (o1 +^ k9) in o1 by ORDINAL1: 5;

        

         A6: ((c1 +^ c2) . x) <= ((b1 +^ b2) . x) & k9 = ((o1 +^ k9) -^ o1) by A2, A1, ORDINAL3: 52, PRE_POLY:def 11;

        (o1 +^ k9) in (o1 +^ o2) by A4, ORDINAL2: 32;

        then

         A7: (o1 +^ k9) in ((o1 +^ o2) \ o1) by A5, XBOOLE_0:def 5;

        then ((b1 +^ b2) . (o1 +^ k9)) = (b2 . ((o1 +^ k9) -^ o1)) by Def1;

        hence thesis by A7, A6, Def1;

      end;

      take c1, c2;

      for k be object st k in o1 holds (c19 . k) <= (b19 . k)

      proof

        let k be object;

        assume

         A8: k in o1;

        then

        reconsider k9 = k as Ordinal;

        

         A9: ((c1 +^ c2) . k) <= ((b1 +^ b2) . k) by A2, A1, PRE_POLY:def 11;

        ((c1 +^ c2) . k9) = (c1 . k9) by A8, Def1;

        hence thesis by A8, A9, Def1;

      end;

      hence thesis by A1, A3, PRE_POLY: 46;

    end;

    theorem :: POLYNOM6:11

    

     Th11: for a1,b1 be Element of ( Bags o1), a2,b2 be Element of ( Bags o2) holds (a1 +^ a2) < (b1 +^ b2) iff a1 < b1 or a1 = b1 & a2 < b2

    proof

      let a1,b1 be Element of ( Bags o1), a2,b2 be Element of ( Bags o2);

      thus (a1 +^ a2) < (b1 +^ b2) implies a1 < b1 or a1 = b1 & a2 < b2

      proof

        assume (a1 +^ a2) < (b1 +^ b2);

        then

        consider k be Ordinal such that

         A1: ((a1 +^ a2) . k) < ((b1 +^ b2) . k) and

         A2: for l be Ordinal st l in k holds ((a1 +^ a2) . l) = ((b1 +^ b2) . l) by PRE_POLY:def 9;

        now

          assume not k in ( dom (b1 +^ b2));

          then ((b1 +^ b2) . k) = 0 by FUNCT_1:def 2;

          hence contradiction by A1, NAT_1: 2;

        end;

        then

         A3: k in (o1 +^ o2) by PARTFUN1:def 2;

        now

          per cases by A3, XBOOLE_0:def 5;

            case

             A4: k in o1;

            reconsider a19 = a1, b19 = b1 as bag of o1;

            

             A5: for l be Ordinal st l in k holds (a19 . l) = (b19 . l)

            proof

              let l be Ordinal;

              assume

               A6: l in k;

              then

               A7: ((a1 +^ a2) . l) = ((b1 +^ b2) . l) by A2;

              

               A8: l in o1 by A4, A6, ORDINAL1: 10;

              then ((a1 +^ a2) . l) = (a1 . l) by Def1;

              hence thesis by A7, A8, Def1;

            end;

            ((a1 +^ a2) . k) = (a1 . k) by A4, Def1;

            then (a1 . k) < (b1 . k) by A1, A4, Def1;

            hence a1 < b1 by A5, PRE_POLY:def 9;

          end;

            case

             A9: k in ((o1 +^ o2) \ o1);

            set k1 = (k -^ o1);

             not k in o1 by A9, XBOOLE_0:def 5;

            then o1 c= k by ORDINAL1: 16;

            then

             A10: k = (o1 +^ (k -^ o1)) by ORDINAL3:def 5;

            

             A11: for l be Ordinal st l in k1 holds (a2 . l) = (b2 . l)

            proof

              let l be Ordinal;

              o1 c= (o1 +^ l) by ORDINAL3: 24;

              then

               A12: not (o1 +^ l) in o1 by ORDINAL1: 5;

              assume

               A13: l in k1;

              then (o1 +^ l) in (o1 +^ k1) by ORDINAL2: 32;

              then (o1 +^ l) in (o1 +^ o2) by A9, A10, ORDINAL1: 10;

              then

               A14: (o1 +^ l) in ((o1 +^ o2) \ o1) by A12, XBOOLE_0:def 5;

              

              then

               A15: ((b1 +^ b2) . (o1 +^ l)) = (b2 . ((o1 +^ l) -^ o1)) by Def1

              .= (b2 . l) by ORDINAL3: 52;

              ((a1 +^ a2) . (o1 +^ l)) = (a2 . ((o1 +^ l) -^ o1)) by A14, Def1

              .= (a2 . l) by ORDINAL3: 52;

              hence thesis by A2, A10, A13, A15, ORDINAL2: 32;

            end;

            for i be object st i in o1 holds (a1 . i) = (b1 . i)

            proof

               not k in o1 by A9, XBOOLE_0:def 5;

              then

               A16: o1 c= k by ORDINAL1: 16;

              let i be object;

              assume

               A17: i in o1;

              then

              reconsider i9 = i as Ordinal;

              ((a1 +^ a2) . i9) = (a1 . i9) & ((b1 +^ b2) . i9) = (b1 . i9) by A17, Def1;

              hence thesis by A2, A17, A16;

            end;

            hence a1 = b1 by PBOOLE: 3;

            ((a1 +^ a2) . k) = (a2 . (k -^ o1)) by A9, Def1;

            then (a2 . k1) < (b2 . k1) by A1, A9, Def1;

            hence a2 < b2 by A11, PRE_POLY:def 9;

          end;

        end;

        hence thesis;

      end;

      thus a1 < b1 or a1 = b1 & a2 < b2 implies (a1 +^ a2) < (b1 +^ b2)

      proof

        assume

         A18: a1 < b1 or a1 = b1 & a2 < b2;

        now

          per cases ;

            case a1 < b1;

            then

            consider k be Ordinal such that

             A19: k in o1 and

             A20: (a1 . k) < (b1 . k) and

             A21: for l be Ordinal st l in k holds (a1 . l) = (b1 . l) by Th2;

            

             A22: for l be Ordinal st l in k holds ((a1 +^ a2) . l) = ((b1 +^ b2) . l)

            proof

              let l be Ordinal;

              assume

               A23: l in k;

              then l in o1 by A19, ORDINAL1: 10;

              then ((a1 +^ a2) . l) = (a1 . l) & ((b1 +^ b2) . l) = (b1 . l) by Def1;

              hence thesis by A21, A23;

            end;

            ((a1 +^ a2) . k) = (a1 . k) & ((b1 +^ b2) . k) = (b1 . k) by A19, Def1;

            hence thesis by A20, A22, PRE_POLY:def 9;

          end;

            case

             A24: not a1 < b1;

            then

            consider k be Ordinal such that

             A25: k in o2 and

             A26: (a2 . k) < (b2 . k) and

             A27: for l be Ordinal st l in k holds (a2 . l) = (b2 . l) by A18, Th2;

            set x = (o1 +^ k);

            

             A28: for l be Ordinal st l in x holds ((a1 +^ a2) . l) = ((b1 +^ b2) . l)

            proof

              let l be Ordinal;

              assume

               A29: l in x;

              per cases ;

                suppose

                 A30: l in o1;

                

                hence ((a1 +^ a2) . l) = (b1 . l) by A18, A24, Def1

                .= ((b1 +^ b2) . l) by A30, Def1;

              end;

                suppose

                 A31: not l in o1;

                then o1 c= l by ORDINAL1: 16;

                then (l -^ o1) in ((o1 +^ k) -^ o1) by A29, ORDINAL3: 53;

                then

                 A32: (l -^ o1) in k by ORDINAL3: 52;

                (o1 +^ k) in (o1 +^ o2) by A25, ORDINAL2: 32;

                then l in (o1 +^ o2) by A29, ORDINAL1: 10;

                then

                 A33: l in ((o1 +^ o2) \ o1) by A31, XBOOLE_0:def 5;

                

                hence ((a1 +^ a2) . l) = (a2 . (l -^ o1)) by Def1

                .= (b2 . (l -^ o1)) by A27, A32

                .= ((b1 +^ b2) . l) by A33, Def1;

              end;

            end;

            o1 c= (o1 +^ k) by ORDINAL3: 24;

            then

             A34: not (o1 +^ k) in o1 by ORDINAL1: 5;

            

             A35: k = ((o1 +^ k) -^ o1) by ORDINAL3: 52;

            (o1 +^ k) in (o1 +^ o2) by A25, ORDINAL2: 32;

            then

             A36: (o1 +^ k) in ((o1 +^ o2) \ o1) by A34, XBOOLE_0:def 5;

            then ((b1 +^ b2) . (o1 +^ k)) = (b2 . ((o1 +^ k) -^ o1)) by Def1;

            then ((a1 +^ a2) . x) < ((b1 +^ b2) . x) by A26, A36, A35, Def1;

            hence thesis by A28, PRE_POLY:def 9;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: POLYNOM6:12

    

     Th12: for b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) holds for G be FinSequence of (( Bags (o1 +^ o2)) * ) st ( dom G) = ( dom ( divisors b1)) & for i be Nat st i in ( dom ( divisors b1)) holds ex a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) st Fk = (G /. i) & (( divisors b1) /. i) = a19 & ( len Fk) = ( len ( divisors b2)) & for m be Nat st m in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. m) = a199 & (Fk /. m) = (a19 +^ a199) holds ( divisors (b1 +^ b2)) = ( FlattenSeq G)

    proof

      let b1 be Element of ( Bags o1), b2 be Element of ( Bags o2);

      let G be FinSequence of (( Bags (o1 +^ o2)) * ) such that

       A1: ( dom G) = ( dom ( divisors b1)) and

       A2: for i be Nat st i in ( dom ( divisors b1)) holds ex a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) st Fk = (G /. i) & (( divisors b1) /. i) = a19 & ( len Fk) = ( len ( divisors b2)) & for m be Nat st m in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. m) = a199 & (Fk /. m) = (a19 +^ a199);

      reconsider D = ( Del (G,1)) as FinSequence of (( Bags (o1 +^ o2)) * );

      consider a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) such that

       A3: Fk = (G /. 1) and (( divisors b1) /. 1) = a19 and

       A4: ( len Fk) = ( len ( divisors b2)) and for m be Nat st m in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. m) = a199 & (Fk /. m) = (a19 +^ a199) by A2, FINSEQ_5: 6;

      ( len ( divisors b1)) <> 0 ;

      then ( len G) <> 0 by A1, FINSEQ_3: 29;

      then

       A5: G is non empty;

      then

       A6: 1 in ( dom G) by FINSEQ_5: 6;

      then

      reconsider G1 = (G . 1) as Element of (( Bags (o1 +^ o2)) * ) by A3, PARTFUN1:def 6;

      G = ( <*(G . 1)*> ^ ( Del (G,1))) by A5, FINSEQ_5: 86;

      

      then

       A7: ( FlattenSeq G) = (( FlattenSeq <*G1*>) ^ ( FlattenSeq D)) by PRE_POLY: 3

      .= (G1 ^ ( FlattenSeq D)) by PRE_POLY: 1;

      set F = ( FlattenSeq G);

      

       A8: 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 ( BagOrder (o1 +^ o2))

      proof

        let n,m be Nat such that

         A9: n in ( dom F) and

         A10: m in ( dom F) and

         A11: n < m;

        

         A12: (F /. n) = (F . n) by A9, PARTFUN1:def 6;

        consider i1,j1 be Nat such that

         A13: i1 in ( dom G) and

         A14: j1 in ( dom (G . i1)) and

         A15: n = (( Sum ( Card (G | (i1 -' 1)))) + j1) and

         A16: ((G . i1) . j1) = (( FlattenSeq G) . n) by A9, PRE_POLY: 29;

        consider a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) such that

         A17: Fk = (G /. i1) and

         A18: (( divisors b1) /. i1) = a19 and

         A19: ( len Fk) = ( len ( divisors b2)) and

         A20: for r be Nat st r in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. r) = a199 & (Fk /. r) = (a19 +^ a199) by A1, A2, A13;

        

         A21: j1 in ( dom Fk) by A13, A14, A17, PARTFUN1:def 6;

        then

        consider a199 be Element of ( Bags o2) such that

         A22: (( divisors b2) /. j1) = a199 and

         A23: (Fk /. j1) = (a19 +^ a199) by A20;

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

        then

         A24: j1 in ( dom ( divisors b2)) by A19, A21, FINSEQ_1:def 3;

        now

          consider i2,j2 be Nat such that

           A25: i2 in ( dom G) and

           A26: j2 in ( dom (G . i2)) and

           A27: m = (( Sum ( Card (G | (i2 -' 1)))) + j2) and

           A28: ((G . i2) . j2) = (( FlattenSeq G) . m) by A10, PRE_POLY: 29;

          consider a29 be Element of ( Bags o1), Fk9 be FinSequence of ( Bags (o1 +^ o2)) such that

           A29: Fk9 = (G /. i2) and

           A30: (( divisors b1) /. i2) = a29 and

           A31: ( len Fk9) = ( len ( divisors b2)) and

           A32: for r be Nat st r in ( dom Fk9) holds ex a299 be Element of ( Bags o2) st (( divisors b2) /. r) = a299 & (Fk9 /. r) = (a29 +^ a299) by A1, A2, A25;

          

           A33: (( divisors b1) . i2) = a29 by A1, A25, A30, PARTFUN1:def 6;

          Fk9 = (G . i2) by A25, A29, PARTFUN1:def 6;

          then

           A34: (( FlattenSeq G) . m) = (Fk9 /. j2) by A26, A28, PARTFUN1:def 6;

          

           A35: j2 in ( dom Fk9) by A25, A26, A29, PARTFUN1:def 6;

          then

          consider a299 be Element of ( Bags o2) such that

           A36: (( divisors b2) /. j2) = a299 and

           A37: (Fk9 /. j2) = (a29 +^ a299) by A32;

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

          then

           A38: j2 in ( dom ( divisors b2)) by A31, A35, FINSEQ_1:def 3;

          then

           A39: (( divisors b2) . j2) = a299 by A36, PARTFUN1:def 6;

          consider i1,j1 be Nat such that

           A40: i1 in ( dom G) and

           A41: j1 in ( dom (G . i1)) and

           A42: n = (( Sum ( Card (G | (i1 -' 1)))) + j1) and

           A43: ((G . i1) . j1) = (( FlattenSeq G) . n) by A9, PRE_POLY: 29;

          consider a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) such that

           A44: Fk = (G /. i1) and

           A45: (( divisors b1) /. i1) = a19 and

           A46: ( len Fk) = ( len ( divisors b2)) and

           A47: for r be Nat st r in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. r) = a199 & (Fk /. r) = (a19 +^ a199) by A1, A2, A40;

          

           A48: (( divisors b1) . i1) = a19 by A1, A40, A45, PARTFUN1:def 6;

          Fk = (G . i1) by A40, A44, PARTFUN1:def 6;

          then

           A49: (( FlattenSeq G) . n) = (Fk /. j1) by A41, A43, PARTFUN1:def 6;

          

           A50: j1 in ( dom Fk) by A40, A41, A44, PARTFUN1:def 6;

          then

          consider a199 be Element of ( Bags o2) such that

           A51: (( divisors b2) /. j1) = a199 and

           A52: (Fk /. j1) = (a19 +^ a199) by A47;

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

          then

           A53: j1 in ( dom ( divisors b2)) by A46, A50, FINSEQ_1:def 3;

          then

           A54: (( divisors b2) . j1) = a199 by A51, PARTFUN1:def 6;

          assume

           A55: (F /. n) = (F /. m);

          

           A56: (F /. n) = (F . n) & (F /. m) = (F . m) by A9, A10, PARTFUN1:def 6;

          then a19 = a29 by A55, A52, A37, A49, A34, Th7;

          then

           A57: i1 = i2 by A1, A40, A25, A48, A33, FUNCT_1:def 4;

          a199 = a299 by A55, A56, A52, A37, A49, A34, Th7;

          hence contradiction by A11, A42, A27, A57, A53, A54, A38, A39, FUNCT_1:def 4;

        end;

        hence (F /. n) <> (F /. m);

        reconsider Fn = (F /. n), Fm = (F /. m) as bag of (o1 +^ o2);

        reconsider Fn9 = Fn, Fm9 = Fm as Element of ( Bags (o1 +^ o2));

        consider a1 be Element of ( Bags o1), a2 be Element of ( Bags o2) such that

         A58: Fn9 = (a1 +^ a2) by Th6;

        Fk = (G . i1) by A13, A17, PARTFUN1:def 6;

        then

         A59: Fn9 = (Fk /. j1) by A12, A14, A16, PARTFUN1:def 6;

        then

         A60: a19 = a1 by A58, A23, Th7;

        then

         A61: (( divisors b1) . i1) = a1 by A1, A13, A18, PARTFUN1:def 6;

        

         A62: a199 = a2 by A58, A23, A59, Th7;

        then

         A63: (( divisors b2) . j1) = a2 by A22, A24, PARTFUN1:def 6;

        

         A64: (F /. m) = (F . m) by A10, PARTFUN1:def 6;

        consider c1 be Element of ( Bags o1), c2 be Element of ( Bags o2) such that

         A65: Fm9 = (c1 +^ c2) by Th6;

        consider i2,j2 be Nat such that

         A66: i2 in ( dom G) and

         A67: j2 in ( dom (G . i2)) and

         A68: m = (( Sum ( Card (G | (i2 -' 1)))) + j2) and

         A69: ((G . i2) . j2) = (( FlattenSeq G) . m) by A10, PRE_POLY: 29;

        consider a29 be Element of ( Bags o1), Fk9 be FinSequence of ( Bags (o1 +^ o2)) such that

         A70: Fk9 = (G /. i2) and

         A71: (( divisors b1) /. i2) = a29 and

         A72: ( len Fk9) = ( len ( divisors b2)) and

         A73: for r be Nat st r in ( dom Fk9) holds ex a299 be Element of ( Bags o2) st (( divisors b2) /. r) = a299 & (Fk9 /. r) = (a29 +^ a299) by A1, A2, A66;

        

         A74: j2 in ( dom Fk9) by A66, A67, A70, PARTFUN1:def 6;

        then

        consider a299 be Element of ( Bags o2) such that

         A75: (( divisors b2) /. j2) = a299 and

         A76: (Fk9 /. j2) = (a29 +^ a299) by A73;

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

        then

         A77: j2 in ( dom ( divisors b2)) by A72, A74, FINSEQ_1:def 3;

        Fk9 = (G . i2) by A66, A70, PARTFUN1:def 6;

        then

         A78: Fm9 = (Fk9 /. j2) by A64, A67, A69, PARTFUN1:def 6;

        then

         A79: a29 = c1 by A65, A76, Th7;

        then

         A80: (( divisors b1) . i2) = c1 by A1, A66, A71, PARTFUN1:def 6;

        

         A81: a299 = c2 by A65, A76, A78, Th7;

        then

         A82: (( divisors b2) . j2) = c2 by A75, A77, PARTFUN1:def 6;

        now

           A83:

          now

            assume that

             A84: not i1 < i2 and

             A85: not (i1 = i2 & j1 < j2);

            per cases by A84, XXREAL_0: 1;

              suppose i1 = i2;

              hence contradiction by A11, A15, A68, A85, XREAL_1: 6;

            end;

              suppose

               A86: i1 > i2;

              i2 >= 1 by A66, FINSEQ_3: 25;

              then

               A87: (i2 -' 1) = (i2 - 1) by XREAL_1: 233;

              reconsider G1 = (G . i2) as Element of (( Bags (o1 +^ o2)) * ) by A66, A70, PARTFUN1:def 6;

              

               A88: ( Card (G | i2)) = (( Card G) | i2) & ( Card (G | (i1 -' 1))) = (( Card G) | (i1 -' 1)) by POLYNOM3: 16;

              reconsider GG1 = <*G1*> as FinSequence of (( Bags (o1 +^ o2)) * );

              i2 < (i2 + 1) by XREAL_1: 29;

              then

               A89: (i2 - 1) < i2 by XREAL_1: 19;

              i2 >= 1 by A66, FINSEQ_3: 25;

              then

               A90: ((i2 -' 1) + 1) = i2 by XREAL_1: 235;

              i2 <= ( len G) by A66, FINSEQ_3: 25;

              then (i2 -' 1) < ( len G) by A87, A89, XXREAL_0: 2;

              then (G | i2) = ((G | (i2 -' 1)) ^ GG1) by A90, FINSEQ_5: 83;

              then ( Card (G | i2)) = (( Card (G | (i2 -' 1))) ^ ( Card GG1)) by PRE_POLY: 25;

              then ( Card (G | i2)) = (( Card (G | (i2 -' 1))) ^ <*( card G1)*>) by PRE_POLY: 24;

              then

               A91: ( Sum ( Card (G | i2))) = (( Sum ( Card (G | (i2 -' 1)))) + ( card (G . i2))) by RVSUM_1: 74;

              j2 <= ( card (G . i2)) by A67, FINSEQ_3: 25;

              then

               A92: (( Sum ( Card (G | (i2 -' 1)))) + j2) <= ( Sum ( Card (G | i2))) by A91, XREAL_1: 6;

              i2 <= (i1 -' 1) by A86, NAT_D: 49;

              then ( Sum ( Card (G | i2))) <= ( Sum ( Card (G | (i1 -' 1)))) by A88, POLYNOM3: 18;

              then

               A93: (( Sum ( Card (G | (i2 -' 1)))) + j2) <= ( Sum ( Card (G | (i1 -' 1)))) by A92, XXREAL_0: 2;

              ( Sum ( Card (G | (i1 -' 1)))) <= (( Sum ( Card (G | (i1 -' 1)))) + j1) by NAT_1: 11;

              hence contradiction by A11, A15, A68, A93, XXREAL_0: 2;

            end;

          end;

          consider S be non empty finite Subset of ( Bags o1) such that

           A94: ( divisors b1) = ( SgmX (( BagOrder o1),S)) and for p be bag of o1 holds p in S iff p divides b1 by PRE_POLY:def 16;

          ( field ( BagOrder o1)) = ( Bags o1) by ORDERS_1: 15;

          then

           A95: ( BagOrder o1) linearly_orders S by ORDERS_1: 37, ORDERS_1: 38;

          consider T be non empty finite Subset of ( Bags o2) such that

           A96: ( divisors b2) = ( SgmX (( BagOrder o2),T)) and for p be bag of o2 holds p in T iff p divides b2 by PRE_POLY:def 16;

          ( field ( BagOrder o2)) = ( Bags o2) by ORDERS_1: 15;

          then

           A97: ( BagOrder o2) linearly_orders T by ORDERS_1: 37, ORDERS_1: 38;

          per cases by A83;

            case

             A98: i1 < i2;

            then [(( divisors b1) /. i1), (( divisors b1) /. i2)] in ( BagOrder o1) by A1, A13, A66, A94, A95, PRE_POLY:def 2;

            then

             A99: a1 <=' c1 by A18, A71, A60, A79, PRE_POLY:def 14;

            a1 <> c1 by A1, A13, A66, A61, A80, A98, FUNCT_1:def 4;

            hence a1 < c1 by A99, PRE_POLY:def 10;

          end;

            case that

             A100: i1 = i2 and

             A101: j1 < j2;

             [(( divisors b2) /. j1), (( divisors b2) /. j2)] in ( BagOrder o2) by A24, A77, A96, A97, A101, PRE_POLY:def 2;

            then

             A102: a2 <=' c2 by A22, A75, A62, A81, PRE_POLY:def 14;

            thus a1 = c1 by A65, A18, A71, A76, A78, A60, A100, Th7;

            a2 <> c2 by A24, A63, A77, A82, A101, FUNCT_1:def 4;

            hence a2 < c2 by A102, PRE_POLY:def 10;

          end;

        end;

        then Fn < Fm or Fn = Fm by A58, A65, Th11;

        then Fn <=' Fm by PRE_POLY:def 10;

        hence thesis by PRE_POLY:def 14;

      end;

      Fk = (G . 1) by A6, A3, PARTFUN1:def 6;

      then (G . 1) <> {} by A4;

      then

      reconsider S = ( rng ( FlattenSeq G)) as non empty finite Subset of ( Bags (o1 +^ o2)) by A7, FINSEQ_1:def 4, RELAT_1: 41;

      

       A103: for p be bag of (o1 +^ o2) holds p in S iff p divides (b1 +^ b2)

      proof

        consider W be non empty finite Subset of ( Bags o2) such that

         A104: ( divisors b2) = ( SgmX (( BagOrder o2),W)) and

         A105: for q be bag of o2 holds q in W iff q divides b2 by PRE_POLY:def 16;

        ( field ( BagOrder o2)) = ( Bags o2) by ORDERS_1: 15;

        then ( BagOrder o2) linearly_orders W by ORDERS_1: 37, ORDERS_1: 38;

        then

         A106: ( rng ( SgmX (( BagOrder o2),W))) = W by PRE_POLY:def 2;

        let p be bag of (o1 +^ o2);

        consider T be non empty finite Subset of ( Bags o1) such that

         A107: ( divisors b1) = ( SgmX (( BagOrder o1),T)) and

         A108: for q be bag of o1 holds q in T iff q divides b1 by PRE_POLY:def 16;

        ( field ( BagOrder o1)) = ( Bags o1) by ORDERS_1: 15;

        then ( BagOrder o1) linearly_orders T by ORDERS_1: 37, ORDERS_1: 38;

        then

         A109: ( rng ( SgmX (( BagOrder o1),T))) = T by PRE_POLY:def 2;

        thus p in S implies p divides (b1 +^ b2)

        proof

          assume p in S;

          then

          consider x be object such that

           A110: x in ( dom ( FlattenSeq G)) and

           A111: p = (( FlattenSeq G) . x) by FUNCT_1:def 3;

          consider i,j be Nat such that

           A112: i in ( dom G) and

           A113: j in ( dom (G . i)) and x = (( Sum ( Card (G | (i -' 1)))) + j) and

           A114: ((G . i) . j) = (( FlattenSeq G) . x) by A110, PRE_POLY: 29;

          consider a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) such that

           A115: Fk = (G /. i) and

           A116: (( divisors b1) /. i) = a19 and

           A117: ( len Fk) = ( len ( divisors b2)) and

           A118: for m be Nat st m in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. m) = a199 & (Fk /. m) = (a19 +^ a199) by A1, A2, A112;

          reconsider a119 = a19 as bag of o1;

          (( divisors b1) . i) = a19 by A1, A112, A116, PARTFUN1:def 6;

          then a19 in T by A1, A107, A109, A112, FUNCT_1: 3;

          then

           A119: a119 divides b1 by A108;

          

           A120: Fk = (G . i) by A112, A115, PARTFUN1:def 6;

          then

          consider a199 be Element of ( Bags o2) such that

           A121: (( divisors b2) /. j) = a199 and

           A122: (Fk /. j) = (a19 +^ a199) by A113, A118;

          reconsider a1199 = a199 as bag of o2;

          j in ( Seg ( len Fk)) by A113, A120, FINSEQ_1:def 3;

          then

           A123: j in ( dom ( divisors b2)) by A117, FINSEQ_1:def 3;

          then (( divisors b2) . j) = a199 by A121, PARTFUN1:def 6;

          then a199 in W by A104, A106, A123, FUNCT_1: 3;

          then

           A124: a1199 divides b2 by A105;

          p = (a19 +^ a199) by A111, A113, A114, A120, A122, PARTFUN1:def 6;

          hence thesis by A119, A124, Th9;

        end;

        thus p divides (b1 +^ b2) implies p in S

        proof

          assume p divides (b1 +^ b2);

          then

          consider p1 be Element of ( Bags o1), p2 be Element of ( Bags o2) such that

           A125: p1 divides b1 and

           A126: p2 divides b2 and

           A127: p = (p1 +^ p2) by Th10;

          p1 in T by A108, A125;

          then

          consider i be object such that

           A128: i in ( dom ( divisors b1)) and

           A129: p1 = (( divisors b1) . i) by A107, A109, FUNCT_1:def 3;

          reconsider i as Element of NAT by A128;

          consider a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) such that

           A130: Fk = (G /. i) and

           A131: (( divisors b1) /. i) = a19 and

           A132: ( len Fk) = ( len ( divisors b2)) and

           A133: for m be Nat st m in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. m) = a199 & (Fk /. m) = (a19 +^ a199) by A2, A128;

          

           A134: a19 = p1 by A128, A129, A131, PARTFUN1:def 6;

          p2 in ( rng ( divisors b2)) by A104, A105, A106, A126;

          then

          consider j be object such that

           A135: j in ( dom ( divisors b2)) and

           A136: p2 = (( divisors b2) . j) by FUNCT_1:def 3;

          

           A137: j in ( Seg ( len ( divisors b2))) by A135, FINSEQ_1:def 3;

          ( Seg ( len (G . i))) = ( Seg ( len ( divisors b2))) by A1, A128, A130, A132, PARTFUN1:def 6;

          then

           A138: j in ( dom (G . i)) by A137, FINSEQ_1:def 3;

          reconsider j as Element of NAT by A135;

          

           A139: (G /. i) = (G . i) by A1, A128, PARTFUN1:def 6;

          then

          consider a199 be Element of ( Bags o2) such that

           A140: (( divisors b2) /. j) = a199 and

           A141: (Fk /. j) = (a19 +^ a199) by A130, A133, A138;

          

           A142: a199 = p2 by A135, A136, A140, PARTFUN1:def 6;

          

           A143: (( Sum ( Card (G | (i -' 1)))) + j) in ( dom ( FlattenSeq G)) & ((G . i) . j) = (( FlattenSeq G) . (( Sum ( Card (G | (i -' 1)))) + j)) by A1, A128, A138, PRE_POLY: 30;

          ((G . i) . j) = (a19 +^ a199) by A130, A138, A139, A141, PARTFUN1:def 6;

          hence thesis by A127, A143, A134, A142, FUNCT_1:def 3;

        end;

      end;

      ( field ( BagOrder (o1 +^ o2))) = ( Bags (o1 +^ o2)) by ORDERS_1: 15;

      then ( BagOrder (o1 +^ o2)) linearly_orders S by ORDERS_1: 37, ORDERS_1: 38;

      then ( FlattenSeq G) = ( SgmX (( BagOrder (o1 +^ o2)),S)) by A8, PRE_POLY:def 2;

      hence thesis by A103, PRE_POLY:def 16;

    end;

    theorem :: POLYNOM6:13

    

     Th13: for a1,b1,c1 be Element of ( Bags o1), a2,b2,c2 be Element of ( Bags o2) st c1 = (b1 -' a1) & c2 = (b2 -' a2) holds ((b1 +^ b2) -' (a1 +^ a2)) = (c1 +^ c2)

    proof

      let a1,b1,c1 be Element of ( Bags o1), a2,b2,c2 be Element of ( Bags o2);

      assume that

       A1: c1 = (b1 -' a1) and

       A2: c2 = (b2 -' a2);

      reconsider w = ((b1 +^ b2) -' (a1 +^ a2)) as Element of ( Bags (o1 +^ o2)) by PRE_POLY:def 12;

      for o be Ordinal holds (o in o1 implies (w . o) = (c1 . o)) & (o in ((o1 +^ o2) \ o1) implies (w . o) = (c2 . (o -^ o1)))

      proof

        let o be Ordinal;

        hereby

          assume

           A3: o in o1;

          

          thus (w . o) = (((b1 +^ b2) . o) -' ((a1 +^ a2) . o)) by PRE_POLY:def 6

          .= ((b1 . o) -' ((a1 +^ a2) . o)) by A3, Def1

          .= ((b1 . o) -' (a1 . o)) by A3, Def1

          .= (c1 . o) by A1, PRE_POLY:def 6;

        end;

        assume

         A4: o in ((o1 +^ o2) \ o1);

        

        thus (w . o) = (((b1 +^ b2) . o) -' ((a1 +^ a2) . o)) by PRE_POLY:def 6

        .= ((b2 . (o -^ o1)) -' ((a1 +^ a2) . o)) by A4, Def1

        .= ((b2 . (o -^ o1)) -' (a2 . (o -^ o1))) by A4, Def1

        .= (c2 . (o -^ o1)) by A2, PRE_POLY:def 6;

      end;

      hence thesis by Def1;

    end;

    theorem :: POLYNOM6:14

    

     Th14: for b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) holds for G be FinSequence of ((2 -tuples_on ( Bags (o1 +^ o2))) * ) st ( dom G) = ( dom ( decomp b1)) & for i be Nat st i in ( dom ( decomp b1)) holds ex a19,b19 be Element of ( Bags o1), Fk be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) st Fk = (G /. i) & (( decomp b1) /. i) = <*a19, b19*> & ( len Fk) = ( len ( decomp b2)) & for m be Nat st m in ( dom Fk) holds ex a199,b199 be Element of ( Bags o2) st (( decomp b2) /. m) = <*a199, b199*> & (Fk /. m) = <*(a19 +^ a199), (b19 +^ b199)*> holds ( decomp (b1 +^ b2)) = ( FlattenSeq G)

    proof

      let b1 be Element of ( Bags o1), b2 be Element of ( Bags o2);

      let G be FinSequence of ((2 -tuples_on ( Bags (o1 +^ o2))) * ) such that

       A1: ( dom G) = ( dom ( decomp b1)) and

       A2: for i be Nat st i in ( dom ( decomp b1)) holds ex a19,b19 be Element of ( Bags o1), Fk be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) st Fk = (G /. i) & (( decomp b1) /. i) = <*a19, b19*> & ( len Fk) = ( len ( decomp b2)) & for m be Nat st m in ( dom Fk) holds ex a199,b199 be Element of ( Bags o2) st (( decomp b2) /. m) = <*a199, b199*> & (Fk /. m) = <*(a19 +^ a199), (b19 +^ b199)*>;

      defpred P[ set, Function] means ( dom $2) = ( dom (G . $1)) & for j be Nat st j in ( dom $2) holds ex p be Element of (2 -tuples_on ( Bags (o1 +^ o2))) st p = ((G . $1) . j) & ($2 . j) = (p . 1);

      

       A3: for k be Nat st k in ( Seg ( len G)) holds ex p be Element of (( Bags (o1 +^ o2)) * ) st P[k, p]

      proof

        let k be Nat such that

         A4: k in ( Seg ( len G));

        defpred Q[ set, set] means ex q be Element of (2 -tuples_on ( Bags (o1 +^ o2))) st q = ((G . k) . $1) & $2 = (q . 1);

        

         A5: for j be Nat st j in ( Seg ( len (G . k))) holds ex x be Element of ( Bags (o1 +^ o2)) st Q[j, x]

        proof

          k in ( dom G) by A4, FINSEQ_1:def 3;

          then

           A6: (G . k) in ( rng G) by FUNCT_1: 3;

          ( rng G) c= ((2 -tuples_on ( Bags (o1 +^ o2))) * ) by FINSEQ_1:def 4;

          then (G . k) is Element of ((2 -tuples_on ( Bags (o1 +^ o2))) * ) by A6;

          then

          reconsider Gk = (G . k) as FinSequence of (2 -tuples_on ( Bags (o1 +^ o2)));

          let j be Nat;

          assume j in ( Seg ( len (G . k)));

          then j in ( dom (G . k)) by FINSEQ_1:def 3;

          then ((G . k) . j) = (Gk /. j) by PARTFUN1:def 6;

          then

          reconsider q = ((G . k) . j) as Element of (2 -tuples_on ( Bags (o1 +^ o2)));

          ex q1,q2 be Element of ( Bags (o1 +^ o2)) st q = <*q1, q2*> by FINSEQ_2: 100;

          then

          reconsider x = (q . 1) as Element of ( Bags (o1 +^ o2)) by FINSEQ_1: 44;

          take x;

          thus thesis;

        end;

        consider p be FinSequence of ( Bags (o1 +^ o2)) such that

         A7: ( dom p) = ( Seg ( len (G . k))) and

         A8: for j be Nat st j in ( Seg ( len (G . k))) holds Q[j, (p /. j)] from RECDEF_1:sch 17( A5);

        reconsider p as Element of (( Bags (o1 +^ o2)) * ) by FINSEQ_1:def 11;

        take p;

        thus ( dom p) = ( dom (G . k)) by A7, FINSEQ_1:def 3;

        let j be Nat;

        assume

         A9: j in ( dom p);

        then

        consider q be Element of (2 -tuples_on ( Bags (o1 +^ o2))) such that

         A10: q = ((G . k) . j) and

         A11: (p /. j) = (q . 1) by A7, A8;

        take q;

        thus q = ((G . k) . j) by A10;

        thus thesis by A9, A11, PARTFUN1:def 6;

      end;

      consider F be FinSequence of (( Bags (o1 +^ o2)) * ) such that

       A12: ( dom F) = ( Seg ( len G)) and

       A13: for i be Nat st i in ( Seg ( len G)) holds P[i, (F /. i)] from RECDEF_1:sch 17( A3);

      

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

      .= ( dom G) by A12, FINSEQ_1:def 3

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

      

       A15: ( dom ( divisors b1)) = ( dom ( decomp b1)) by PRE_POLY:def 17;

      

       A16: for i be Nat st i in ( dom ( divisors b1)) holds ex a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) st Fk = (F /. i) & (( divisors b1) /. i) = a19 & ( len Fk) = ( len ( divisors b2)) & for m be Nat st m in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. m) = a199 & (Fk /. m) = (a19 +^ a199)

      proof

        let i be Nat;

        reconsider Fk = (F /. i) as FinSequence of ( Bags (o1 +^ o2));

        

         A17: ( dom ( decomp b2)) = ( dom ( divisors b2)) by PRE_POLY:def 17;

        assume

         A18: i in ( dom ( divisors b1));

        then

        consider a19,b19 be Element of ( Bags o1), Gi be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) such that

         A19: Gi = (G /. i) and

         A20: (( decomp b1) /. i) = <*a19, b19*> and

         A21: ( len Gi) = ( len ( decomp b2)) and

         A22: for m be Nat st m in ( dom Gi) holds ex a199,b199 be Element of ( Bags o2) st (( decomp b2) /. m) = <*a199, b199*> & (Gi /. m) = <*(a19 +^ a199), (b19 +^ b199)*> by A2, A15;

        take a19, Fk;

        thus Fk = (F /. i);

        thus (( divisors b1) /. i) = a19 by A15, A18, A20, PRE_POLY: 70;

        

         A23: i in ( Seg ( len G)) by A1, A15, A18, FINSEQ_1:def 3;

        then

         A24: ( dom (F /. i)) = ( dom (G . i)) by A13;

        

        hence ( len Fk) = ( len (G . i)) by FINSEQ_3: 29

        .= ( len ( decomp b2)) by A1, A15, A18, A19, A21, PARTFUN1:def 6

        .= ( len ( divisors b2)) by A17, FINSEQ_3: 29;

        let m be Nat;

        assume

         A25: m in ( dom Fk);

        then

        consider p be Element of (2 -tuples_on ( Bags (o1 +^ o2))) such that

         A26: p = ((G . i) . m) and

         A27: ((F /. i) . m) = (p . 1) by A13, A23;

        

         A28: (G . i) = (G /. i) by A1, A15, A18, PARTFUN1:def 6;

        then

        consider a199,b199 be Element of ( Bags o2) such that

         A29: (( decomp b2) /. m) = <*a199, b199*> and

         A30: (Gi /. m) = <*(a19 +^ a199), (b19 +^ b199)*> by A19, A22, A24, A25;

        

         A31: p = <*(a19 +^ a199), (b19 +^ b199)*> by A19, A24, A28, A25, A30, A26, PARTFUN1:def 6;

        take a199;

        m in ( dom ( decomp b2)) by A19, A21, A24, A28, A25, FINSEQ_3: 29;

        hence (( divisors b2) /. m) = a199 by A29, PRE_POLY: 70;

        

        thus (Fk /. m) = (Fk . m) by A25, PARTFUN1:def 6

        .= (a19 +^ a199) by A27, A31, FINSEQ_1: 44;

      end;

      ( dom ( decomp b2)) = ( dom ( divisors b2)) by PRE_POLY:def 17;

      then

       A32: ( len ( decomp b2)) = ( len ( divisors b2)) by FINSEQ_3: 29;

      

       A33: for j be Nat st j in ( dom ( Card F)) holds (( Card F) . j) = (( Card G) . j)

      proof

        let j be Nat;

        assume

         A34: j in ( dom ( Card F));

        then

         A35: j in ( dom G) by A14, CARD_3:def 2;

        

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

        then

         A37: (( Card F) . j) = ( card (F . j)) by A34, CARD_3:def 2;

        j in ( dom ( decomp b1)) by A1, A12, A34, A36, FINSEQ_1:def 3;

        then

         A38: (ex a19 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) st Fk = (F /. j) & (( divisors b1) /. j) = a19 & ( len Fk) = ( len ( divisors b2)) & for m be Nat st m in ( dom Fk) holds ex a199 be Element of ( Bags o2) st (( divisors b2) /. m) = a199 & (Fk /. m) = (a19 +^ a199)) & ex a29,b29 be Element of ( Bags o1), Gk be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) st Gk = (G /. j) & (( decomp b1) /. j) = <*a29, b29*> & ( len Gk) = ( len ( decomp b2)) & for m be Nat st m in ( dom Gk) holds ex a299,b299 be Element of ( Bags o2) st (( decomp b2) /. m) = <*a299, b299*> & (Gk /. m) = <*(a29 +^ a299), (b29 +^ b299)*> by A2, A15, A16;

        ( card (F . j)) = ( card (F /. j)) by A34, A36, PARTFUN1:def 6

        .= ( card (G . j)) by A32, A35, A38, PARTFUN1:def 6;

        hence thesis by A35, A37, CARD_3:def 2;

      end;

      reconsider bb = (b1 +^ b2) as bag of (o1 +^ o2);

      reconsider FG = ( FlattenSeq G) as FinSequence of (2 -tuples_on ( Bags (o1 +^ o2)));

      ( len ( Card F)) = ( len ( Card G)) by A14, FINSEQ_3: 29;

      then

       A39: ( Card F) = ( Card G) by A33, FINSEQ_2: 9;

      then

       A40: ( len FG) = ( len ( FlattenSeq F)) by PRE_POLY: 28;

      ( dom ( decomp b1)) = ( dom ( divisors b1)) by PRE_POLY:def 17;

      then ( dom F) = ( dom ( divisors b1)) by A1, A12, FINSEQ_1:def 3;

      then

       A41: ( divisors (b1 +^ b2)) = ( FlattenSeq F) by A16, Th12;

      

       A42: ( dom ( decomp b1)) = ( dom ( divisors b1)) by PRE_POLY:def 17;

      

       A43: for i be Element of NAT , p be bag of (o1 +^ o2) st i in ( dom FG) & p = (( divisors bb) /. i) holds (FG /. i) = <*p, (bb -' p)*>

      proof

        let k be Element of NAT , p be bag of (o1 +^ o2) such that

         A44: k in ( dom FG) and

         A45: p = (( divisors bb) /. k);

        consider i,j be Nat such that

         A46: i in ( dom G) and

         A47: j in ( dom (G . i)) and

         A48: k = (( Sum ( Card (G | (i -' 1)))) + j) and

         A49: ((G . i) . j) = (FG . k) by A44, PRE_POLY: 29;

        consider fa1 be Element of ( Bags o1), Fk be FinSequence of ( Bags (o1 +^ o2)) such that

         A50: Fk = (F /. i) and

         A51: (( divisors b1) /. i) = fa1 and ( len Fk) = ( len ( divisors b2)) and

         A52: for m be Nat st m in ( dom Fk) holds ex fa19 be Element of ( Bags o2) st (( divisors b2) /. m) = fa19 & (Fk /. m) = (fa1 +^ fa19) by A1, A16, A42, A46;

        consider a19,b19 be Element of ( Bags o1), Gi be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) such that

         A53: Gi = (G /. i) and

         A54: (( decomp b1) /. i) = <*a19, b19*> and

         A55: ( len Gi) = ( len ( decomp b2)) and

         A56: for m be Nat st m in ( dom Gi) holds ex a199,b199 be Element of ( Bags o2) st (( decomp b2) /. m) = <*a199, b199*> & (Gi /. m) = <*(a19 +^ a199), (b19 +^ b199)*> by A1, A2, A46;

        

         A57: a19 = fa1 by A1, A46, A54, A51, PRE_POLY: 70;

        then

         A58: <*a19, b19*> = <*a19, (b1 -' a19)*> by A1, A46, A54, A51, PRE_POLY:def 17;

        

         A59: j in ( dom Gi) by A46, A47, A53, PARTFUN1:def 6;

        then

        consider a199,b199 be Element of ( Bags o2) such that

         A60: (( decomp b2) /. j) = <*a199, b199*> and

         A61: (Gi /. j) = <*(a19 +^ a199), (b19 +^ b199)*> by A56;

        reconsider b2a1 = (b2 -' a199) as Element of ( Bags o2) by PRE_POLY:def 12;

        reconsider b1a1 = (b1 -' a19) as Element of ( Bags o1) by PRE_POLY:def 12;

        k in ( dom ( FlattenSeq F)) by A40, A44, FINSEQ_3: 29;

        then

        consider i9,j9 be Nat such that

         A62: i9 in ( dom F) and

         A63: j9 in ( dom (F . i9)) and

         A64: k = (( Sum ( Card (F | (i9 -' 1)))) + j9) and

         A65: ((F . i9) . j9) = (( FlattenSeq F) . k) by PRE_POLY: 29;

        

         A66: ( Card (G | (i -' 1))) = (( Card G) | (i -' 1)) & ( Card (F | (i9 -' 1))) = (( Card F) | (i9 -' 1)) by POLYNOM3: 16;

        then

         A67: i = i9 by A39, A46, A47, A48, A62, A63, A64, POLYNOM3: 22;

        

         A68: j = j9 by A39, A46, A47, A48, A62, A63, A64, A66, POLYNOM3: 22;

        then

         A69: j in ( dom Fk) by A62, A63, A67, A50, PARTFUN1:def 6;

        then

        consider fa19 be Element of ( Bags o2) such that

         A70: (( divisors b2) /. j) = fa19 and

         A71: (Fk /. j) = (fa1 +^ fa19) by A52;

        

         A72: j in ( dom ( decomp b2)) by A55, A59, FINSEQ_3: 29;

        then

         A73: a199 = fa19 by A60, A70, PRE_POLY: 70;

        then

         A74: <*a199, b199*> = <*a199, (b2 -' a199)*> by A60, A70, A72, PRE_POLY:def 17;

        k in ( dom ( FlattenSeq F)) by A40, A44, FINSEQ_3: 29;

        

        then

         A75: p = ((F . i) . j) by A41, A45, A65, A67, A68, PARTFUN1:def 6

        .= (Fk . j) by A62, A67, A50, PARTFUN1:def 6

        .= (a19 +^ a199) by A69, A71, A57, A73, PARTFUN1:def 6;

        

        then

         A76: (bb -' p) = (b1a1 +^ b2a1) by Th13

        .= (b19 +^ b2a1) by A58, FINSEQ_1: 77

        .= (b19 +^ b199) by A74, FINSEQ_1: 77;

        

        thus (FG /. k) = ((G . i) . j) by A44, A49, PARTFUN1:def 6

        .= (Gi . j) by A46, A53, PARTFUN1:def 6

        .= <*p, (bb -' p)*> by A59, A61, A75, A76, PARTFUN1:def 6;

      end;

      ( dom FG) = ( dom ( divisors bb)) by A41, A40, FINSEQ_3: 29;

      hence thesis by A43, PRE_POLY:def 17;

    end;

    theorem :: POLYNOM6:15

    for o1,o2 be non empty Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative well-unital non trivial doubleLoopStr holds (( Polynom-Ring (o1,( Polynom-Ring (o2,L)))),( Polynom-Ring ((o1 +^ o2),L))) are_isomorphic

    proof

      let o1,o2 be non empty Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative well-unital non trivial non empty doubleLoopStr;

      set P2 = ( Polynom-Ring ((o1 +^ o2),L)), P1 = ( Polynom-Ring (o1,( Polynom-Ring (o2,L))));

      defpred R[ set, set] means for P be Polynomial of o1, ( Polynom-Ring (o2,L)) st $1 = P holds $2 = ( Compress P);

      reconsider 1P1 = ( 1_ P1) as Polynomial of o1, ( Polynom-Ring (o2,L)) by POLYNOM1:def 11;

      reconsider 1P2 = ( 1_ P2) as Polynomial of (o1 +^ o2), L by POLYNOM1:def 11;

      

       A1: for x be Element of P1 holds ex u be Element of P2 st R[x, u]

      proof

        let x be Element of P1;

        reconsider Q = x as Polynomial of o1, ( Polynom-Ring (o2,L)) by POLYNOM1:def 11;

        reconsider u = ( Compress Q) as Element of P2 by POLYNOM1:def 11;

        take u;

        let P be Polynomial of o1, ( Polynom-Ring (o2,L));

        assume x = P;

        hence thesis;

      end;

      consider f be Function of the carrier of P1, the carrier of P2 such that

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

      reconsider f as Function of P1, P2;

      take f;

      thus f is additive

      proof

        let x,y be Element of P1;

        reconsider x9 = x, y9 = y as Element of P1;

        reconsider p = x9, q = y9 as Polynomial of o1, ( Polynom-Ring (o2,L)) by POLYNOM1:def 11;

        reconsider fp = (f . x), fq = (f . y), fpq = (f . (x + y)) as Element of P2;

        reconsider fp, fq, fpq as Polynomial of (o1 +^ o2), L by POLYNOM1:def 11;

        for x be bag of (o1 +^ o2) holds (fpq . x) = ((fp . x) + (fq . x))

        proof

          let b be bag of (o1 +^ o2);

          reconsider b9 = b as Element of ( Bags (o1 +^ o2)) by PRE_POLY:def 12;

          consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

           A3: Q1 = (p . b1) and

           A4: b9 = (b1 +^ b2) and

           A5: (( Compress p) . b9) = (Q1 . b2) by Def2;

          consider b19 be Element of ( Bags o1), b29 be Element of ( Bags o2), Q19 be Polynomial of o2, L such that

           A6: Q19 = (q . b19) and

           A7: b9 = (b19 +^ b29) and

           A8: (( Compress q) . b9) = (Q19 . b29) by Def2;

          consider b199 be Element of ( Bags o1), b299 be Element of ( Bags o2), Q199 be Polynomial of o2, L such that

           A9: Q199 = ((p + q) . b199) and

           A10: b9 = (b199 +^ b299) and

           A11: (( Compress (p + q)) . b9) = (Q199 . b299) by Def2;

          

           A12: b19 = b199 by A7, A10, Th7;

          reconsider b1 as bag of o1;

          

           A13: ((p + q) . b1) = ((p . b1) + (q . b1)) by POLYNOM1: 15;

          b1 = b19 by A4, A7, Th7;

          then Q199 = (Q1 + Q19) by A3, A6, A9, A12, A13, POLYNOM1:def 11;

          then

           A14: (Q199 . b2) = ((Q1 . b2) + (Q19 . b2)) by POLYNOM1: 15;

          

           A15: b29 = b299 by A7, A10, Th7;

          

           A16: b2 = b29 by A4, A7, Th7;

          (x + y) = (p + q) by POLYNOM1:def 11;

          

          hence (fpq . b) = (( Compress (p + q)) . b9) by A2

          .= ((( Compress p) . b9) + (fq . b)) by A2, A5, A8, A11, A16, A15, A14

          .= ((fp . b) + (fq . b)) by A2;

        end;

        

        hence (f . (x + y)) = (fp + fq) by POLYNOM1: 16

        .= ((f . x) + (f . y)) by POLYNOM1:def 11;

      end;

      now

        let x,y be Element of P1;

        reconsider x9 = x, y9 = y as Element of P1;

        reconsider p = x9, q = y9 as Polynomial of o1, ( Polynom-Ring (o2,L)) by POLYNOM1:def 11;

        reconsider fp = (f . x), fq = (f . y) as Element of P2;

        reconsider fp, fq as Polynomial of (o1 +^ o2), L by POLYNOM1:def 11;

        (f . (x * y)) = (f . (p *' q)) by POLYNOM1:def 11;

        then

        reconsider fpq9 = (f . (p *' q)) as Polynomial of (o1 +^ o2), L by POLYNOM1:def 11;

        

         A17: for b be bag of (o1 +^ o2) holds ex s be FinSequence of the carrier of L st (fpq9 . b) = ( Sum s) & ( len s) = ( len ( decomp b)) & for k be Element of NAT st k in ( dom s) holds ex b1,b2 be bag of (o1 +^ o2) st (( decomp b) /. k) = <*b1, b2*> & (s /. k) = ((fp . b1) * (fq . b2))

        proof

          reconsider x = (p *' q) as Element of P1 by POLYNOM1:def 11;

          let c be bag of (o1 +^ o2);

          reconsider b = c as Element of ( Bags (o1 +^ o2)) by PRE_POLY:def 12;

          consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) such that

           A18: b = (b1 +^ b2) by Th6;

          reconsider b1 as bag of o1;

          consider r be FinSequence of the carrier of ( Polynom-Ring (o2,L)) such that

           A19: ((p *' q) . b1) = ( Sum r) and

           A20: ( len r) = ( len ( decomp b1)) and

           A21: for k be Element of NAT st k in ( dom r) holds ex a19,b19 be bag of o1 st (( decomp b1) /. k) = <*a19, b19*> & (r /. k) = ((p . a19) * (q . b19)) by POLYNOM1:def 10;

          for x be object st x in ( dom r) holds (r . x) is Function

          proof

            let x be object;

            assume x in ( dom r);

            then

             A22: (r . x) in ( rng r) by FUNCT_1: 3;

            ( rng r) c= the carrier of ( Polynom-Ring (o2,L)) by FINSEQ_1:def 4;

            hence thesis by A22, POLYNOM1:def 11;

          end;

          then

          reconsider rFF = r as Function-yielding Function by FUNCOP_1:def 6;

          deffunc F( object) = ((rFF . $1) . b2);

          consider rFFb2 be Function such that

           A23: ( dom rFFb2) = ( dom r) and

           A24: for i be object st i in ( dom r) holds (rFFb2 . i) = F(i) from FUNCT_1:sch 3;

          ex i be Nat st ( dom r) = ( Seg i) by FINSEQ_1:def 2;

          then

          reconsider rFFb2 as FinSequence by A23, FINSEQ_1:def 2;

          

           A25: ( rng rFFb2) c= the carrier of L

          proof

            let u be object;

            

             A26: ( rng rFF) c= the carrier of ( Polynom-Ring (o2,L)) by FINSEQ_1:def 4;

            assume u in ( rng rFFb2);

            then

            consider x be object such that

             A27: x in ( dom rFFb2) and

             A28: u = (rFFb2 . x) by FUNCT_1:def 3;

            (rFF . x) in ( rng rFF) by A23, A27, FUNCT_1: 3;

            then

             A29: (rFF . x) is Function of ( Bags o2), the carrier of L by A26, POLYNOM1:def 11;

            then

             A30: ( rng (rFF . x)) c= the carrier of L by RELAT_1:def 19;

            ( dom (rFF . x)) = ( Bags o2) by A29, FUNCT_2:def 1;

            then

             A31: ((rFF . x) . b2) in ( rng (rFF . x)) by FUNCT_1: 3;

            (rFFb2 . x) = ((rFF . x) . b2) by A23, A24, A27;

            hence thesis by A28, A30, A31;

          end;

          defpred P[ set, set] means ex a19,b19 be bag of o1, Fk be FinSequence of the carrier of L, pa19,qb19 be Polynomial of o2, L st pa19 = (p . a19) & qb19 = (q . b19) & Fk = $2 & (( decomp b1) /. $1) = <*a19, b19*> & ( len Fk) = ( len ( decomp b2)) & for m be Nat st m in ( dom Fk) holds ex a199,b199 be bag of o2 st (( decomp b2) /. m) = <*a199, b199*> & (Fk /. m) = ((pa19 . a199) * (qb19 . b199));

          

           A32: for k be Nat st k in ( Seg ( len r)) holds ex x be Element of (the carrier of L * ) st P[k, x]

          proof

            let k be Nat;

            assume k in ( Seg ( len r));

            then k in ( dom ( decomp b1)) by A20, FINSEQ_1:def 3;

            then

            consider a19,b19 be bag of o1 such that

             A33: (( decomp b1) /. k) = <*a19, b19*> and b1 = (a19 + b19) by PRE_POLY: 68;

            reconsider pa199 = (p . a19), qb199 = (q . b19) as Element of ( Polynom-Ring (o2,L));

            reconsider pa19 = pa199, qb19 = qb199 as Polynomial of o2, L by POLYNOM1:def 11;

            defpred Q[ set, set] means ex a199,b199 be bag of o2 st (( decomp b2) /. $1) = <*a199, b199*> & $2 = ((pa19 . a199) * (qb19 . b199));

            

             A34: for k be Nat st k in ( Seg ( len ( decomp b2))) holds ex x be Element of L st Q[k, x]

            proof

              let k be Nat;

              assume k in ( Seg ( len ( decomp b2)));

              then k in ( dom ( decomp b2)) by FINSEQ_1:def 3;

              then

              consider a199,b199 be bag of o2 such that

               A35: (( decomp b2) /. k) = <*a199, b199*> and b2 = (a199 + b199) by PRE_POLY: 68;

              reconsider x = ((pa19 . a199) * (qb19 . b199)) as Element of L;

              take x, a199, b199;

              thus thesis by A35;

            end;

            consider Fk be FinSequence of the carrier of L such that

             A36: ( dom Fk) = ( Seg ( len ( decomp b2))) and

             A37: for k be Nat st k in ( Seg ( len ( decomp b2))) holds Q[k, (Fk /. k)] from RECDEF_1:sch 17( A34);

            reconsider x = Fk as Element of (the carrier of L * ) by FINSEQ_1:def 11;

            take x, a19, b19, Fk, pa19, qb19;

            thus pa19 = (p . a19) & qb19 = (q . b19) & Fk = x;

            thus (( decomp b1) /. k) = <*a19, b19*> by A33;

            thus ( len Fk) = ( len ( decomp b2)) by A36, FINSEQ_1:def 3;

            let m be Nat;

            assume m in ( dom Fk);

            hence thesis by A36, A37;

          end;

          consider F be FinSequence of (the carrier of L * ) such that

           A38: ( dom F) = ( Seg ( len r)) and

           A39: for k be Nat st k in ( Seg ( len r)) holds P[k, (F /. k)] from RECDEF_1:sch 17( A32);

          take s = ( FlattenSeq F);

          

           A40: ( len ( Sum F)) = ( len F) by MATRLIN:def 6;

          reconsider rFFb2 as FinSequence of the carrier of L by A25, FINSEQ_1:def 4;

          

           A41: (f . x) = ( Compress (p *' q)) by A2;

          

           A42: ( dom rFFb2) = ( dom F) by A38, A23, FINSEQ_1:def 3

          .= ( dom ( Sum F)) by A40, FINSEQ_3: 29;

          for k be Nat st k in ( dom rFFb2) holds (rFFb2 . k) = (( Sum F) . k)

          proof

            let k be Nat such that

             A43: k in ( dom rFFb2);

            consider c1,d1 be bag of o1 such that

             A44: (( decomp b1) /. k) = <*c1, d1*> and

             A45: (r /. k) = ((p . c1) * (q . d1)) by A21, A23, A43;

            k in ( Seg ( len r)) by A23, A43, FINSEQ_1:def 3;

            then

            consider a19,b19 be bag of o1, Fk be FinSequence of the carrier of L, pa19,qb19 be Polynomial of o2, L such that

             A46: pa19 = (p . a19) & qb19 = (q . b19) and

             A47: Fk = (F /. k) and

             A48: (( decomp b1) /. k) = <*a19, b19*> and

             A49: ( len Fk) = ( len ( decomp b2)) and

             A50: for ki be Nat st ki in ( dom Fk) holds ex a199,b199 be bag of o2 st (( decomp b2) /. ki) = <*a199, b199*> & (Fk /. ki) = ((pa19 . a199) * (qb19 . b199)) by A39;

            

             A51: c1 = a19 & d1 = b19 by A44, A48, FINSEQ_1: 77;

            consider s1 be FinSequence of the carrier of L such that

             A52: ((pa19 *' qb19) . b2) = ( Sum s1) and

             A53: ( len s1) = ( len ( decomp b2)) and

             A54: for ki be Element of NAT st ki in ( dom s1) holds ex x1,y2 be bag of o2 st (( decomp b2) /. ki) = <*x1, y2*> & (s1 /. ki) = ((pa19 . x1) * (qb19 . y2)) by POLYNOM1:def 10;

            

             A55: ( dom s1) = ( Seg ( len s1)) by FINSEQ_1:def 3;

            now

              let ki be Nat;

              assume

               A56: ki in ( dom s1);

              then

               A57: (s1 /. ki) = (s1 . ki) by PARTFUN1:def 6;

              

               A58: ki in ( dom Fk) by A49, A53, A55, A56, FINSEQ_1:def 3;

              then

              consider a199,b199 be bag of o2 such that

               A59: (( decomp b2) /. ki) = <*a199, b199*> and

               A60: (Fk /. ki) = ((pa19 . a199) * (qb19 . b199)) by A50;

              consider x1,y2 be bag of o2 such that

               A61: (( decomp b2) /. ki) = <*x1, y2*> and

               A62: (s1 /. ki) = ((pa19 . x1) * (qb19 . y2)) by A54, A56;

              x1 = a199 & y2 = b199 by A61, A59, FINSEQ_1: 77;

              hence (s1 . ki) = (Fk . ki) by A62, A58, A60, A57, PARTFUN1:def 6;

            end;

            then

             A63: s1 = Fk by A49, A53, FINSEQ_2: 9;

            

             A64: (rFF . k) = (r /. k) by A23, A43, PARTFUN1:def 6

            .= (pa19 *' qb19) by A45, A46, A51, POLYNOM1:def 11;

            

            thus (rFFb2 . k) = ((rFF . k) . b2) by A23, A24, A43

            .= (( Sum F) /. k) by A42, A43, A47, A64, A52, A63, MATRLIN:def 6

            .= (( Sum F) . k) by A42, A43, PARTFUN1:def 6;

          end;

          then

           A65: rFFb2 = ( Sum F) by A42;

          reconsider Sr = ( Sum r) as Polynomial of o2, L by POLYNOM1:def 11;

          consider gg be sequence of the carrier of ( Polynom-Ring (o2,L)) such that

           A66: ( Sum r) = (gg . ( len r)) and

           A67: (gg . 0 ) = ( 0. ( Polynom-Ring (o2,L))) and

           A68: for j be Nat, v be Element of ( Polynom-Ring (o2,L)) st j < ( len r) & v = (r . (j + 1)) holds (gg . (j + 1)) = ((gg . j) + v) by RLVECT_1:def 12;

          defpred R[ Nat, set] means for pp be Polynomial of o2, L st $1 <= ( len r) & pp = (gg . $1) holds $2 = (pp . b2);

          

           A69: for x be Element of NAT holds ex y be Element of L st R[x, y]

          proof

            let x be Element of NAT ;

            reconsider pp9 = (gg . x) as Polynomial of o2, L by POLYNOM1:def 11;

            take y = (pp9 . b2);

            let pp be Polynomial of o2, L;

            assume that x <= ( len r) and

             A70: pp = (gg . x);

            thus thesis by A70;

          end;

          consider ff be sequence of the carrier of L such that

           A71: for j be Element of NAT holds R[j, (ff . j)] from FUNCT_2:sch 3( A69);

          

           A72: for j be Nat holds R[j, (ff . j)]

          proof

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            hence thesis by A71;

          end;

          defpred VV[ set, set] means ex a19,b19 be Element of ( Bags o1), Fk be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) st Fk = $2 & (( decomp b1) /. $1) = <*a19, b19*> & ( len Fk) = ( len ( decomp b2)) & for m be Nat st m in ( dom Fk) holds ex a199,b199 be Element of ( Bags o2) st (( decomp b2) /. m) = <*a199, b199*> & (Fk /. m) = <*(a19 +^ a199), (b19 +^ b199)*>;

          

           A73: for i be Nat st i in ( Seg ( len r)) holds ex x be Element of ((2 -tuples_on ( Bags (o1 +^ o2))) * ) st VV[i, x]

          proof

            let k be Nat;

            assume k in ( Seg ( len r));

            then k in ( dom ( decomp b1)) by A20, FINSEQ_1:def 3;

            then

            consider a19,b19 be bag of o1 such that

             A74: (( decomp b1) /. k) = <*a19, b19*> and b1 = (a19 + b19) by PRE_POLY: 68;

            reconsider a19, b19 as Element of ( Bags o1) by PRE_POLY:def 12;

            defpred Q[ set, set] means ex a199,b199 be Element of ( Bags o2) st (( decomp b2) /. $1) = <*a199, b199*> & $2 = <*(a19 +^ a199), (b19 +^ b199)*>;

            

             A75: for k be Nat st k in ( Seg ( len ( decomp b2))) holds ex x be Element of (2 -tuples_on ( Bags (o1 +^ o2))) st Q[k, x]

            proof

              let k be Nat;

              assume k in ( Seg ( len ( decomp b2)));

              then k in ( dom ( decomp b2)) by FINSEQ_1:def 3;

              then

              consider a199,b199 be bag of o2 such that

               A76: (( decomp b2) /. k) = <*a199, b199*> and b2 = (a199 + b199) by PRE_POLY: 68;

              reconsider a199, b199 as Element of ( Bags o2) by PRE_POLY:def 12;

              reconsider x = <*(a19 +^ a199), (b19 +^ b199)*> as Element of (2 -tuples_on ( Bags (o1 +^ o2)));

              take x;

              take a199, b199;

              thus thesis by A76;

            end;

            consider Fk be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) such that

             A77: ( dom Fk) = ( Seg ( len ( decomp b2))) and

             A78: for k be Nat st k in ( Seg ( len ( decomp b2))) holds Q[k, (Fk /. k)] from RECDEF_1:sch 17( A75);

            reconsider x = Fk as Element of ((2 -tuples_on ( Bags (o1 +^ o2))) * ) by FINSEQ_1:def 11;

            take x, a19, b19;

            take Fk;

            thus Fk = x;

            thus (( decomp b1) /. k) = <*a19, b19*> by A74;

            thus ( len Fk) = ( len ( decomp b2)) by A77, FINSEQ_1:def 3;

            let m be Nat;

            assume m in ( dom Fk);

            hence thesis by A77, A78;

          end;

          consider G be FinSequence of ((2 -tuples_on ( Bags (o1 +^ o2))) * ) such that

           A79: ( dom G) = ( Seg ( len r)) and

           A80: for i be Nat st i in ( Seg ( len r)) holds VV[i, (G /. i)] from RECDEF_1:sch 17( A73);

          

           A81: for i be Nat st i in ( Seg ( len r)) holds VV[i, (G /. i)] by A80;

          

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

          

           A83: for j be Nat st j in ( dom ( Card F)) holds (( Card F) . j) = (( Card G) . j)

          proof

            let j be Nat;

            assume

             A84: j in ( dom ( Card F));

            then

             A85: j in ( dom F) by CARD_3:def 2;

            then

             A86: (( Card F) . j) = ( card (F . j)) by CARD_3:def 2;

            

             A87: (ex a19,b19 be bag of o1, Fk be FinSequence of the carrier of L, pa19,qb19 be Polynomial of o2, L st pa19 = (p . a19) & qb19 = (q . b19) & Fk = (F /. j) & (( decomp b1) /. j) = <*a19, b19*> & ( len Fk) = ( len ( decomp b2)) & for m be Nat st m in ( dom Fk) holds ex a199,b199 be bag of o2 st (( decomp b2) /. m) = <*a199, b199*> & (Fk /. m) = ((pa19 . a199) * (qb19 . b199))) & ex a29,b29 be Element of ( Bags o1), Gk be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) st Gk = (G /. j) & (( decomp b1) /. j) = <*a29, b29*> & ( len Gk) = ( len ( decomp b2)) & for m be Nat st m in ( dom Gk) holds ex a299,b299 be Element of ( Bags o2) st (( decomp b2) /. m) = <*a299, b299*> & (Gk /. m) = <*(a29 +^ a299), (b29 +^ b299)*> by A38, A39, A80, A85;

            ( card (F . j)) = ( card (F /. j)) by A85, PARTFUN1:def 6

            .= ( card (G . j)) by A38, A79, A82, A84, A87, PARTFUN1:def 6;

            hence thesis by A38, A79, A82, A84, A86, CARD_3:def 2;

          end;

          consider c1 be Element of ( Bags o1), c2 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

           A88: Q1 = ((p *' q) . c1) and

           A89: b = (c1 +^ c2) and

           A90: (( Compress (p *' q)) . b) = (Q1 . c2) by Def2;

          

           A91: c1 = b1 by A18, A89, Th7;

          then ( dom G) = ( dom ( decomp c1)) by A20, A79, FINSEQ_1:def 3;

          then

           A92: ( decomp c) = ( FlattenSeq G) by A18, A79, A81, A91, Th14;

          

           A93: for j be Nat, v be Element of L st j < ( len rFFb2) & v = (rFFb2 . (j + 1)) holds (ff . (j + 1)) = ((ff . j) + v)

          proof

            let j be Nat, v be Element of L;

            assume that

             A94: j < ( len rFFb2) and

             A95: v = (rFFb2 . (j + 1));

            reconsider w = (r /. (j + 1)), pp = (gg . j), pp9 = (gg . (j + 1)) as Polynomial of o2, L by POLYNOM1:def 11;

            reconsider w1 = w, pp1 = pp, pp19 = pp9 as Element of ( Polynom-Ring (o2,L));

            reconsider w1, pp1, pp19 as Element of ( Polynom-Ring (o2,L));

            

             A96: j < ( len r) by A23, A94, FINSEQ_3: 29;

            then

             A97: (j + 1) <= ( len r) by NAT_1: 13;

            then

             A98: w = (r . (j + 1)) by FINSEQ_4: 15, NAT_1: 11;

            then

             A99: pp19 = (pp1 + w1) by A68, A96;

            1 <= (j + 1) by NAT_1: 11;

            then (j + 1) in ( dom r) by A97, FINSEQ_3: 25;

            then

             A100: (w . b2) = v by A24, A95, A98;

            (j + 1) <= ( len r) by A96, NAT_1: 13;

            

            hence (ff . (j + 1)) = (pp9 . b2) by A72

            .= ((pp + w) . b2) by A99, POLYNOM1:def 11

            .= ((pp . b2) + (w . b2)) by POLYNOM1: 15

            .= ((ff . j) + v) by A72, A96, A100;

          end;

          (gg . 0 ) = ( 0_ (o2,L)) by A67, POLYNOM1:def 11;

          

          then

           A101: (ff . 0 ) = (( 0_ (o2,L)) . b2) by A72, NAT_1: 2

          .= ( 0. L) by POLYNOM1: 22;

          ( len rFFb2) = ( len r) by A23, FINSEQ_3: 29;

          then (Sr . b2) = (ff . ( len rFFb2)) by A66, A72;

          then

           A102: (Sr . b2) = ( Sum rFFb2) by A101, A93, RLVECT_1:def 12;

          b1 = c1 & b2 = c2 by A18, A89, Th7;

          hence (fpq9 . c) = ( Sum s) by A19, A88, A90, A65, A102, A41, POLYNOM1: 14;

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

          then ( len ( Card F)) = ( len ( Card G)) by A38, A79, A82, FINSEQ_3: 29;

          then

           A103: ( Card F) = ( Card G) by A83, FINSEQ_2: 9;

          hence

           A104: ( len s) = ( len ( decomp c)) by A92, PRE_POLY: 28;

          let k be Element of NAT ;

          assume

           A105: k in ( dom s);

          then

          consider i,j be Nat such that

           A106: i in ( dom F) and

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

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

           A109: ((F . i) . j) = (( FlattenSeq F) . k) by PRE_POLY: 29;

          

           A110: k in ( dom ( decomp c)) by A104, A105, FINSEQ_3: 29;

          then

          consider i9,j9 be Nat such that

           A111: i9 in ( dom G) and

           A112: j9 in ( dom (G . i9)) and

           A113: k = (( Sum ( Card (G | (i9 -' 1)))) + j9) and

           A114: ((G . i9) . j9) = (( decomp c) . k) by A92, PRE_POLY: 29;

          (( Sum (( Card F) | (i -' 1))) + j) = (( Sum ( Card (F | (i -' 1)))) + j) by POLYNOM3: 16

          .= (( Sum (( Card G) | (i9 -' 1))) + j9) by A108, A113, POLYNOM3: 16;

          then

           A115: i = i9 & j = j9 by A103, A106, A107, A111, A112, POLYNOM3: 22;

          consider c1,c2 be bag of (o1 +^ o2) such that

           A116: (( decomp c) /. k) = <*c1, c2*> and c = (c1 + c2) by A110, PRE_POLY: 68;

          reconsider cc1 = c1, cc2 = c2 as Element of ( Bags (o1 +^ o2)) by PRE_POLY:def 12;

          consider cb1 be Element of ( Bags o1), cb2 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

           A117: Q1 = (p . cb1) and

           A118: cc1 = (cb1 +^ cb2) and

           A119: (( Compress p) . cc1) = (Q1 . cb2) by Def2;

          consider a19,b19 be bag of o1, Fk be FinSequence of the carrier of L, pa19,qb19 be Polynomial of o2, L such that

           A120: pa19 = (p . a19) and

           A121: qb19 = (q . b19) and

           A122: Fk = (F /. i) and

           A123: (( decomp b1) /. i) = <*a19, b19*> and ( len Fk) = ( len ( decomp b2)) and

           A124: for m be Nat st m in ( dom Fk) holds ex a199,b199 be bag of o2 st (( decomp b2) /. m) = <*a199, b199*> & (Fk /. m) = ((pa19 . a199) * (qb19 . b199)) by A38, A39, A106;

          consider ga19,gb19 be Element of ( Bags o1), Gk be FinSequence of (2 -tuples_on ( Bags (o1 +^ o2))) such that

           A125: Gk = (G /. i) and

           A126: (( decomp b1) /. i) = <*ga19, gb19*> and ( len Gk) = ( len ( decomp b2)) and

           A127: for m be Nat st m in ( dom Gk) holds ex ga199,gb199 be Element of ( Bags o2) st (( decomp b2) /. m) = <*ga199, gb199*> & (Gk /. m) = <*(ga19 +^ ga199), (gb19 +^ gb199)*> by A38, A80, A106;

          

           A128: b19 = gb19 by A123, A126, FINSEQ_1: 77;

          

           A129: Gk = (G . i) by A38, A79, A106, A125, PARTFUN1:def 6;

          then

          consider ga199,gb199 be Element of ( Bags o2) such that

           A130: (( decomp b2) /. j) = <*ga199, gb199*> and

           A131: (Gk /. j) = <*(ga19 +^ ga199), (gb19 +^ gb199)*> by A112, A115, A127;

          

           A132: <*c1, c2*> = ((G . i) . j) by A110, A116, A114, A115, PARTFUN1:def 6

          .= <*(ga19 +^ ga199), (gb19 +^ gb199)*> by A112, A115, A129, A131, PARTFUN1:def 6;

          then c1 = (ga19 +^ ga199) by FINSEQ_1: 77;

          then

           A133: cb1 = ga19 & cb2 = ga199 by A118, Th7;

          

           A134: a19 = ga19 by A123, A126, FINSEQ_1: 77;

          j in ( dom Fk) by A106, A107, A122, PARTFUN1:def 6;

          then

          consider a199,b199 be bag of o2 such that

           A135: (( decomp b2) /. j) = <*a199, b199*> and

           A136: (Fk /. j) = ((pa19 . a199) * (qb19 . b199)) by A124;

          a199 = ga199 by A130, A135, FINSEQ_1: 77;

          then

           A137: (pa19 . a199) = (fp . c1) by A2, A120, A117, A119, A133, A134;

          take c1, c2;

          thus (( decomp c) /. k) = <*c1, c2*> by A116;

          consider cb1 be Element of ( Bags o1), cb2 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

           A138: Q1 = (q . cb1) and

           A139: cc2 = (cb1 +^ cb2) and

           A140: (( Compress q) . cc2) = (Q1 . cb2) by Def2;

          c2 = (gb19 +^ gb199) by A132, FINSEQ_1: 77;

          then

           A141: cb1 = gb19 & cb2 = gb199 by A139, Th7;

          

           A142: Fk = (F . i) by A106, A122, PARTFUN1:def 6;

          b199 = gb199 by A130, A135, FINSEQ_1: 77;

          then

           A143: (qb19 . b199) = (fq . c2) by A2, A121, A128, A138, A140, A141;

          

          thus (s /. k) = (s . k) by A105, PARTFUN1:def 6

          .= ((fp . c1) * (fq . c2)) by A107, A109, A142, A136, A137, A143, PARTFUN1:def 6;

        end;

        

        thus (f . (x * y)) = (f . (p *' q)) by POLYNOM1:def 11

        .= (fp *' fq) by A17, POLYNOM1:def 10

        .= ((f . x) * (f . y)) by POLYNOM1:def 11;

      end;

      hence f is multiplicative by GROUP_6:def 6;

      

       A144: for b be Element of ( Bags (o1 +^ o2)) holds (( Compress 1P1) . b) = (1P2 . b)

      proof

        let b be Element of ( Bags (o1 +^ o2));

        

         A145: (1P2 . b) = (( 1_ ((o1 +^ o2),L)) . b) by POLYNOM1: 31;

        consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

         A146: Q1 = (1P1 . b1) and

         A147: b = (b1 +^ b2) and

         A148: (( Compress 1P1) . b) = (Q1 . b2) by Def2;

        per cases ;

          suppose

           A149: b = ( EmptyBag (o1 +^ o2));

          then

           A150: b1 = ( EmptyBag o1) by A147, Th5;

          

           A151: b2 = ( EmptyBag o2) by A147, A149, Th5;

          Q1 = (( 1_ (o1,( Polynom-Ring (o2,L)))) . b1) by A146, POLYNOM1: 31

          .= ( 1_ ( Polynom-Ring (o2,L))) by A150, POLYNOM1: 25;

          

          then (Q1 . b2) = (( 1_ (o2,L)) . b2) by POLYNOM1: 31

          .= ( 1_ L) by A151, POLYNOM1: 25

          .= (1P2 . b) by A145, A149, POLYNOM1: 25;

          hence thesis by A148;

        end;

          suppose

           A152: b <> ( EmptyBag (o1 +^ o2));

          then

           A153: b1 <> ( EmptyBag o1) or b2 <> ( EmptyBag o2) by A147, Th5;

          now

            per cases ;

              suppose

               A154: b1 = ( EmptyBag o1);

              Q1 = (( 1_ (o1,( Polynom-Ring (o2,L)))) . b1) by A146, POLYNOM1: 31

              .= ( 1_ ( Polynom-Ring (o2,L))) by A154, POLYNOM1: 25

              .= ( 1_ (o2,L)) by POLYNOM1: 31;

              

              then (Q1 . b2) = ( 0. L) by A153, A154, POLYNOM1: 25

              .= (1P2 . b) by A145, A152, POLYNOM1: 25;

              hence thesis by A148;

            end;

              suppose

               A155: b1 <> ( EmptyBag o1);

              Q1 = (( 1_ (o1,( Polynom-Ring (o2,L)))) . b1) by A146, POLYNOM1: 31

              .= ( 0. ( Polynom-Ring (o2,L))) by A155, POLYNOM1: 25

              .= ( 0_ (o2,L)) by POLYNOM1:def 11;

              

              then (Q1 . b2) = ( 0. L) by POLYNOM1: 22

              .= (1P2 . b) by A145, A152, POLYNOM1: 25;

              hence thesis by A148;

            end;

          end;

          hence thesis;

        end;

      end;

      (f . ( 1_ P1)) = ( Compress 1P1) by A2

      .= ( 1_ P2) by A144, FUNCT_2: 63;

      hence f is unity-preserving by GROUP_1:def 13;

      thus f is one-to-one

      proof

        let x1,x2 be object;

        assume x1 in ( dom f);

        then

        reconsider x19 = x1 as Element of P1 by FUNCT_2:def 1;

        assume x2 in ( dom f);

        then

        reconsider x29 = x2 as Element of P1 by FUNCT_2:def 1;

        reconsider x299 = x29 as Polynomial of o1, ( Polynom-Ring (o2,L)) by POLYNOM1:def 11;

        reconsider x199 = x19 as Polynomial of o1, ( Polynom-Ring (o2,L)) by POLYNOM1:def 11;

        

         A156: (f . x29) = ( Compress x299) by A2;

        then

        reconsider w2 = (f . x29) as Polynomial of (o1 +^ o2), L;

        

         A157: (f . x19) = ( Compress x199) by A2;

        then

        reconsider w1 = (f . x19) as Polynomial of (o1 +^ o2), L;

        assume

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

        now

          let b1 be Element of ( Bags o1);

          reconsider x199b1 = (x199 . b1), x299b1 = (x299 . b1) as Polynomial of o2, L by POLYNOM1:def 11;

          now

            let b2 be Element of ( Bags o2);

            set b = (b1 +^ b2);

            consider b19 be Element of ( Bags o1), b29 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

             A159: Q1 = (x199 . b19) and

             A160: b = (b19 +^ b29) and

             A161: (w1 . b) = (Q1 . b29) by A157, Def2;

            

             A162: b1 = b19 & b2 = b29 by A160, Th7;

            consider c1 be Element of ( Bags o1), c2 be Element of ( Bags o2), Q19 be Polynomial of o2, L such that

             A163: Q19 = (x299 . c1) and

             A164: b = (c1 +^ c2) and

             A165: (w2 . b) = (Q19 . c2) by A156, Def2;

            b1 = c1 by A164, Th7;

            hence (x199b1 . b2) = (x299b1 . b2) by A158, A159, A161, A163, A164, A165, A162, Th7;

          end;

          hence (x199 . b1) = (x299 . b1) by FUNCT_2: 63;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      thus ( rng f) c= the carrier of P2 by RELAT_1:def 19;

      thus the carrier of P2 c= ( rng f)

      proof

        defpred KK[ set, set] means ex b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) st $1 = (b1 +^ b2) & $2 = b1;

        let y be object;

        assume y in the carrier of P2;

        then

        reconsider s = y as Polynomial of (o1 +^ o2), L by POLYNOM1:def 11;

        defpred K[ Element of ( Bags o1), Element of ( Polynom-Ring (o2,L))] means ex h be Function st h = $2 & for b2 be Element of ( Bags o2), b be Element of ( Bags (o1 +^ o2)) st b = ($1 +^ b2) holds (h . b2) = (s . b);

        

         A166: for x be Element of ( Bags (o1 +^ o2)) holds ex y be Element of ( Bags o1) st KK[x, y]

        proof

          let x be Element of ( Bags (o1 +^ o2));

          consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) such that

           A167: x = (b1 +^ b2) by Th6;

          reconsider y = b1 as Element of ( Bags o1);

          take y, b1, b2;

          thus x = (b1 +^ b2) by A167;

          thus y = b1;

        end;

        consider kk be Function of ( Bags (o1 +^ o2)), ( Bags o1) such that

         A168: for b be Element of ( Bags (o1 +^ o2)) holds KK[b, (kk . b)] from FUNCT_2:sch 3( A166);

        

         A169: for x be Element of ( Bags o1) holds ex y be Element of ( Polynom-Ring (o2,L)) st K[x, y]

        proof

          defpred KK[ set, set] means ex b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) st $1 = (b1 +^ b2) & $2 = b2;

          let x be Element of ( Bags o1);

          reconsider b1 = x as Element of ( Bags o1);

          defpred L[ Element of ( Bags o2), Element of L] means for b be Element of ( Bags (o1 +^ o2)) st b = (b1 +^ $1) holds $2 = (s . b);

          

           A170: for p be Element of ( Bags o2) holds ex q be Element of L st L[p, q]

          proof

            let p be Element of ( Bags o2);

            take (s . (b1 +^ p));

            let b be Element of ( Bags (o1 +^ o2));

            assume b = (b1 +^ p);

            hence thesis;

          end;

          consider t be Function of ( Bags o2), the carrier of L such that

           A171: for b2 be Element of ( Bags o2) holds L[b2, (t . b2)] from FUNCT_2:sch 3( A170);

          reconsider t as Function of ( Bags o2), L;

          

           A172: for x be Element of ( Bags (o1 +^ o2)) holds ex y be Element of ( Bags o2) st KK[x, y]

          proof

            let x be Element of ( Bags (o1 +^ o2));

            consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2) such that

             A173: x = (b1 +^ b2) by Th6;

            reconsider y = b2 as Element of ( Bags o2);

            take y, b1, b2;

            thus x = (b1 +^ b2) by A173;

            thus y = b2;

          end;

          consider kk be Function of ( Bags (o1 +^ o2)), ( Bags o2) such that

           A174: for b be Element of ( Bags (o1 +^ o2)) holds KK[b, (kk . b)] from FUNCT_2:sch 3( A172);

          ( Support t) c= (kk .: ( Support s))

          proof

            let x be object;

            assume

             A175: x in ( Support t);

            then

            reconsider b2 = x as Element of ( Bags o2);

            set b = (b1 +^ b2);

            (t . x) <> ( 0. L) by A175, POLYNOM1:def 4;

            then (s . b) <> ( 0. L) by A171;

            then

             A176: ( dom kk) = ( Bags (o1 +^ o2)) & b in ( Support s) by FUNCT_2:def 1, POLYNOM1:def 4;

            ex b19 be Element of ( Bags o1), b29 be Element of ( Bags o2) st b = (b19 +^ b29) & (kk . b) = b29 by A174;

            then x = (kk . b) by Th7;

            hence thesis by A176, FUNCT_1:def 6;

          end;

          then t is Polynomial of o2, L by POLYNOM1:def 5;

          then

          reconsider t99 = t as Element of ( Polynom-Ring (o2,L)) by POLYNOM1:def 11;

          reconsider t9 = t as Function;

          take t99, t9;

          thus t99 = t9;

          let b2 be Element of ( Bags o2), b be Element of ( Bags (o1 +^ o2));

          assume b = (x +^ b2);

          hence thesis by A171;

        end;

        consider g be Function of ( Bags o1), the carrier of ( Polynom-Ring (o2,L)) such that

         A177: for x be Element of ( Bags o1) holds K[x, (g . x)] from FUNCT_2:sch 3( A169);

        reconsider g as Function of ( Bags o1), ( Polynom-Ring (o2,L));

        

         A178: ( Support g) c= (kk .: ( Support s))

        proof

          let x be object;

          assume

           A179: x in ( Support g);

          then

          reconsider b1 = x as Element of ( Bags o1);

          consider h be Function such that

           A180: h = (g . b1) and

           A181: for b2 be Element of ( Bags o2), b be Element of ( Bags (o1 +^ o2)) st b = (b1 +^ b2) holds (h . b2) = (s . b) by A177;

          reconsider h as Polynomial of o2, L by A180, POLYNOM1:def 11;

          (g . b1) <> ( 0. ( Polynom-Ring (o2,L))) by A179, POLYNOM1:def 4;

          then (g . b1) <> ( 0_ (o2,L)) by POLYNOM1:def 11;

          then

          consider b2 be Element of ( Bags o2) such that

           A182: b2 in ( Support h) by A180, POLYNOM2: 17, SUBSET_1: 4;

          set b = (b1 +^ b2);

          (h . b2) <> ( 0. L) by A182, POLYNOM1:def 4;

          then (s . b) <> ( 0. L) by A181;

          then

           A183: ( dom kk) = ( Bags (o1 +^ o2)) & b in ( Support s) by FUNCT_2:def 1, POLYNOM1:def 4;

          ex b19 be Element of ( Bags o1), b29 be Element of ( Bags o2) st b = (b19 +^ b29) & (kk . b) = b19 by A168;

          then x = (kk . b) by Th7;

          hence thesis by A183, FUNCT_1:def 6;

        end;

        then g is Polynomial of o1, ( Polynom-Ring (o2,L)) by POLYNOM1:def 5;

        then

        reconsider g as Element of P1 by POLYNOM1:def 11;

        reconsider g9 = g as Polynomial of o1, ( Polynom-Ring (o2,L)) by A178, POLYNOM1:def 5;

        now

          let b be Element of ( Bags (o1 +^ o2));

          consider b1 be Element of ( Bags o1), b2 be Element of ( Bags o2), Q1 be Polynomial of o2, L such that

           A184: Q1 = (g9 . b1) & b = (b1 +^ b2) & (( Compress g9) . b) = (Q1 . b2) by Def2;

          ex h be Function st h = (g9 . b1) & for b2 be Element of ( Bags o2), b be Element of ( Bags (o1 +^ o2)) st b = (b1 +^ b2) holds (h . b2) = (s . b) by A177;

          hence (s . b) = (( Compress g9) . b) by A184;

        end;

        

        then

         A185: y = ( Compress g9) by FUNCT_2: 63

        .= (f . g) by A2;

        ( dom f) = the carrier of P1 by FUNCT_2:def 1;

        hence thesis by A185, FUNCT_1: 3;

      end;

    end;