:: POLYNOM6 semantic presentation

begin


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: are_isomorphic
redefine predL1 is_ringisomorph_to L2;
reflexivity
 for L1 being non empty doubleLoopStr holds R83(b1,b1)
proof
let L1 be non empty doubleLoopStr ; ::_thesis: R83(L1,L1)
take  id L1 ; :: according to QUOFIELD:def_23 ::_thesis: id L1 is RingIsomorphism
thus  id L1 is RingHomomorphism ; :: according to QUOFIELD:def_20,QUOFIELD:def_21 ::_thesis: ( id L1 is one-to-one & id L1 is RingEpimorphism )
thus  id L1 is one-to-one ; ::_thesis: id L1 is RingEpimorphism
thus  id L1 is RingHomomorphism ; :: according to QUOFIELD:def_19 ::_thesis: K795( the carrier of L1,(id L1)) = the carrier of L1
thus  rng (id L1) = [#] L1 by TOPGRP_1:1
.= the carrier of L1 ; ::_thesis: verum
end;
end;

theorem Th1: :: POLYNOM6:1
for o1, o2 being Ordinal
for B being set st ( for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ) holds
o1 +^ o2 = o1 \/ B
proof
let o1, o2 be Ordinal; ::_thesis: for B being set st ( for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ) holds
o1 +^ o2 = o1 \/ B
let B be set ; ::_thesis: ( ( for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ) implies o1 +^ o2 = o1 \/ B )
assume A1: for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ; ::_thesis: o1 +^ o2 = o1 \/ B
 for x being set holds
( x in o1 +^ o2 iff x in o1 \/ B )
proof
let x be set ; ::_thesis: ( x in o1 +^ o2 iff x in o1 \/ B )
A2: ( x in o1 \/ B implies x in o1 +^ o2 )
proof
assume A3: x in o1 \/ B ; ::_thesis: x in o1 +^ o2
percases ( x in o1 or x in B ) by A3, XBOOLE_0:def_3;
supposeA4: x in o1 ; ::_thesis: x in o1 +^ o2
 o1 c= o1 +^ o2 by ORDINAL3:24;
hence  x in o1 +^ o2 by A4; ::_thesis: verum
end;
suppose x in B ; ::_thesis: x in o1 +^ o2
then  ex o being Ordinal st
( x = o1 +^ o & o in o2 ) by A1;
hence  x in o1 +^ o2 by ORDINAL2:32; ::_thesis: verum
end;
end;
end;
percases ( x in o1 or not x in o1 ) ;
suppose x in o1 ; ::_thesis: ( x in o1 +^ o2 iff x in o1 \/ B )
hence  ( x in o1 +^ o2 implies x in o1 \/ B ) by XBOOLE_0:def_3; ::_thesis: ( x in o1 \/ B implies x in o1 +^ o2 )
thus  ( x in o1 \/ B implies x in o1 +^ o2 ) by A2; ::_thesis: verum
end;
supposeA5: not x in o1 ; ::_thesis: ( x in o1 +^ o2 iff x in o1 \/ B )
thus  ( x in o1 +^ o2 implies x in o1 \/ B ) ::_thesis: ( x in o1 \/ B implies x in o1 +^ o2 )
proof
assume A6: x in o1 +^ o2 ; ::_thesis: x in o1 \/ B
percases ( o2 = {} or o2 <> {} ) ;
suppose o2 = {} ; ::_thesis: x in o1 \/ B
hence  x in o1 \/ B by A5, A6, ORDINAL2:27; ::_thesis: verum
end;
supposeA7: o2 <> {} ; ::_thesis: x in o1 \/ B
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  x in o1 \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
thus  ( x in o1 \/ B implies x in o1 +^ o2 ) by A2; ::_thesis: verum
end;
end;
end;
hence  o1 +^ o2 = o1 \/ B by TARSKI:1; ::_thesis: verum
end;

registration
let o1 be Ordinal;
let o2 be non empty Ordinal;
clustero1 +^ o2 ->  non empty ;
coherence
 not o1 +^ o2 is empty by ORDINAL3:26;
clustero2 +^ o1 ->  non empty ;
coherence
 not o2 +^ o1 is empty by ORDINAL3:26;
end;

theorem Th2: :: POLYNOM6:2
for n being Ordinal
for a, b being bag of n st a < b holds
ex o being Ordinal st
( o in n & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )
proof
let n be Ordinal; ::_thesis: for a, b being bag of n st a < b holds
ex o being Ordinal st
( o in n & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )
let a, b be bag of n; ::_thesis: ( a < b implies ex o being Ordinal st
( o in n & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) ) )
assume  a < b ; ::_thesis: ex o being Ordinal st
( o in n & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )
then consider o being Ordinal such that
A1: a . o < b . o and
A2: for l being Ordinal st l in o holds
a . l = b . l by PRE_POLY:def_9;
take  o ; ::_thesis: ( o in n & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )
now__::_thesis:_o_in_n
assume A3: not o in n ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  o in n ; ::_thesis: ( a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )
thus  a . o < b . o by A1; ::_thesis: for l being Ordinal st l in o holds
a . l = b . l
thus  for l being Ordinal st l in o holds
a . l = b . l by A2; ::_thesis: verum
end;

begin

definition
let o1, o2 be Ordinal;
let a be Element of Bags o1;
let b be Element of Bags o2;
funca +^ b ->  Element of Bags (o1 +^ o2) means :Def1: :: POLYNOM6:def 1
 for o being Ordinal holds
( ( o in o1 implies it . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies it . o = b . (o -^ o1) ) );
existence
 ex b1 being Element of Bags (o1 +^ o2) st
for o being Ordinal holds
( ( o in o1 implies b1 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b1 . o = b . (o -^ o1) ) )
proof
percases ( o2 = {} or o2 <> {} ) ;
supposeA1: o2 = {} ; ::_thesis: ex b1 being Element of Bags (o1 +^ o2) st
for o being Ordinal holds
( ( o in o1 implies b1 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b1 . o = b . (o -^ o1) ) )
then reconsider a9 = a as Element of Bags (o1 +^ o2) by ORDINAL2:27;
take  a9 ; ::_thesis: for o being Ordinal holds
( ( o in o1 implies a9 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) ) )
let o be Ordinal; ::_thesis: ( ( o in o1 implies a9 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) ) )
thus  ( o in o1 implies a9 . o = a . o ) ; ::_thesis: ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) )
 o1 +^ o2 = o1 by A1, ORDINAL2:27;
hence  ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) ) by XBOOLE_1:37; ::_thesis: verum
end;
suppose o2 <> {} ; ::_thesis: ex b1 being Element of Bags (o1 +^ o2) st
for o being Ordinal holds
( ( o in o1 implies b1 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b1 . o = b . (o -^ o1) ) )
then reconsider o29 = o2 as non empty Ordinal ;
defpred S1[ set , set ] means  ex o being Ordinal st
( o = $1 & ( o in o1 implies $2 = a . o ) & ( o in (o1 +^ o2) \ o1 implies $2 = b . (o -^ o1) ) );
deffunc H1( Element of o29) ->  set = o1 +^ $1;
set B =  {  H1(o) where o is Element of o29 : o in support b  }  ;
set C =  {  (o1 +^ o) where o is Element of o29 : verum  }  ;
A2: for i being set st i in o1 +^ o2 holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in o1 +^ o2 implies ex j being set st S1[i,j] )
assume A3: i in o1 +^ o2 ; ::_thesis: ex j being set st S1[i,j]
reconsider o = i as Ordinal by A3;
A4: ( o in o1 iff not o in (o1 +^ o2) \ o1 ) by A3, XBOOLE_0:def_5;
percases ( o in o1 or o in (o1 +^ o2) \ o1 ) by A3, XBOOLE_0:def_5;
supposeA5: o in o1 ; ::_thesis: ex j being set st S1[i,j]
take  a . o ; ::_thesis: S1[i,a . o]
take  o ; ::_thesis: ( o = i & ( o in o1 implies a . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a . o = b . (o -^ o1) ) )
thus  ( o = i & ( o in o1 implies a . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a . o = b . (o -^ o1) ) ) by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA6: o in (o1 +^ o2) \ o1 ; ::_thesis: ex j being set st S1[i,j]
take  b . (o -^ o1) ; ::_thesis: S1[i,b . (o -^ o1)]
thus  S1[i,b . (o -^ o1)] by A4, A6; ::_thesis: verum
end;
end;
end;
consider f being ManySortedSet of o1 +^ o2 such that
A7: for i being set st i in o1 +^ o2 holds
S1[i,f . i] from PBOOLE:sch_3(A2);
A8: support f c= (support a) \/  {  H1(o) where o is Element of o29 : o in support b  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support f or x in (support a) \/  {  H1(o) where o is Element of o29 : o in support b  }  )
assume  x in support f ; ::_thesis: x in (support a) \/  {  H1(o) where o is Element of o29 : o in support b  }
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 being set holds
( x in  {  (o1 +^ o) where o is Element of o29 : verum  }  iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) )
proof
let x be set ; ::_thesis: ( x in  {  (o1 +^ o) where o is Element of o29 : verum  }  iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) )
thus  ( x in  {  (o1 +^ o) where o is Element of o29 : verum  }  implies ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ::_thesis: ( ex o being Ordinal st
( x = o1 +^ o & o in o2 ) implies x in  {  (o1 +^ o) where o is Element of o29 : verum  }  )
proof
assume  x in  {  (o1 +^ o) where o is Element of o29 : verum  }  ; ::_thesis: ex o being Ordinal st
( x = o1 +^ o & o in o2 )
then  ex o9 being Element of o29 st x = o1 +^ o9 ;
hence  ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ; ::_thesis: verum
end;
thus  ( ex o being Ordinal st
( x = o1 +^ o & o in o2 ) implies x in  {  (o1 +^ o) where o is Element of o29 : verum  }  ) ; ::_thesis: verum
end;
then A11: x in o1 \/  {  (o1 +^ o) where o is Element of o29 : verum  }  by A10, Th1;
percases ( x in o1 or x in  {  (o1 +^ o) where o is Element of o29 : verum  }  ) by A11, XBOOLE_0:def_3;
supposeA12: x in o1 ; ::_thesis: x in (support a) \/  {  H1(o) where o is Element of o29 : o in support b  }
 S1[x,f . x] by A7, A10;
then  x in support a by A9, A12, PRE_POLY:def_7;
hence  x in (support a) \/  {  H1(o) where o is Element of o29 : o in support b  }  by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in  {  (o1 +^ o) where o is Element of o29 : verum  }  ; ::_thesis: x in (support a) \/  {  H1(o) where o is Element of o29 : o in support b  }
then  ex o9 being Element of o29 st x = o1 +^ o9 ;
then consider o99 being 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__::_thesis:_not_o_in_o1
percases ( o = o1 or o <> o1 ) ;
suppose o = o1 ; ::_thesis: not o in o1
hence  not o in o1 ; ::_thesis: verum
end;
suppose o <> o1 ; ::_thesis: not o in o1
then  o1 c< o by A15, XBOOLE_0:def_8;
hence  not o in o1 by ORDINAL1:11; ::_thesis: verum
end;
end;
end;
A17: S1[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  {  H1(o) where o is Element of o29 : o in support b  }  by A13, A14;
hence  x in (support a) \/  {  H1(o) where o is Element of o29 : o in support b  }  by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
A18: support b is finite ;
  {  H1(o) where o is Element of o29 : o in support 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 set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom f or f . x is natural )
assume  x in dom f ; ::_thesis: f . x is natural
then A20: x in o1 +^ o2 by PARTFUN1:def_2;
then reconsider o = x as Ordinal ;
A21: ex o9 being 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;
percases ( o in o1 or o in (o1 +^ o2) \ o1 ) by A20, XBOOLE_0:def_5;
suppose o in o1 ; ::_thesis: f . x is natural
hence  f . x is natural by A21; ::_thesis: verum
end;
suppose o in (o1 +^ o2) \ o1 ; ::_thesis: f . x is natural
hence  f . x is natural by A21; ::_thesis: verum
end;
end;
end;
then reconsider f = f as Element of Bags (o1 +^ o2) by A19, PRE_POLY:def_12;
take  f ; ::_thesis: for o being Ordinal holds
( ( o in o1 implies f . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies f . o = b . (o -^ o1) ) )
let o be Ordinal; ::_thesis: ( ( o in o1 implies f . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies f . o = b . (o -^ o1) ) )
thus  ( o in o1 implies f . o = a . o ) ::_thesis: ( o in (o1 +^ o2) \ o1 implies f . o = b . (o -^ o1) )
proof
assume A22: o in o1 ; ::_thesis: f . o = a . o
 o1 c= o1 +^ o2 by ORDINAL3:24;
then  ex p being 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  f . o = a . o by A22; ::_thesis: verum
end;
assume A23: o in (o1 +^ o2) \ o1 ; ::_thesis: f . o = b . (o -^ o1)
then  ex p being 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  f . o = b . (o -^ o1) by A23; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being Element of Bags (o1 +^ o2) st ( for o being Ordinal holds
( ( o in o1 implies b1 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b1 . o = b . (o -^ o1) ) ) ) & ( for o being Ordinal holds
( ( o in o1 implies b2 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b2 . o = b . (o -^ o1) ) ) ) holds
b1 = b2
proof
let a1, a2 be Element of Bags (o1 +^ o2); ::_thesis: ( ( for o being Ordinal holds
( ( o in o1 implies a1 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a1 . o = b . (o -^ o1) ) ) ) & ( for o being Ordinal holds
( ( o in o1 implies a2 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a2 . o = b . (o -^ o1) ) ) ) implies a1 = a2 )
assume that
A24: for o being 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 being Ordinal holds
( ( o in o1 implies a2 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a2 . o = b . (o -^ o1) ) ) ; ::_thesis: a1 = a2
A26: dom a1 = o1 +^ o2 by PARTFUN1:def_2;
A27: for c being set st c in dom a1 holds
a1 . c = a2 . c
proof
let c be set ; ::_thesis: ( c in dom a1 implies a1 . c = a2 . c )
assume A28: c in dom a1 ; ::_thesis: a1 . c = a2 . c
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 ;
percases ( o in o1 or o in (o1 +^ o2) \ o1 ) by A26, A28, A30, XBOOLE_0:def_3;
supposeA31: o in o1 ; ::_thesis: a1 . c = a2 . c
hence a1 . c = a . o by A24
.= a2 . c by A25, A31 ;
::_thesis: verum
end;
supposeA32: o in (o1 +^ o2) \ o1 ; ::_thesis: a1 . c = a2 . c
hence a1 . c = b . (o -^ o1) by A24
.= a2 . c by A25, A32 ;
::_thesis: verum
end;
end;
end;
 dom a1 = dom a2 by A26, PARTFUN1:def_2;
hence  a1 = a2 by A27, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines +^ POLYNOM6:def_1_:_
 for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2
for b5 being Element of Bags (o1 +^ o2) holds
( b5 = a +^ b iff for o being Ordinal holds
( ( o in o1 implies b5 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b5 . o = b . (o -^ o1) ) ) );

theorem Th3: :: POLYNOM6:3
for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2 st o2 = {} holds
a +^ b = a
proof
let o1, o2 be Ordinal; ::_thesis: for a being Element of Bags o1
for b being Element of Bags o2 st o2 = {} holds
a +^ b = a
let a be Element of Bags o1; ::_thesis: for b being Element of Bags o2 st o2 = {} holds
a +^ b = a
let b be Element of Bags o2; ::_thesis: ( o2 = {} implies a +^ b = a )
assume  o2 = {} ; ::_thesis: a +^ b = a
then reconsider ab = a +^ b as Element of Bags o1 by ORDINAL2:27;
 for i being set st i in o1 holds
ab . i = a . i by Def1;
hence  a +^ b = a by PBOOLE:3; ::_thesis: verum
end;

theorem :: POLYNOM6:4
for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2 st o1 = {} holds
a +^ b = b
proof
let o1, o2 be Ordinal; ::_thesis: for a being Element of Bags o1
for b being Element of Bags o2 st o1 = {} holds
a +^ b = b
let a be Element of Bags o1; ::_thesis: for b being Element of Bags o2 st o1 = {} holds
a +^ b = b
let b be Element of Bags o2; ::_thesis: ( o1 = {} implies a +^ b = b )
assume A1: o1 = {} ; ::_thesis: a +^ b = b
then reconsider ab = a +^ b as Element of Bags o2 by ORDINAL2:30;
now__::_thesis:_for_i_being_set_st_i_in_o2_holds_
ab_._i_=_b_._i
let i be set ; ::_thesis: ( i in o2 implies ab . i = b . i )
assume A2: i in o2 ; ::_thesis: ab . i = b . i
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; ::_thesis: verum
end;
hence  a +^ b = b by PBOOLE:3; ::_thesis: verum
end;

theorem Th5: :: POLYNOM6:5
for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2 holds
( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )
proof
let o1, o2 be Ordinal; ::_thesis: for b1 being Element of Bags o1
for b2 being Element of Bags o2 holds
( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )
let b1 be Element of Bags o1; ::_thesis: for b2 being Element of Bags o2 holds
( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )
let b2 be Element of Bags o2; ::_thesis: ( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )
hereby  ::_thesis: ( b1 = EmptyBag o1 & b2 = EmptyBag o2 implies b1 +^ b2 = EmptyBag (o1 +^ o2) )
assume A1: b1 +^ b2 = EmptyBag (o1 +^ o2) ; ::_thesis: ( b1 = EmptyBag o1 & b2 = EmptyBag o2 )
A2: for z being set st z in dom b1 holds
b1 . z = 0
proof
let z be set ; ::_thesis: ( z in dom b1 implies b1 . z = 0 )
A3: dom b1 = o1 by PARTFUN1:def_2;
assume A4: z in dom b1 ; ::_thesis: b1 . z = 0
then reconsider o = z as Ordinal by A3;
b1 . o = (b1 +^ b2) . o by A4, A3, Def1
.= 0 by A1, PRE_POLY:52 ;
hence  b1 . z = 0 ; ::_thesis: verum
end;
 dom b1 = o1 by PARTFUN1:def_2;
then  b1 = o1 --> 0 by A2, FUNCOP_1:11;
hence  b1 = EmptyBag o1 by PRE_POLY:def_13; ::_thesis: b2 = EmptyBag o2
A5: for z being set st z in dom b2 holds
b2 . z = 0
proof
let z be set ; ::_thesis: ( z in dom b2 implies b2 . z = 0 )
A6: dom b2 = o2 by PARTFUN1:def_2;
assume A7: z in dom b2 ; ::_thesis: b2 . z = 0
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, PRE_POLY:52;
hence  b2 . z = 0 by ORDINAL3:52; ::_thesis: verum
end;
 dom b2 = o2 by PARTFUN1:def_2;
then  b2 = o2 --> 0 by A5, FUNCOP_1:11;
hence  b2 = EmptyBag o2 by PRE_POLY:def_13; ::_thesis: verum
end;
thus  ( b1 = EmptyBag o1 & b2 = EmptyBag o2 implies b1 +^ b2 = EmptyBag (o1 +^ o2) ) ::_thesis: verum
proof
assume that
A9: b1 = EmptyBag o1 and
A10: b2 = EmptyBag o2 ; ::_thesis: b1 +^ b2 = EmptyBag (o1 +^ o2)
A11: for z being set st z in dom (b1 +^ b2) holds
(b1 +^ b2) . z = 0
proof
let z be set ; ::_thesis: ( z in dom (b1 +^ b2) implies (b1 +^ b2) . z = 0 )
A12: dom (b1 +^ b2) = o1 +^ o2 by PARTFUN1:def_2;
assume A13: z in dom (b1 +^ b2) ; ::_thesis: (b1 +^ b2) . z = 0
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, PRE_POLY:52;
 ( o in o1 implies ( b1 . o = 0 & (b1 +^ b2) . o = b1 . o ) ) by A9, Def1, PRE_POLY:52;
hence  (b1 +^ b2) . z = 0 by A13, A12, A14, XBOOLE_0:def_5; ::_thesis: verum
end;
 dom (b1 +^ b2) = o1 +^ o2 by PARTFUN1:def_2;
then  b1 +^ b2 = (o1 +^ o2) --> 0 by A11, FUNCOP_1:11;
hence  b1 +^ b2 = EmptyBag (o1 +^ o2) by PRE_POLY:def_13; ::_thesis: verum
end;
end;

theorem Th6: :: POLYNOM6:6
for o1, o2 being Ordinal
for c being Element of Bags (o1 +^ o2) ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2
proof
let o1, o2 be Ordinal; ::_thesis: for c being Element of Bags (o1 +^ o2) ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2
let c be Element of Bags (o1 +^ o2); ::_thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2
percases ( o2 is empty or not o2 is empty ) ;
supposeA1: o2 is empty ; ::_thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2
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 ; ::_thesis: ex c2 being Element of Bags o2 st c = c1 +^ c2
take  c2 ; ::_thesis: c = c1 +^ c2
thus  c = c1 +^ c2 by A1, Th3; ::_thesis: verum
end;
supposeA2: not o2 is empty ; ::_thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2
then reconsider o29 = o2 as non empty Ordinal ;
A3: support (c | o1) c= support c
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (c | o1) or x in support c )
assume  x in support (c | o1) ; ::_thesis: x in support c
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  x in support c by A4, PRE_POLY:def_7; ::_thesis: verum
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 H1( Element of o1 +^ o29) ->  set = $1 -^ o1;
defpred S1[ set , set ] means  for x1 being Element of o2 st x1 = $1 holds
$2 = c . (o1 +^ x1);
take  c1 ; ::_thesis: ex c2 being Element of Bags o2 st c = c1 +^ c2
set B =  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }  ;
set C =  {  H1(o9) where o9 is Element of o1 +^ o29 : o9 in support c  }  ;
A5:  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }  c=  {  H1(o9) where o9 is Element of o1 +^ o29 : o9 in support c  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }  or x in  {  H1(o9) where o9 is Element of o1 +^ o29 : o9 in support c  }  )
assume  x in  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }  ; ::_thesis: x in  {  H1(o9) where o9 is Element of o1 +^ o29 : o9 in support c  }
then  ex o9 being Element of o1 +^ o29 st
( x = o9 -^ o1 & o1 c= o9 & o9 in support c ) ;
hence  x in  {  H1(o9) where o9 is Element of o1 +^ o29 : o9 in support c  }  ; ::_thesis: verum
end;
A6: for i being set st i in o2 holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in o2 implies ex j being set st S1[i,j] )
assume  i in o2 ; ::_thesis: ex j being set st S1[i,j]
then reconsider x1 = i as Element of o2 ;
take  c . (o1 +^ x1) ; ::_thesis: S1[i,c . (o1 +^ x1)]
thus  S1[i,c . (o1 +^ x1)] ; ::_thesis: verum
end;
consider f being ManySortedSet of o2 such that
A7: for i being set st i in o2 holds
S1[i,f . i] from PBOOLE:sch_3(A6);
A8: support f c=  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support f or x in  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }  )
assume  x in support f ; ::_thesis: x in  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }
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  x in  {  (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c )  }  by A10; ::_thesis: verum
end;
A11: f is natural-valued
proof
let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom f or f . x is natural )
assume A12: x in dom f ; ::_thesis: f . x is natural
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  f . x is natural ; ::_thesis: verum
end;
A13: support c is finite ;
  {  H1(o9) where o9 is Element of o1 +^ o29 : o9 in support 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 ; ::_thesis: c = c1 +^ c2
now__::_thesis:_for_i_being_set_st_i_in_o1_+^_o2_holds_
c_._i_=_(c1_+^_c2)_._i
let i be set ; ::_thesis: ( i in o1 +^ o2 implies c . b1 = (c1 +^ c2) . b1 )
assume A14: i in o1 +^ o2 ; ::_thesis: c . b1 = (c1 +^ c2) . b1
percases ( i in o1 or i in (o1 +^ o2) \ o1 ) by A14, XBOOLE_0:def_5;
supposeA15: i in o1 ; ::_thesis: c . b1 = (c1 +^ c2) . b1
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 ; ::_thesis: verum
end;
supposeA16: i in (o1 +^ o2) \ o1 ; ::_thesis: c . b1 = (c1 +^ c2) . b1
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 ; ::_thesis: verum
end;
end;
end;
hence  c = c1 +^ c2 by PBOOLE:3; ::_thesis: verum
end;
end;
end;

theorem Th7: :: POLYNOM6:7
for o1, o2 being Ordinal
for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds
( b1 = c1 & b2 = c2 )
proof
let o1, o2 be Ordinal; ::_thesis: for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds
( b1 = c1 & b2 = c2 )
let b1, c1 be Element of Bags o1; ::_thesis: for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds
( b1 = c1 & b2 = c2 )
let b2, c2 be Element of Bags o2; ::_thesis: ( b1 +^ b2 = c1 +^ c2 implies ( b1 = c1 & b2 = c2 ) )
assume A1: b1 +^ b2 = c1 +^ c2 ; ::_thesis: ( b1 = c1 & b2 = c2 )
now__::_thesis:_for_i_being_set_st_i_in_o1_holds_
b1_._i_=_c1_._i
let i be set ; ::_thesis: ( i in o1 implies b1 . i = c1 . i )
assume A2: i in o1 ; ::_thesis: b1 . i = c1 . i
then reconsider i9 = i as Ordinal ;
 (b1 +^ b2) . i9 = b1 . i9 by A2, Def1;
hence  b1 . i = c1 . i by A1, A2, Def1; ::_thesis: verum
end;
hence  b1 = c1 by PBOOLE:3; ::_thesis: b2 = c2
now__::_thesis:_for_i_being_set_st_i_in_o2_holds_
b2_._i_=_c2_._i
let i be set ; ::_thesis: ( i in o2 implies b2 . i = c2 . i )
assume A3: i in o2 ; ::_thesis: b2 . i = c2 . i
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; ::_thesis: verum
end;
hence  b2 = c2 by PBOOLE:3; ::_thesis: verum
end;

theorem Th8: :: POLYNOM6:8
for n being Ordinal
for L being non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr
for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr
for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)
let L be non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr ; ::_thesis: for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)
let p, q, r be Series of n,L; ::_thesis: (p + q) *' r = (p *' r) + (q *' r)
set cL = the carrier of L;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_((p_+_q)_*'_r)_._b_=_((p_*'_r)_+_(q_*'_r))_._b
let b be Element of Bags n; ::_thesis: ((p + q) *' r) . b = ((p *' r) + (q *' r)) . b
consider s being FinSequence of the carrier of L such that
A1: ((p + q) *' r) . b = Sum s and
A2: len s = len (decomp b) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((p + q) . b1) * (r . b2) ) by POLYNOM1:def_9;
consider u being FinSequence of the carrier of L such that
A4: (q *' r) . b = Sum u and
A5: len u = len (decomp b) and
A6: for k being Element of NAT st k in dom u holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & u /. k = (q . b1) * (r . b2) ) by POLYNOM1:def_9;
consider t being FinSequence of the carrier of L such that
A7: (p *' r) . b = Sum t and
A8: len t = len (decomp b) and
A9: for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & t /. k = (p . b1) * (r . b2) ) by POLYNOM1:def_9;
reconsider t = t, u = u as Element of (len s) -tuples_on the carrier of L 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__::_thesis:_for_i_being_Nat_st_i_in_dom_s_holds_
s_._i_=_(t_+_u)_._i
let i be Nat; ::_thesis: ( i in dom s implies s . i = (t + u) . i )
assume A14: i in dom s ; ::_thesis: s . i = (t + u) . i
then consider sb1, sb2 being 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 being 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 being 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 ;
::_thesis: verum
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 ;
::_thesis: verum
end;
hence  (p + q) *' r = (p *' r) + (q *' r) by FUNCT_2:63; ::_thesis: verum
end;

begin

registration
let n be Ordinal;
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
cluster Polynom-Ring (n,L) ->  non trivial distributive ;
coherence
 ( not Polynom-Ring (n,L) is trivial & Polynom-Ring (n,L) is distributive )
proof
thus  not Polynom-Ring (n,L) is trivial ::_thesis: Polynom-Ring (n,L) is distributive
proof
take  1_ (Polynom-Ring (n,L)) ; :: according to STRUCT_0:def_18 ::_thesis: not 1_ (Polynom-Ring (n,L)) = 0. (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_10;
hence  not 1_ (Polynom-Ring (n,L)) = 0. (Polynom-Ring (n,L)) by A1, POLYNOM1:25; ::_thesis: verum
end;
thus  Polynom-Ring (n,L) is distributive ::_thesis: verum
proof
let x, y, z be Element of (Polynom-Ring (n,L)); :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider u = x, v = y, w = z as Polynomial of n,L by POLYNOM1:def_10;
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_10;
 y9 + z9 = v + w by POLYNOM1:def_10;
hence x * (y + z) = u *' (v + w) by POLYNOM1:def_10
.= (u *' v) + (u *' w) by POLYNOM1:26
.= (x * y) + (x * z) by A2, POLYNOM1:def_10 ;
::_thesis: (y + z) * x = (y * x) + (z * x)
A3: ( v *' u = y9 * x9 & w *' u = z9 * x9 ) by POLYNOM1:def_10;
 y9 + z9 = v + w by POLYNOM1:def_10;
hence (y + z) * x = (v + w) *' u by POLYNOM1:def_10
.= (v *' u) + (w *' u) by Th8
.= (y * x) + (z * x) by A3, POLYNOM1:def_10 ;
::_thesis: verum
end;
end;
end;

definition
let o1, o2 be non empty Ordinal;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let P be Polynomial of o1,(Polynom-Ring (o2,L));
func Compress P ->  Polynomial of (o1 +^ o2),L means :Def2: :: POLYNOM6:def 2
 for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & it . b = Q1 . b2 );
existence
 ex b1 being Polynomial of (o1 +^ o2),L st
for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b1 . b = Q1 . b2 )
proof
deffunc H1( Element of Bags o1) ->  set =  {  ($1 +^ b2) where b2 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . $1 & b2 in Support Q )  }  ;
defpred S1[ Element of Bags (o1 +^ o2), Element of L] means  ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & $1 = b1 +^ b2 & $2 = Q1 . b2 );
set A =  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  ;
A1: for B being set st B in  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  holds
B is finite
proof
let B be set ; ::_thesis: ( B in  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  implies B is finite )
assume  B in  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  ; ::_thesis: B is finite
then consider b1 being Element of Bags o1 such that
A2: B =  {  (b1 +^ b2) where b2 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q )  }  and
 b1 in Support P ;
deffunc H2( Element of Bags o2) ->  Element of Bags (o1 +^ o2) = b1 +^ $1;
reconsider Q0 = P . b1 as Polynomial of o2,L by POLYNOM1:def_10;
set B0 =  {  H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0  }  ;
A3: B c=  {  H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in  {  H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0  }  )
assume  x in B ; ::_thesis: x in  {  H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0  }
then  ex b2 being Element of Bags o2 st
( x = b1 +^ b2 & ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) ) by A2;
hence  x in  {  H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0  }  ; ::_thesis: verum
end;
A4: Support Q0 is finite ;
  {  H2(b2) where b2 is Element of Bags o2 : b2 in Support Q0  }  is finite from FRAENKEL:sch_21(A4);
hence  B is finite by A3; ::_thesis: verum
end;
A5: for b being Element of Bags (o1 +^ o2) ex u being Element of L st S1[b,u]
proof
let b be Element of Bags (o1 +^ o2); ::_thesis: ex u being Element of L st S1[b,u]
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A6: b = b1 +^ b2 by Th6;
reconsider Q1 = P . b1 as Polynomial of o2,L by POLYNOM1:def_10;
take  Q1 . b2 ; ::_thesis: S1[b,Q1 . b2]
take  b1 ; ::_thesis: ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 )
take  b2 ; ::_thesis: ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 )
take  Q1 ; ::_thesis: ( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 )
thus  ( Q1 = P . b1 & b = b1 +^ b2 & Q1 . b2 = Q1 . b2 ) by A6; ::_thesis: verum
end;
consider f being Function of (Bags (o1 +^ o2)), the carrier of L such that
A7: for b being Element of Bags (o1 +^ o2) holds S1[b,f . b] from FUNCT_2:sch_3(A5);
reconsider f = f as Series of (o1 +^ o2),L ;
A8: Support f = union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }
proof
thus  Support f c= union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  :: according to XBOOLE_0:def_10 ::_thesis: union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  c= Support f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support f or x in union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  )
assume A9: x in Support f ; ::_thesis: x in union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }
then A10: f . x <> 0. L by POLYNOM1:def_3;
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A11: x = b1 +^ b2 by A9, Th6;
consider Y being set  such that
A12: Y =  {  (b1 +^ b29) where b29 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . b1 & b29 in Support Q )  }  ;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q1 being 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__::_thesis:_not_P_._b1_=_0._(Polynom-Ring_(o2,L))
assume  P . b1 = 0. (Polynom-Ring (o2,L)) ; ::_thesis: contradiction
then  Q1 = 0_ (o2,L) by A13, A16, POLYNOM1:def_10;
hence  contradiction by A10, A11, A15, POLYNOM1:22; ::_thesis: verum
end;
then  b1 in Support P by POLYNOM1:def_3;
then A17: Y in  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  by A12;
 b2 = b29 by A14, Th7;
then  b2 in Support Q1 by A10, A11, A15, POLYNOM1:def_3;
then  x in Y by A11, A12, A13, A16;
hence  x in union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  by A17, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  or x in Support f )
assume  x in union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  ; ::_thesis: x in Support f
then consider Y being set  such that
A18: x in Y and
A19: Y in  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  by TARSKI:def_4;
consider b1 being Element of Bags o1 such that
A20: Y =  {  (b1 +^ b2) where b2 is Element of Bags o2 : ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q )  }  and
 b1 in Support P by A19;
consider b2 being Element of Bags o2 such that
A21: x = b1 +^ b2 and
A22: ex Q being Polynomial of o2,L st
( Q = P . b1 & b2 in Support Q ) by A18, A20;
consider Q being 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_3;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q1 being 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  x in Support f by A21, A25, A29, POLYNOM1:def_3; ::_thesis: verum
end;
A30: Support P is finite by POLYNOM1:def_4;
  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  is finite from FRAENKEL:sch_21(A30);
then  union  {  H1(b1) where b1 is Element of Bags o1 : b1 in Support P  }  is finite by A1, FINSET_1:7;
then reconsider f = f as Polynomial of (o1 +^ o2),L by A8, POLYNOM1:def_4;
take  f ; ::_thesis: for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
let b be Element of Bags (o1 +^ o2); ::_thesis: ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q19 being 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 being Element of Bags o1, b2 being Element of Bags o2 such that
A34: b = b1 +^ b2 by Th6;
reconsider Q1 = P . b1 as Polynomial of o2,L by POLYNOM1:def_10;
take  b1 ; ::_thesis: ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
take  b2 ; ::_thesis: ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
take  Q1 ; ::_thesis: ( Q1 = P . b1 & b = b1 +^ b2 & f . b = Q1 . b2 )
thus  Q1 = P . b1 ; ::_thesis: ( b = b1 +^ b2 & f . b = Q1 . b2 )
thus  b = b1 +^ b2 by A34; ::_thesis: f . b = Q1 . b2
 b1 = b19 by A34, A32, Th7;
hence  f . b = Q1 . b2 by A34, A31, A32, A33, Th7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Polynomial of (o1 +^ o2),L st ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b1 . b = Q1 . b2 ) ) & ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b2 . b = Q1 . b2 ) ) holds
b1 = b2
proof
let w1, w2 be Polynomial of (o1 +^ o2),L; ::_thesis: ( ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w1 . b = Q1 . b2 ) ) & ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w2 . b = Q1 . b2 ) ) implies w1 = w2 )
assume that
A35: for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w1 . b = Q1 . b2 ) and
A36: for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w2 . b = Q1 . b2 ) ; ::_thesis: w1 = w2
 for c being Element of Bags (o1 +^ o2) holds w1 . c = w2 . c
proof
let c be Element of Bags (o1 +^ o2); ::_thesis: w1 . c = w2 . c
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1 being 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 being Element of Bags o1, d2 being Element of Bags o2, S1 being 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  w1 . c = w2 . c by A37, A38, A39, A40, A41, A42, Th7; ::_thesis: verum
end;
hence  w1 = w2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Compress POLYNOM6:def_2_:_
 for o1, o2 being non empty Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for P being Polynomial of o1,(Polynom-Ring (o2,L))
for b5 being Polynomial of (o1 +^ o2),L holds
( b5 = Compress P iff for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b5 . b = Q1 . b2 ) );

theorem Th9: :: POLYNOM6:9
for o1, o2 being Ordinal
for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 divides c1 & b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2
proof
let o1, o2 be Ordinal; ::_thesis: for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 divides c1 & b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2
let b1, c1 be Element of Bags o1; ::_thesis: for b2, c2 being Element of Bags o2 st b1 divides c1 & b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2
let b2, c2 be Element of Bags o2; ::_thesis: ( b1 divides c1 & b2 divides c2 implies b1 +^ b2 divides c1 +^ c2 )
assume that
A1: b1 divides c1 and
A2: b2 divides c2 ; ::_thesis: b1 +^ b2 divides c1 +^ c2
now__::_thesis:_for_k_being_set_st_k_in_o1_+^_o2_holds_
(b1_+^_b2)_._k_<=_(c1_+^_c2)_._k
reconsider b19 = b1, c19 = c1 as bag of o1 ;
let k be set ; ::_thesis: ( k in o1 +^ o2 implies (b1 +^ b2) . b1 <= (c1 +^ c2) . b1 )
A3: b19 . k <= c19 . k by A1, PRE_POLY:def_11;
assume A4: k in o1 +^ o2 ; ::_thesis: (b1 +^ b2) . b1 <= (c1 +^ c2) . b1
percases ( k in o1 or k in (o1 +^ o2) \ o1 ) by A4, XBOOLE_0:def_5;
supposeA5: k in o1 ; ::_thesis: (b1 +^ b2) . b1 <= (c1 +^ c2) . b1
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; ::_thesis: verum
end;
supposeA6: k in (o1 +^ o2) \ o1 ; ::_thesis: (b1 +^ b2) . b1 <= (c1 +^ c2) . b1
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; ::_thesis: verum
end;
end;
end;
hence  b1 +^ b2 divides c1 +^ c2 by PRE_POLY:46; ::_thesis: verum
end;

theorem Th10: :: POLYNOM6:10
for o1, o2 being Ordinal
for b being bag of o1 +^ o2
for b1 being Element of Bags o1
for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
proof
let o1, o2 be Ordinal; ::_thesis: for b being bag of o1 +^ o2
for b1 being Element of Bags o1
for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
let b be bag of o1 +^ o2; ::_thesis: for b1 being Element of Bags o1
for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
let b1 be Element of Bags o1; ::_thesis: for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
let b2 be Element of Bags o2; ::_thesis: ( b divides b1 +^ b2 implies ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 ) )
reconsider b9 = b as Element of Bags (o1 +^ o2) by PRE_POLY:def_12;
consider c1 being Element of Bags o1, c2 being 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 ; ::_thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
A3: for k being set st k in o2 holds
c29 . k <= b29 . k
proof
let k be set ; ::_thesis: ( k in o2 implies c29 . k <= b29 . k )
assume A4: k in o2 ; ::_thesis: c29 . k <= b29 . k
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) . (o1 +^ k9) <= (b1 +^ b2) . (o1 +^ k9) & 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  c29 . k <= b29 . k by A7, A6, Def1; ::_thesis: verum
end;
take  c1 ; ::_thesis: ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
take  c2 ; ::_thesis: ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )
 for k being set st k in o1 holds
c19 . k <= b19 . k
proof
let k be set ; ::_thesis: ( k in o1 implies c19 . k <= b19 . k )
assume A8: k in o1 ; ::_thesis: c19 . k <= b19 . k
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  c19 . k <= b19 . k by A8, A9, Def1; ::_thesis: verum
end;
hence  ( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 ) by A1, A3, PRE_POLY:46; ::_thesis: verum
end;

theorem Th11: :: POLYNOM6:11
for o1, o2 being Ordinal
for a1, b1 being Element of Bags o1
for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )
proof
let o1, o2 be Ordinal; ::_thesis: for a1, b1 being Element of Bags o1
for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )
let a1, b1 be Element of Bags o1; ::_thesis: for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )
let a2, b2 be Element of Bags o2; ::_thesis: ( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )
thus  ( not a1 +^ a2 < b1 +^ b2 or a1 < b1 or ( a1 = b1 & a2 < b2 ) ) ::_thesis: ( ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) implies a1 +^ a2 < b1 +^ b2 )
proof
assume  a1 +^ a2 < b1 +^ b2 ; ::_thesis: ( a1 < b1 or ( a1 = b1 & a2 < b2 ) )
then consider k being Ordinal such that
A1: (a1 +^ a2) . k < (b1 +^ b2) . k and
A2: for l being Ordinal st l in k holds
(a1 +^ a2) . l = (b1 +^ b2) . l by PRE_POLY:def_9;
now__::_thesis:_k_in_dom_(b1_+^_b2)
assume  not k in dom (b1 +^ b2) ; ::_thesis: contradiction
then  (b1 +^ b2) . k = 0 by FUNCT_1:def_2;
hence  contradiction by A1, NAT_1:2; ::_thesis: verum
end;
then A3: k in o1 +^ o2 by PARTFUN1:def_2;
now__::_thesis:_(_(_k_in_o1_&_a1_<_b1_)_or_(_k_in_(o1_+^_o2)_\_o1_&_a1_=_b1_&_a2_<_b2_)_)
percases ( k in o1 or k in (o1 +^ o2) \ o1 ) by A3, XBOOLE_0:def_5;
caseA4: k in o1 ; ::_thesis: a1 < b1
reconsider a19 = a1, b19 = b1 as bag of o1 ;
A5: for l being Ordinal st l in k holds
a19 . l = b19 . l
proof
let l be Ordinal; ::_thesis: ( l in k implies a19 . l = b19 . l )
assume A6: l in k ; ::_thesis: a19 . l = b19 . l
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  a19 . l = b19 . l by A7, A8, Def1; ::_thesis: verum
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; ::_thesis: verum
end;
caseA9: k in (o1 +^ o2) \ o1 ; ::_thesis: ( a1 = b1 & a2 < b2 )
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 being Ordinal st l in k -^ o1 holds
a2 . l = b2 . l
proof
let l be Ordinal; ::_thesis: ( l in k -^ o1 implies a2 . l = b2 . l )
 o1 c= o1 +^ l by ORDINAL3:24;
then A12: not o1 +^ l in o1 by ORDINAL1:5;
assume A13: l in k -^ o1 ; ::_thesis: a2 . l = b2 . l
then  o1 +^ l in o1 +^ (k -^ o1) 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  a2 . l = b2 . l by A2, A10, A13, A15, ORDINAL2:32; ::_thesis: verum
end;
 for i being set 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 set ; ::_thesis: ( i in o1 implies a1 . i = b1 . i )
assume A17: i in o1 ; ::_thesis: a1 . i = b1 . i
then reconsider i9 = i as Ordinal ;
 ( (a1 +^ a2) . i9 = a1 . i9 & (b1 +^ b2) . i9 = b1 . i9 ) by A17, Def1;
hence  a1 . i = b1 . i by A2, A17, A16; ::_thesis: verum
end;
hence  a1 = b1 by PBOOLE:3; ::_thesis: a2 < b2
 (a1 +^ a2) . k = a2 . (k -^ o1) by A9, Def1;
then  a2 . (k -^ o1) < b2 . (k -^ o1) by A1, A9, Def1;
hence  a2 < b2 by A11, PRE_POLY:def_9; ::_thesis: verum
end;
end;
end;
hence  ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) ; ::_thesis: verum
end;
thus  ( ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) implies a1 +^ a2 < b1 +^ b2 ) ::_thesis: verum
proof
assume A18: ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) ; ::_thesis: a1 +^ a2 < b1 +^ b2
now__::_thesis:_(_(_a1_<_b1_&_a1_+^_a2_<_b1_+^_b2_)_or_(_not_a1_<_b1_&_a1_+^_a2_<_b1_+^_b2_)_)
percases ( a1 < b1 or not a1 < b1 ) ;
case a1 < b1 ; ::_thesis: a1 +^ a2 < b1 +^ b2
then consider k being Ordinal such that
A19: k in o1 and
A20: a1 . k < b1 . k and
A21: for l being Ordinal st l in k holds
a1 . l = b1 . l by Th2;
A22: for l being Ordinal st l in k holds
(a1 +^ a2) . l = (b1 +^ b2) . l
proof
let l be Ordinal; ::_thesis: ( l in k implies (a1 +^ a2) . l = (b1 +^ b2) . l )
assume A23: l in k ; ::_thesis: (a1 +^ a2) . l = (b1 +^ b2) . l
then  l in o1 by A19, ORDINAL1:10;
then  ( (a1 +^ a2) . l = a1 . l & (b1 +^ b2) . l = b1 . l ) by Def1;
hence  (a1 +^ a2) . l = (b1 +^ b2) . l by A21, A23; ::_thesis: verum
end;
 ( (a1 +^ a2) . k = a1 . k & (b1 +^ b2) . k = b1 . k ) by A19, Def1;
hence  a1 +^ a2 < b1 +^ b2 by A20, A22, PRE_POLY:def_9; ::_thesis: verum
end;
caseA24: not a1 < b1 ; ::_thesis: a1 +^ a2 < b1 +^ b2
then consider k being Ordinal such that
A25: k in o2 and
A26: a2 . k < b2 . k and
A27: for l being Ordinal st l in k holds
a2 . l = b2 . l by A18, Th2;
set x = o1 +^ k;
A28: for l being Ordinal st l in o1 +^ k holds
(a1 +^ a2) . l = (b1 +^ b2) . l
proof
let l be Ordinal; ::_thesis: ( l in o1 +^ k implies (a1 +^ a2) . l = (b1 +^ b2) . l )
assume A29: l in o1 +^ k ; ::_thesis: (a1 +^ a2) . l = (b1 +^ b2) . l
percases ( l in o1 or not l in o1 ) ;
supposeA30: l in o1 ; ::_thesis: (a1 +^ a2) . l = (b1 +^ b2) . l
hence (a1 +^ a2) . l = b1 . l by A18, A24, Def1
.= (b1 +^ b2) . l by A30, Def1 ;
::_thesis: verum
end;
supposeA31: not l in o1 ; ::_thesis: (a1 +^ a2) . l = (b1 +^ b2) . l
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 ;
::_thesis: verum
end;
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) . (o1 +^ k) < (b1 +^ b2) . (o1 +^ k) by A26, A36, A35, Def1;
hence  a1 +^ a2 < b1 +^ b2 by A28, PRE_POLY:def_9; ::_thesis: verum
end;
end;
end;
hence  a1 +^ a2 < b1 +^ b2 ; ::_thesis: verum
end;
end;

theorem Th12: :: POLYNOM6:12
for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (Bags (o1 +^ o2)) * st dom G = dom (divisors b1) & ( for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G
proof
let o1, o2 be Ordinal; ::_thesis: for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (Bags (o1 +^ o2)) * st dom G = dom (divisors b1) & ( for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G
let b1 be Element of Bags o1; ::_thesis: for b2 being Element of Bags o2
for G being FinSequence of (Bags (o1 +^ o2)) * st dom G = dom (divisors b1) & ( for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G
let b2 be Element of Bags o2; ::_thesis: for G being FinSequence of (Bags (o1 +^ o2)) * st dom G = dom (divisors b1) & ( for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G
let G be FinSequence of (Bags (o1 +^ o2)) * ; ::_thesis: ( dom G = dom (divisors b1) & ( for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) implies divisors (b1 +^ b2) = FlattenSeq G )
assume that
A1: dom G = dom (divisors b1) and
A2: for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ; ::_thesis: divisors (b1 +^ b2) = FlattenSeq G
reconsider D = Del (G,1) as FinSequence of (Bags (o1 +^ o2)) * ;
consider a19 being Element of Bags o1, Fk being 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 being Nat st m in dom Fk holds
ex a199 being 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: not G is 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, POLYALG1:4;
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 being Nat st n in dom (FlattenSeq G) & m in dom (FlattenSeq G) & n < m holds
( (FlattenSeq G) /. n <> (FlattenSeq G) /. m & [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) )
proof
let n, m be Nat; ::_thesis: ( n in dom (FlattenSeq G) & m in dom (FlattenSeq G) & n < m implies ( (FlattenSeq G) /. n <> (FlattenSeq G) /. m & [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) ) )
assume that
A9: n in dom (FlattenSeq G) and
A10: m in dom (FlattenSeq G) and
A11: n < m ; ::_thesis: ( (FlattenSeq G) /. n <> (FlattenSeq G) /. m & [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) )
A12: (FlattenSeq G) /. n = (FlattenSeq G) . n by A9, PARTFUN1:def_6;
consider i1, j1 being Element of 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 being Element of Bags o1, Fk being 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 being Nat st r in dom Fk holds
ex a199 being 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 being 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__::_thesis:_not_(FlattenSeq_G)_/._n_=_(FlattenSeq_G)_/._m
consider i2, j2 being Element of 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 being Element of Bags o1, Fk9 being 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 being Nat st r in dom Fk9 holds
ex a299 being 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 being 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 being Element of 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 being Element of Bags o1, Fk being 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 being Nat st r in dom Fk holds
ex a199 being 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 being 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: (FlattenSeq G) /. n = (FlattenSeq G) /. m ; ::_thesis: contradiction
A56: ( (FlattenSeq G) /. n = (FlattenSeq G) . n & (FlattenSeq G) /. m = (FlattenSeq G) . 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; ::_thesis: verum
end;
hence  (FlattenSeq G) /. n <> (FlattenSeq G) /. m ; ::_thesis: [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2)
reconsider Fn = (FlattenSeq G) /. n, Fm = (FlattenSeq G) /. m as bag of o1 +^ o2 ;
reconsider Fn9 = Fn, Fm9 = Fm as Element of Bags (o1 +^ o2) ;
consider a1 being Element of Bags o1, a2 being 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: (FlattenSeq G) /. m = (FlattenSeq G) . m by A10, PARTFUN1:def_6;
consider c1 being Element of Bags o1, c2 being Element of Bags o2 such that
A65: Fm9 = c1 +^ c2 by Th6;
consider i2, j2 being Element of 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 being Element of Bags o1, Fk9 being 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 being Nat st r in dom Fk9 holds
ex a299 being 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 being 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__::_thesis:_(_(_i1_<_i2_&_a1_<_c1_)_or_(_i1_=_i2_&_j1_<_j2_&_a1_=_c1_&_a2_<_c2_)_)
A83: now__::_thesis:_(_not_i1_<_i2_implies_(_i1_=_i2_&_j1_<_j2_)_)
assume that
A84: not i1 < i2 and
A85: ( not i1 = i2 or not j1 < j2 ) ; ::_thesis: contradiction
percases ( i1 = i2 or i1 > i2 ) by A84, XXREAL_0:1;
suppose i1 = i2 ; ::_thesis: contradiction
hence  contradiction by A11, A15, A68, A85, XREAL_1:6; ::_thesis: verum
end;
supposeA86: i1 > i2 ; ::_thesis: contradiction
 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, POLYNOM3:19;
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; ::_thesis: verum
end;
end;
end;
consider S being non empty finite Subset of (Bags o1) such that
A94: divisors b1 = SgmX ((BagOrder o1),S) and
 for p being 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 being non empty finite Subset of (Bags o2) such that
A96: divisors b2 = SgmX ((BagOrder o2),T) and
 for p being 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;
percases ( i1 < i2 or ( i1 = i2 & j1 < j2 ) ) by A83;
caseA98: i1 < i2 ; ::_thesis: a1 < c1
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; ::_thesis: verum
end;
casethat A100: i1 = i2 and
A101: j1 < j2 ; ::_thesis: ( a1 = c1 & a2 < c2 )
 [((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; ::_thesis: a2 < c2
 a2 <> c2 by A24, A63, A77, A82, A101, FUNCT_1:def_4;
hence  a2 < c2 by A102, PRE_POLY:def_10; ::_thesis: verum
end;
end;
end;
then  ( Fn < Fm or Fn = Fm ) by A58, A65, Th11;
then  Fn <=' Fm by PRE_POLY:def_10;
hence  [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) by PRE_POLY:def_14; ::_thesis: verum
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 being bag of o1 +^ o2 holds
( p in S iff p divides b1 +^ b2 )
proof
consider W being non empty finite Subset of (Bags o2) such that
A104: divisors b2 = SgmX ((BagOrder o2),W) and
A105: for q being 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; ::_thesis: ( p in S iff p divides b1 +^ b2 )
consider T being non empty finite Subset of (Bags o1) such that
A107: divisors b1 = SgmX ((BagOrder o1),T) and
A108: for q being 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 ) ::_thesis: ( p divides b1 +^ b2 implies p in S )
proof
assume  p in S ; ::_thesis: p divides b1 +^ b2
then consider x being set  such that
A110: x in dom (FlattenSeq G) and
A111: p = (FlattenSeq G) . x by FUNCT_1:def_3;
consider i, j being Element of 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 being Element of Bags o1, Fk being 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 being Nat st m in dom Fk holds
ex a199 being 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 being 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  p divides b1 +^ b2 by A119, A124, Th9; ::_thesis: verum
end;
thus  ( p divides b1 +^ b2 implies p in S ) ::_thesis: verum
proof
assume  p divides b1 +^ b2 ; ::_thesis: p in S
then consider p1 being Element of Bags o1, p2 being 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 being set  such that
A128: i in dom (divisors b1) and
A129: p1 = (divisors b1) . i by A107, A109, FUNCT_1:def_3;
reconsider i = i as Element of NAT by A128;
consider a19 being Element of Bags o1, Fk being 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 being Nat st m in dom Fk holds
ex a199 being 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 being set  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 = j as Element of NAT by A135;
A139: G /. i = G . i by A1, A128, PARTFUN1:def_6;
then consider a199 being 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  p in S by A127, A143, A134, A142, FUNCT_1:def_3; ::_thesis: verum
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  divisors (b1 +^ b2) = FlattenSeq G by A103, PRE_POLY:def_16; ::_thesis: verum
end;

theorem Th13: :: POLYNOM6:13
for o1, o2 being Ordinal
for a1, b1, c1 being Element of Bags o1
for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
proof
let o1, o2 be Ordinal; ::_thesis: for a1, b1, c1 being Element of Bags o1
for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
let a1, b1, c1 be Element of Bags o1; ::_thesis: for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
let a2, b2, c2 be Element of Bags o2; ::_thesis: ( c1 = b1 -' a1 & c2 = b2 -' a2 implies (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2 )
assume that
A1: c1 = b1 -' a1 and
A2: c2 = b2 -' a2 ; ::_thesis: (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
reconsider w = (b1 +^ b2) -' (a1 +^ a2) as Element of Bags (o1 +^ o2) by PRE_POLY:def_12;
 for o being 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; ::_thesis: ( ( o in o1 implies w . o = c1 . o ) & ( o in (o1 +^ o2) \ o1 implies w . o = c2 . (o -^ o1) ) )
hereby  ::_thesis: ( o in (o1 +^ o2) \ o1 implies w . o = c2 . (o -^ o1) )
assume A3: o in o1 ; ::_thesis: w . o = c1 . o
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 ; ::_thesis: verum
end;
assume A4: o in (o1 +^ o2) \ o1 ; ::_thesis: w . o = c2 . (o -^ 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 ; ::_thesis: verum
end;
hence  (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2 by Def1; ::_thesis: verum
end;

theorem Th14: :: POLYNOM6:14
for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G
proof
let o1, o2 be Ordinal; ::_thesis: for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G
let b1 be Element of Bags o1; ::_thesis: for b2 being Element of Bags o2
for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G
let b2 be Element of Bags o2; ::_thesis: for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G
let G be FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * ; ::_thesis: ( dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) implies decomp (b1 +^ b2) = FlattenSeq G )
assume that
A1: dom G = dom (decomp b1) and
A2: for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ; ::_thesis: decomp (b1 +^ b2) = FlattenSeq G
defpred S1[ set , Function] means ( dom $2 = dom (G . $1) & ( for j being Nat st j in dom $2 holds
ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . $1) . j & $2 . j = p . 1 ) ) );
A3: for k being Element of NAT st k in Seg (len G) holds
ex p being Element of (Bags (o1 +^ o2)) * st S1[k,p]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len G) implies ex p being Element of (Bags (o1 +^ o2)) * st S1[k,p] )
assume A4: k in Seg (len G) ; ::_thesis: ex p being Element of (Bags (o1 +^ o2)) * st S1[k,p]
defpred S2[ set , set ] means  ex q being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( q = (G . k) . $1 & $2 = q . 1 );
A5: for j being Element of NAT st j in Seg (len (G . k)) holds
ex x being Element of Bags (o1 +^ o2) st S2[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 Element of NAT ; ::_thesis: ( j in Seg (len (G . k)) implies ex x being Element of Bags (o1 +^ o2) st S2[j,x] )
assume  j in Seg (len (G . k)) ; ::_thesis: ex x being Element of Bags (o1 +^ o2) st S2[j,x]
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 being 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 ; ::_thesis: S2[j,x]
thus  S2[j,x] ; ::_thesis: verum
end;
consider p being FinSequence of Bags (o1 +^ o2) such that
A7: dom p = Seg (len (G . k)) and
A8: for j being Element of NAT st j in Seg (len (G . k)) holds
S2[j,p /. j] from RECDEF_1:sch_17(A5);
reconsider p = p as Element of (Bags (o1 +^ o2)) * by FINSEQ_1:def_11;
take  p ; ::_thesis: S1[k,p]
thus  dom p = dom (G . k) by A7, FINSEQ_1:def_3; ::_thesis: for j being Nat st j in dom p holds
ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . k) . j & p . j = p . 1 )
let j be Nat; ::_thesis: ( j in dom p implies ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . k) . j & p . j = p . 1 ) )
assume A9: j in dom p ; ::_thesis: ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . k) . j & p . j = p . 1 )
then consider q being 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 ; ::_thesis: ( q = (G . k) . j & p . j = q . 1 )
thus  q = (G . k) . j by A10; ::_thesis: p . j = q . 1
thus  p . j = q . 1 by A9, A11, PARTFUN1:def_6; ::_thesis: verum
end;
consider F being FinSequence of (Bags (o1 +^ o2)) *  such that
A12: dom F = Seg (len G) and
A13: for i being Element of NAT st i in Seg (len G) holds
S1[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 being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) )
proof
let i be Nat; ::_thesis: ( i in dom (divisors b1) implies ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) )
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) ; ::_thesis: ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) )
then consider a19, b19 being Element of Bags o1, Gi being 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 being Nat st m in dom Gi holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Gi /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) by A2, A15;
take  a19 ; ::_thesis: ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) )
take  Fk ; ::_thesis: ( Fk = F /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) )
thus  Fk = F /. i ; ::_thesis: ( (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) )
thus  (divisors b1) /. i = a19 by A15, A18, A20, PRE_POLY:70; ::_thesis: ( len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) )
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 ;
::_thesis: for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 )
let m be Nat; ::_thesis: ( m in dom Fk implies ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) )
assume A25: m in dom Fk ; ::_thesis: ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 )
then consider p being 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 being 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 ; ::_thesis: ( (divisors b2) /. m = a199 & Fk /. m = a19 +^ 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; ::_thesis: Fk /. m = a19 +^ a199
thus Fk /. m = Fk . m by A25, PARTFUN1:def_6
.= a19 +^ a199 by A27, A31, FINSEQ_1:44 ; ::_thesis: verum
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 being Nat st j in dom (Card F) holds
(Card F) . j = (Card G) . j
proof
let j be Nat; ::_thesis: ( j in dom (Card F) implies (Card F) . j = (Card G) . j )
assume A34: j in dom (Card F) ; ::_thesis: (Card F) . j = (Card G) . j
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 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. j & (divisors b1) /. j = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) & ex a29, b29 being Element of Bags o1 ex Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Gk = G /. j & (decomp b1) /. j = <*a29,b29*> & len Gk = len (decomp b2) & ( for m being Nat st m in dom Gk holds
ex a299, b299 being 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  (Card F) . j = (Card G) . j by A35, A37, CARD_3:def_2; ::_thesis: verum
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 being Element of NAT
for p being 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 ; ::_thesis: for p being bag of o1 +^ o2 st k in dom FG & p = (divisors bb) /. k holds
FG /. k = <*p,(bb -' p)*>
let p be bag of o1 +^ o2; ::_thesis: ( k in dom FG & p = (divisors bb) /. k implies FG /. k = <*p,(bb -' p)*> )
assume that
A44: k in dom FG and
A45: p = (divisors bb) /. k ; ::_thesis: FG /. k = <*p,(bb -' p)*>
consider i, j being Element of 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 being Element of Bags o1, Fk being 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 being Nat st m in dom Fk holds
ex fa19 being Element of Bags o2 st
( (divisors b2) /. m = fa19 & Fk /. m = fa1 +^ fa19 ) by A1, A16, A42, A46;
consider a19, b19 being Element of Bags o1, Gi being 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 being Nat st m in dom Gi holds
ex a199, b199 being 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 being 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 being Element of 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 being 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 ; ::_thesis: verum
end;
 dom FG = dom (divisors bb) by A41, A40, FINSEQ_3:29;
hence  decomp (b1 +^ b2) = FlattenSeq G by A43, PRE_POLY:def_17; ::_thesis: verum
end;

theorem :: POLYNOM6:15
for o1, o2 being non empty Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic
proof
let o1, o2 be non empty Ordinal; ::_thesis: for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic
set P2 = Polynom-Ring ((o1 +^ o2),L);
set P1 = Polynom-Ring (o1,(Polynom-Ring (o2,L)));
defpred S1[ set , set ] means  for P being Polynomial of o1,(Polynom-Ring (o2,L)) st $1 = P holds
$2 = Compress P;
reconsider 1P1 = 1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def_10;
reconsider 1P2 = 1_ (Polynom-Ring ((o1 +^ o2),L)) as Polynomial of (o1 +^ o2),L by POLYNOM1:def_10;
A1: for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ex u being Element of (Polynom-Ring ((o1 +^ o2),L)) st S1[x,u]
proof
let x be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); ::_thesis: ex u being Element of (Polynom-Ring ((o1 +^ o2),L)) st S1[x,u]
reconsider Q = x as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def_10;
reconsider u = Compress Q as Element of (Polynom-Ring ((o1 +^ o2),L)) by POLYNOM1:def_10;
take  u ; ::_thesis: S1[x,u]
let P be Polynomial of o1,(Polynom-Ring (o2,L)); ::_thesis: ( x = P implies u = Compress P )
assume  x = P ; ::_thesis: u = Compress P
hence  u = Compress P ; ::_thesis: verum
end;
consider f being Function of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L)) such that
A2: for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) holds S1[x,f . x] from FUNCT_2:sch_3(A1);
reconsider f = f as Function of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))),(Polynom-Ring ((o1 +^ o2),L)) ;
take  f ; :: according to QUOFIELD:def_23 ::_thesis: f is RingIsomorphism
thus A3: f is additive :: according to QUOFIELD:def_18,QUOFIELD:def_20,QUOFIELD:def_21 ::_thesis: ( f is multiplicative & f is unity-preserving & f is one-to-one & f is RingEpimorphism )
proof
let x, y be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); :: according to VECTSP_1:def_20 ::_thesis: f . (x + y) = (f . x) + (f . y)
reconsider x9 = x, y9 = y as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ;
reconsider p = x9, q = y9 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def_10;
reconsider fp = f . x, fq = f . y, fpq = f . (x + y) as Element of (Polynom-Ring ((o1 +^ o2),L)) ;
reconsider fp = fp, fq = fq, fpq = fpq as Polynomial of (o1 +^ o2),L by POLYNOM1:def_10;
 for x being bag of o1 +^ o2 holds fpq . x = (fp . x) + (fq . x)
proof
let b be bag of o1 +^ o2; ::_thesis: fpq . b = (fp . b) + (fq . b)
reconsider b9 = b as Element of Bags (o1 +^ o2) by PRE_POLY:def_12;
consider b1 being Element of Bags o1, b2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A4: Q1 = p . b1 and
A5: b9 = b1 +^ b2 and
A6: (Compress p) . b9 = Q1 . b2 by Def2;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q19 being Polynomial of o2,L such that
A7: Q19 = q . b19 and
A8: b9 = b19 +^ b29 and
A9: (Compress q) . b9 = Q19 . b29 by Def2;
consider b199 being Element of Bags o1, b299 being Element of Bags o2, Q199 being Polynomial of o2,L such that
A10: Q199 = (p + q) . b199 and
A11: b9 = b199 +^ b299 and
A12: (Compress (p + q)) . b9 = Q199 . b299 by Def2;
A13: b19 = b199 by A8, A11, Th7;
reconsider b1 = b1 as bag of o1 ;
A14: (p + q) . b1 = (p . b1) + (q . b1) by POLYNOM1:15;
 b1 = b19 by A5, A8, Th7;
then  Q199 = Q1 + Q19 by A4, A7, A10, A13, A14, POLYNOM1:def_10;
then A15: Q199 . b2 = (Q1 . b2) + (Q19 . b2) by POLYNOM1:15;
A16: b29 = b299 by A8, A11, Th7;
A17: b2 = b29 by A5, A8, Th7;
 x + y = p + q by POLYNOM1:def_10;
hence fpq . b = (Compress (p + q)) . b9 by A2
.= ((Compress p) . b9) + (fq . b) by A2, A6, A9, A12, A17, A16, A15
.= (fp . b) + (fq . b) by A2 ;
::_thesis: verum
end;
hence f . (x + y) = fp + fq by POLYNOM1:16
.= (f . x) + (f . y) by POLYNOM1:def_10 ;
::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_(Polynom-Ring_(o1,(Polynom-Ring_(o2,L))))_holds_f_._(x_*_y)_=_(f_._x)_*_(f_._y)
let x, y be Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))); ::_thesis: f . (x * y) = (f . x) * (f . y)
reconsider x9 = x, y9 = y as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ;
reconsider p = x9, q = y9 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def_10;
reconsider fp = f . x, fq = f . y as Element of (Polynom-Ring ((o1 +^ o2),L)) ;
reconsider fp = fp, fq = fq as Polynomial of (o1 +^ o2),L by POLYNOM1:def_10;
 f . (x * y) = f . (p *' q) by POLYNOM1:def_10;
then reconsider fpq9 = f . (p *' q) as Polynomial of (o1 +^ o2),L by POLYNOM1:def_10;
A18: for b being bag of o1 +^ o2 ex s being FinSequence of the carrier of L st
( fpq9 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )
proof
reconsider x = p *' q as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by POLYNOM1:def_10;
let c be bag of o1 +^ o2; ::_thesis: ex s being FinSequence of the carrier of L st
( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )
reconsider b = c as Element of Bags (o1 +^ o2) by PRE_POLY:def_12;
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A19: b = b1 +^ b2 by Th6;
reconsider b1 = b1 as bag of o1 ;
consider r being FinSequence of the carrier of (Polynom-Ring (o2,L)) such that
A20: (p *' q) . b1 = Sum r and
A21: len r = len (decomp b1) and
A22: for k being Element of NAT st k in dom r holds
ex a19, b19 being bag of o1 st
( (decomp b1) /. k = <*a19,b19*> & r /. k = (p . a19) * (q . b19) ) by POLYNOM1:def_9;
 for x being set st x in dom r holds
r . x is Function
proof
let x be set ; ::_thesis: ( x in dom r implies r . x is Function )
assume  x in dom r ; ::_thesis: r . x is Function
then A23: 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  r . x is Function by A23, POLYNOM1:def_10; ::_thesis: verum
end;
then reconsider rFF = r as Function-yielding Function by FUNCOP_1:def_6;
deffunc H1( set ) ->  set = (rFF . $1) . b2;
consider rFFb2 being Function such that
A24: dom rFFb2 = dom r and
A25: for i being set st i in dom r holds
rFFb2 . i = H1(i) from FUNCT_1:sch_3();
 ex i being Nat st dom r = Seg i by FINSEQ_1:def_2;
then reconsider rFFb2 = rFFb2 as FinSequence by A24, FINSEQ_1:def_2;
A26: rng rFFb2 c= the carrier of L
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng rFFb2 or u in the carrier of L )
A27: rng rFF c= the carrier of (Polynom-Ring (o2,L)) by FINSEQ_1:def_4;
assume  u in rng rFFb2 ; ::_thesis: u in the carrier of L
then consider x being set  such that
A28: x in dom rFFb2 and
A29: u = rFFb2 . x by FUNCT_1:def_3;
 rFF . x in rng rFF by A24, A28, FUNCT_1:3;
then A30: rFF . x is Function of (Bags o2), the carrier of L by A27, POLYNOM1:def_10;
then A31: rng (rFF . x) c= the carrier of L by RELAT_1:def_19;
 dom (rFF . x) = Bags o2 by A30, FUNCT_2:def_1;
then A32: (rFF . x) . b2 in rng (rFF . x) by FUNCT_1:3;
 rFFb2 . x = (rFF . x) . b2 by A24, A25, A28;
hence  u in the carrier of L by A29, A31, A32; ::_thesis: verum
end;
defpred S2[ set , set ] means  ex a19, b19 being bag of o1 ex Fk being FinSequence of the carrier of L ex pa19, qb19 being 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 being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) );
A33: for k being Element of NAT st k in Seg (len r) holds
ex x being Element of the carrier of L * st S2[k,x]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len r) implies ex x being Element of the carrier of L * st S2[k,x] )
assume  k in Seg (len r) ; ::_thesis: ex x being Element of the carrier of L * st S2[k,x]
then  k in dom (decomp b1) by A21, FINSEQ_1:def_3;
then consider a19, b19 being bag of o1 such that
A34: (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_10;
defpred S3[ set , set ] means  ex a199, b199 being bag of o2 st
( (decomp b2) /. $1 = <*a199,b199*> & $2 = (pa19 . a199) * (qb19 . b199) );
A35: for k being Element of NAT st k in Seg (len (decomp b2)) holds
ex x being Element of L st S3[k,x]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len (decomp b2)) implies ex x being Element of L st S3[k,x] )
assume  k in Seg (len (decomp b2)) ; ::_thesis: ex x being Element of L st S3[k,x]
then  k in dom (decomp b2) by FINSEQ_1:def_3;
then consider a199, b199 being bag of o2 such that
A36: (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 ; ::_thesis: S3[k,x]
take  a199 ; ::_thesis: ex b199 being bag of o2 st
( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) )
take  b199 ; ::_thesis: ( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) )
thus  ( (decomp b2) /. k = <*a199,b199*> & x = (pa19 . a199) * (qb19 . b199) ) by A36; ::_thesis: verum
end;
consider Fk being FinSequence of the carrier of L such that
A37: dom Fk = Seg (len (decomp b2)) and
A38: for k being Element of NAT st k in Seg (len (decomp b2)) holds
S3[k,Fk /. k] from RECDEF_1:sch_17(A35);
reconsider x = Fk as Element of the carrier of L * by FINSEQ_1:def_11;
take  x ; ::_thesis: S2[k,x]
take  a19 ; ::_thesis: ex b19 being bag of o1 ex Fk being FinSequence of the carrier of L ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take  b19 ; ::_thesis: ex Fk being FinSequence of the carrier of L ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take  Fk ; ::_thesis: ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take  pa19 ; ::_thesis: ex qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take  qb19 ; ::_thesis: ( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
thus  ( pa19 = p . a19 & qb19 = q . b19 & Fk = x ) ; ::_thesis: ( (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
thus  (decomp b1) /. k = <*a19,b19*> by A34; ::_thesis: ( len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
thus  len Fk = len (decomp b2) by A37, FINSEQ_1:def_3; ::_thesis: for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) )
let m be Nat; ::_thesis: ( m in dom Fk implies ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) )
assume  m in dom Fk ; ::_thesis: ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) )
hence  ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) by A37, A38; ::_thesis: verum
end;
consider F being FinSequence of the carrier of L *  such that
A39: dom F = Seg (len r) and
A40: for k being Element of NAT st k in Seg (len r) holds
S2[k,F /. k] from RECDEF_1:sch_17(A33);
take s = FlattenSeq F; ::_thesis: ( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )
A41: len (Sum F) = len F by MATRLIN:def_6;
reconsider rFFb2 = rFFb2 as FinSequence of the carrier of L by A26, FINSEQ_1:def_4;
A42: f . x = Compress (p *' q) by A2;
A43: dom rFFb2 = dom F by A39, A24, FINSEQ_1:def_3
.= dom (Sum F) by A41, FINSEQ_3:29 ;
 for k being Nat st k in dom rFFb2 holds
rFFb2 . k = (Sum F) . k
proof
let k be Nat; ::_thesis: ( k in dom rFFb2 implies rFFb2 . k = (Sum F) . k )
assume A44: k in dom rFFb2 ; ::_thesis: rFFb2 . k = (Sum F) . k
consider c1, d1 being bag of o1 such that
A45: (decomp b1) /. k = <*c1,d1*> and
A46: r /. k = (p . c1) * (q . d1) by A22, A24, A44;
 k in Seg (len r) by A24, A44, FINSEQ_1:def_3;
then consider a19, b19 being bag of o1, Fk being FinSequence of the carrier of L, pa19, qb19 being Polynomial of o2,L such that
A47: ( pa19 = p . a19 & qb19 = q . b19 ) and
A48: Fk = F /. k and
A49: (decomp b1) /. k = <*a19,b19*> and
A50: len Fk = len (decomp b2) and
A51: for ki being Nat st ki in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. ki = <*a199,b199*> & Fk /. ki = (pa19 . a199) * (qb19 . b199) ) by A40;
A52: ( c1 = a19 & d1 = b19 ) by A45, A49, FINSEQ_1:77;
consider s1 being FinSequence of the carrier of L such that
A53: (pa19 *' qb19) . b2 = Sum s1 and
A54: len s1 = len (decomp b2) and
A55: for ki being Element of NAT st ki in dom s1 holds
ex x1, y2 being bag of o2 st
( (decomp b2) /. ki = <*x1,y2*> & s1 /. ki = (pa19 . x1) * (qb19 . y2) ) by POLYNOM1:def_9;
A56: dom s1 = Seg (len s1) by FINSEQ_1:def_3;
now__::_thesis:_for_ki_being_Nat_st_ki_in_dom_s1_holds_
s1_._ki_=_Fk_._ki
let ki be Nat; ::_thesis: ( ki in dom s1 implies s1 . ki = Fk . ki )
assume A57: ki in dom s1 ; ::_thesis: s1 . ki = Fk . ki
then A58: s1 /. ki = s1 . ki by PARTFUN1:def_6;
A59: ki in dom Fk by A50, A54, A56, A57, FINSEQ_1:def_3;
then consider a199, b199 being bag of o2 such that
A60: (decomp b2) /. ki = <*a199,b199*> and
A61: Fk /. ki = (pa19 . a199) * (qb19 . b199) by A51;
consider x1, y2 being bag of o2 such that
A62: (decomp b2) /. ki = <*x1,y2*> and
A63: s1 /. ki = (pa19 . x1) * (qb19 . y2) by A55, A57;
 ( x1 = a199 & y2 = b199 ) by A62, A60, FINSEQ_1:77;
hence  s1 . ki = Fk . ki by A63, A59, A61, A58, PARTFUN1:def_6; ::_thesis: verum
end;
then A64: s1 = Fk by A50, A54, FINSEQ_2:9;
A65: rFF . k = r /. k by A24, A44, PARTFUN1:def_6
.= pa19 *' qb19 by A46, A47, A52, POLYNOM1:def_10 ;
thus rFFb2 . k = (rFF . k) . b2 by A24, A25, A44
.= (Sum F) /. k by A43, A44, A48, A65, A53, A64, MATRLIN:def_6
.= (Sum F) . k by A43, A44, PARTFUN1:def_6 ; ::_thesis: verum
end;
then A66: rFFb2 = Sum F by A43, FINSEQ_1:13;
reconsider Sr = Sum r as Polynomial of o2,L by POLYNOM1:def_10;
consider gg being Function of NAT, the carrier of (Polynom-Ring (o2,L)) such that
A67: Sum r = gg . (len r) and
A68: gg . 0 = 0. (Polynom-Ring (o2,L)) and
A69: for j being Element of NAT
for v being 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 S3[ Nat, set ] means  for pp being Polynomial of o2,L st $1 <= len r & pp = gg . $1 holds
$2 = pp . b2;
A70: for x being Element of NAT ex y being Element of L st S3[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of L st S3[x,y]
reconsider pp9 = gg . x as Polynomial of o2,L by POLYNOM1:def_10;
take y = pp9 . b2; ::_thesis: S3[x,y]
let pp be Polynomial of o2,L; ::_thesis: ( x <= len r & pp = gg . x implies y = pp . b2 )
assume that
 x <= len r and
A71: pp = gg . x ; ::_thesis: y = pp . b2
thus  y = pp . b2 by A71; ::_thesis: verum
end;
consider ff being Function of NAT, the carrier of L such that
A72: for j being Element of NAT holds S3[j,ff . j] from FUNCT_2:sch_3(A70);
defpred S4[ set , set ] means  ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = $2 & (decomp b1) /. $1 = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) );
A73: for i being Element of NAT st i in Seg (len r) holds
ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S4[i,x]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len r) implies ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S4[k,x] )
assume  k in Seg (len r) ; ::_thesis: ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S4[k,x]
then  k in dom (decomp b1) by A21, FINSEQ_1:def_3;
then consider a19, b19 being bag of o1 such that
A74: (decomp b1) /. k = <*a19,b19*> and
 b1 = a19 + b19 by PRE_POLY:68;
reconsider a19 = a19, b19 = b19 as Element of Bags o1 by PRE_POLY:def_12;
defpred S5[ set , set ] means  ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. $1 = <*a199,b199*> & $2 = <*(a19 +^ a199),(b19 +^ b199)*> );
A75: for k being Element of NAT st k in Seg (len (decomp b2)) holds
ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S5[k,x]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len (decomp b2)) implies ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S5[k,x] )
assume  k in Seg (len (decomp b2)) ; ::_thesis: ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S5[k,x]
then  k in dom (decomp b2) by FINSEQ_1:def_3;
then consider a199, b199 being bag of o2 such that
A76: (decomp b2) /. k = <*a199,b199*> and
 b2 = a199 + b199 by PRE_POLY:68;
reconsider a199 = a199, b199 = 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 ; ::_thesis: S5[k,x]
take  a199 ; ::_thesis: ex b199 being Element of Bags o2 st
( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )
take  b199 ; ::_thesis: ( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )
thus  ( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> ) by A76; ::_thesis: verum
end;
consider Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
A77: dom Fk = Seg (len (decomp b2)) and
A78: for k being Element of NAT st k in Seg (len (decomp b2)) holds
S5[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 ; ::_thesis: S4[k,x]
take  a19 ; ::_thesis: ex b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
take  b19 ; ::_thesis: ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
take  Fk ; ::_thesis: ( Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
thus  Fk = x ; ::_thesis: ( (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
thus  (decomp b1) /. k = <*a19,b19*> by A74; ::_thesis: ( len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
thus  len Fk = len (decomp b2) by A77, FINSEQ_1:def_3; ::_thesis: for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> )
let m be Nat; ::_thesis: ( m in dom Fk implies ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) )
assume  m in dom Fk ; ::_thesis: ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> )
hence  ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) by A77, A78; ::_thesis: verum
end;
consider G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) *  such that
A79: dom G = Seg (len r) and
A80: for i being Element of NAT st i in Seg (len r) holds
S4[i,G /. i] from RECDEF_1:sch_17(A73);
A81: for i being Nat st i in Seg (len r) holds
S4[i,G /. i] by A80;
A82: dom (Card F) = dom F by CARD_3:def_2;
A83: for j being Nat st j in dom (Card F) holds
(Card F) . j = (Card G) . j
proof
let j be Nat; ::_thesis: ( j in dom (Card F) implies (Card F) . j = (Card G) . j )
assume A84: j in dom (Card F) ; ::_thesis: (Card F) . j = (Card G) . j
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 being bag of o1 ex Fk being FinSequence of the carrier of L ex pa19, qb19 being 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 being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) ) & ex a29, b29 being Element of Bags o1 ex Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Gk = G /. j & (decomp b1) /. j = <*a29,b29*> & len Gk = len (decomp b2) & ( for m being Nat st m in dom Gk holds
ex a299, b299 being Element of Bags o2 st
( (decomp b2) /. m = <*a299,b299*> & Gk /. m = <*(a29 +^ a299),(b29 +^ b299)*> ) ) ) ) by A39, A40, A80, A85;
card (F . j) = card (F /. j) by A85, PARTFUN1:def_6
.= card (G . j) by A39, A79, A82, A84, A87, PARTFUN1:def_6 ;
hence  (Card F) . j = (Card G) . j by A39, A79, A82, A84, A86, CARD_3:def_2; ::_thesis: verum
end;
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1 being 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 A19, A89, Th7;
then  dom G = dom (decomp c1) by A21, A79, FINSEQ_1:def_3;
then A92: decomp c = FlattenSeq G by A19, A79, A81, A91, Th14;
A93: for j being Element of NAT
for v being Element of L st j < len rFFb2 & v = rFFb2 . (j + 1) holds
ff . (j + 1) = (ff . j) + v
proof
let j be Element of NAT ; ::_thesis: for v being Element of L st j < len rFFb2 & v = rFFb2 . (j + 1) holds
ff . (j + 1) = (ff . j) + v
let v be Element of L; ::_thesis: ( j < len rFFb2 & v = rFFb2 . (j + 1) implies ff . (j + 1) = (ff . j) + v )
assume that
A94: j < len rFFb2 and
A95: v = rFFb2 . (j + 1) ; ::_thesis: ff . (j + 1) = (ff . j) + v
reconsider w = r /. (j + 1), pp = gg . j, pp9 = gg . (j + 1) as Polynomial of o2,L by POLYNOM1:def_10;
reconsider w1 = w, pp1 = pp, pp19 = pp9 as Element of (Polynom-Ring (o2,L)) ;
reconsider w1 = w1, pp1 = pp1, pp19 = pp19 as Element of (Polynom-Ring (o2,L)) ;
A96: j < len r by A24, 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 A69, 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 A25, 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_10
.= (pp . b2) + (w . b2) by POLYNOM1:15
.= (ff . j) + v by A72, A96, A100 ;
::_thesis: verum
end;
 gg . 0 = 0_ (o2,L) by A68, POLYNOM1:def_10;
then A101: ff . 0 = (0_ (o2,L)) . b2 by A72, NAT_1:2
.= 0. L by POLYNOM1:22 ;
 len rFFb2 = len r by A24, FINSEQ_3:29;
then  Sr . b2 = ff . (len rFFb2) by A67, A72;
then A102: Sr . b2 = Sum rFFb2 by A101, A93, RLVECT_1:def_12;
 ( b1 = c1 & b2 = c2 ) by A19, A89, Th7;
hence  fpq9 . c = Sum s by A20, A88, A90, A66, A102, A42, POLYNOM1:14; ::_thesis: ( len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )
 dom (Card G) = dom G by CARD_3:def_2;
then  len (Card F) = len (Card G) by A39, 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; ::_thesis: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )
let k be Element of NAT ; ::_thesis: ( k in dom s implies ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) )
assume A105: k in dom s ; ::_thesis: ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )
then consider i, j being Element of 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 being Element of 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 being 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 being Element of Bags o1, cb2 being Element of Bags o2, Q1 being 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 being bag of o1, Fk being FinSequence of the carrier of L, pa19, qb19 being 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 being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) by A39, A40, A106;
consider ga19, gb19 being Element of Bags o1, Gk being 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 being Nat st m in dom Gk holds
ex ga199, gb199 being Element of Bags o2 st
( (decomp b2) /. m = <*ga199,gb199*> & Gk /. m = <*(ga19 +^ ga199),(gb19 +^ gb199)*> ) by A39, A80, A106;
A128: b19 = gb19 by A123, A126, FINSEQ_1:77;
A129: Gk = G . i by A39, A79, A106, A125, PARTFUN1:def_6;
then consider ga199, gb199 being 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 being 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 ; ::_thesis: ex b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*c1,b2*> & s /. k = (fp . c1) * (fq . b2) )
take  c2 ; ::_thesis: ( (decomp c) /. k = <*c1,c2*> & s /. k = (fp . c1) * (fq . c2) )
thus  (decomp c) /. k = <*c1,c2*> by A116; ::_thesis: s /. k = (fp . c1) * (fq . c2)
consider cb1 being Element of Bags o1, cb2 being Element of Bags o2, Q1 being 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 ; ::_thesis: verum
end;
thus f . (x * y) = f . (p *' q) by POLYNOM1:def_10
.= fp *' fq by A18, POLYNOM1:def_9
.= (f . x) * (f . y) by POLYNOM1:def_10 ; ::_thesis: verum
end;
hence A144: f is multiplicative by GROUP_6:def_6; ::_thesis: ( f is unity-preserving & f is one-to-one & f is RingEpimorphism )
A145: for b being Element of Bags (o1 +^ o2) holds (Compress 1P1) . b = 1P2 . b
proof
let b be Element of Bags (o1 +^ o2); ::_thesis: (Compress 1P1) . b = 1P2 . b
A146: 1P2 . b = (1_ ((o1 +^ o2),L)) . b by POLYNOM1:31;
consider b1 being Element of Bags o1, b2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A147: Q1 = 1P1 . b1 and
A148: b = b1 +^ b2 and
A149: (Compress 1P1) . b = Q1 . b2 by Def2;
percases ( b = EmptyBag (o1 +^ o2) or b <> EmptyBag (o1 +^ o2) ) ;
supposeA150: b = EmptyBag (o1 +^ o2) ; ::_thesis: (Compress 1P1) . b = 1P2 . b
then A151: b1 = EmptyBag o1 by A148, Th5;
A152: b2 = EmptyBag o2 by A148, A150, Th5;
Q1 = (1_ (o1,(Polynom-Ring (o2,L)))) . b1 by A147, POLYNOM1:31
.= 1_ (Polynom-Ring (o2,L)) by A151, POLYNOM1:25 ;
then Q1 . b2 = (1_ (o2,L)) . b2 by POLYNOM1:31
.= 1_ L by A152, POLYNOM1:25
.= 1P2 . b by A146, A150, POLYNOM1:25 ;
hence  (Compress 1P1) . b = 1P2 . b by A149; ::_thesis: verum
end;
supposeA153: b <> EmptyBag (o1 +^ o2) ; ::_thesis: (Compress 1P1) . b = 1P2 . b
then A154: ( b1 <> EmptyBag o1 or b2 <> EmptyBag o2 ) by A148, Th5;
now__::_thesis:_(Compress_1P1)_._b_=_1P2_._b
percases ( b1 = EmptyBag o1 or b1 <> EmptyBag o1 ) ;
supposeA155: b1 = EmptyBag o1 ; ::_thesis: (Compress 1P1) . b = 1P2 . b
Q1 = (1_ (o1,(Polynom-Ring (o2,L)))) . b1 by A147, POLYNOM1:31
.= 1_ (Polynom-Ring (o2,L)) by A155, POLYNOM1:25
.= 1_ (o2,L) by POLYNOM1:31 ;
then Q1 . b2 = 0. L by A154, A155, POLYNOM1:25
.= 1P2 . b by A146, A153, POLYNOM1:25 ;
hence  (Compress 1P1) . b = 1P2 . b by A149; ::_thesis: verum
end;
supposeA156: b1 <> EmptyBag o1 ; ::_thesis: (Compress 1P1) . b = 1P2 . b
Q1 = (1_ (o1,(Polynom-Ring (o2,L)))) . b1 by A147, POLYNOM1:31
.= 0. (Polynom-Ring (o2,L)) by A156, POLYNOM1:25
.= 0_ (o2,L) by POLYNOM1:def_10 ;
then Q1 . b2 = 0. L by POLYNOM1:22
.= 1P2 . b by A146, A153, POLYNOM1:25 ;
hence  (Compress 1P1) . b = 1P2 . b by A149; ::_thesis: verum
end;
end;
end;
hence  (Compress 1P1) . b = 1P2 . b ; ::_thesis: verum
end;
end;
end;
f . (1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L))))) = Compress 1P1 by A2
.= 1_ (Polynom-Ring ((o1 +^ o2),L)) by A145, FUNCT_2:63 ;
hence A157: f is unity-preserving by GROUP_1:def_13; ::_thesis: ( f is one-to-one & f is RingEpimorphism )
thus  f is one-to-one ::_thesis: f is RingEpimorphism
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume  x1 in dom f ; ::_thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
then reconsider x19 = x1 as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def_1;
assume  x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
then reconsider x29 = x2 as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def_1;
reconsider x299 = x29 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def_10;
reconsider x199 = x19 as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def_10;
A158: f . x29 = Compress x299 by A2;
then reconsider w2 = f . x29 as Polynomial of (o1 +^ o2),L ;
A159: f . x19 = Compress x199 by A2;
then reconsider w1 = f . x19 as Polynomial of (o1 +^ o2),L ;
assume A160: f . x1 = f . x2 ; ::_thesis: x1 = x2
now__::_thesis:_for_b1_being_Element_of_Bags_o1_holds_x199_._b1_=_x299_._b1
let b1 be Element of Bags o1; ::_thesis: x199 . b1 = x299 . b1
reconsider x199b1 = x199 . b1, x299b1 = x299 . b1 as Polynomial of o2,L by POLYNOM1:def_10;
now__::_thesis:_for_b2_being_Element_of_Bags_o2_holds_x199b1_._b2_=_x299b1_._b2
let b2 be Element of Bags o2; ::_thesis: x199b1 . b2 = x299b1 . b2
set b = b1 +^ b2;
consider b19 being Element of Bags o1, b29 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A161: Q1 = x199 . b19 and
A162: b1 +^ b2 = b19 +^ b29 and
A163: w1 . (b1 +^ b2) = Q1 . b29 by A159, Def2;
A164: ( b1 = b19 & b2 = b29 ) by A162, Th7;
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q19 being Polynomial of o2,L such that
A165: Q19 = x299 . c1 and
A166: b1 +^ b2 = c1 +^ c2 and
A167: w2 . (b1 +^ b2) = Q19 . c2 by A158, Def2;
 b1 = c1 by A166, Th7;
hence  x199b1 . b2 = x299b1 . b2 by A160, A161, A163, A165, A166, A167, A164, Th7; ::_thesis: verum
end;
hence  x199 . b1 = x299 . b1 by FUNCT_2:63; ::_thesis: verum
end;
hence  x1 = x2 by FUNCT_2:63; ::_thesis: verum
end;
thus  f is RingHomomorphism by A3, A144, A157; :: according to QUOFIELD:def_19 ::_thesis: K795( the carrier of (Polynom-Ring ((o1 +^ o2),L)),f) = the carrier of (Polynom-Ring ((o1 +^ o2),L))
thus  rng f c= the carrier of (Polynom-Ring ((o1 +^ o2),L)) by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= K795( the carrier of (Polynom-Ring ((o1 +^ o2),L)),f)
thus  the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= rng f ::_thesis: verum
proof
defpred S2[ set , set ] means  ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 st
( $1 = b1 +^ b2 & $2 = b1 );
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) or y in rng f )
assume  y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) ; ::_thesis: y in rng f
then reconsider s = y as Polynomial of (o1 +^ o2),L by POLYNOM1:def_10;
defpred S3[ Element of Bags o1, Element of (Polynom-Ring (o2,L))] means  ex h being Function st
( h = $2 & ( for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = $1 +^ b2 holds
h . b2 = s . b ) );
A168: for x being Element of Bags (o1 +^ o2) ex y being Element of Bags o1 st S2[x,y]
proof
let x be Element of Bags (o1 +^ o2); ::_thesis: ex y being Element of Bags o1 st S2[x,y]
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A169: x = b1 +^ b2 by Th6;
reconsider y = b1 as Element of Bags o1 ;
take  y ; ::_thesis: S2[x,y]
take  b1 ; ::_thesis: ex b2 being Element of Bags o2 st
( x = b1 +^ b2 & y = b1 )
take  b2 ; ::_thesis: ( x = b1 +^ b2 & y = b1 )
thus  x = b1 +^ b2 by A169; ::_thesis: y = b1
thus  y = b1 ; ::_thesis: verum
end;
consider kk being Function of (Bags (o1 +^ o2)),(Bags o1) such that
A170: for b being Element of Bags (o1 +^ o2) holds S2[b,kk . b] from FUNCT_2:sch_3(A168);
A171: for x being Element of Bags o1 ex y being Element of (Polynom-Ring (o2,L)) st S3[x,y]
proof
defpred S4[ set , set ] means  ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 st
( $1 = b1 +^ b2 & $2 = b2 );
let x be Element of Bags o1; ::_thesis: ex y being Element of (Polynom-Ring (o2,L)) st S3[x,y]
reconsider b1 = x as Element of Bags o1 ;
defpred S5[ Element of Bags o2, Element of L] means  for b being Element of Bags (o1 +^ o2) st b = b1 +^ $1 holds
$2 = s . b;
A172: for p being Element of Bags o2 ex q being Element of L st S5[p,q]
proof
let p be Element of Bags o2; ::_thesis: ex q being Element of L st S5[p,q]
take  s . (b1 +^ p) ; ::_thesis: S5[p,s . (b1 +^ p)]
let b be Element of Bags (o1 +^ o2); ::_thesis: ( b = b1 +^ p implies s . (b1 +^ p) = s . b )
assume  b = b1 +^ p ; ::_thesis: s . (b1 +^ p) = s . b
hence  s . (b1 +^ p) = s . b ; ::_thesis: verum
end;
consider t being Function of (Bags o2), the carrier of L such that
A173: for b2 being Element of Bags o2 holds S5[b2,t . b2] from FUNCT_2:sch_3(A172);
reconsider t = t as Function of (Bags o2),L ;
A174: for x being Element of Bags (o1 +^ o2) ex y being Element of Bags o2 st S4[x,y]
proof
let x be Element of Bags (o1 +^ o2); ::_thesis: ex y being Element of Bags o2 st S4[x,y]
consider b1 being Element of Bags o1, b2 being Element of Bags o2 such that
A175: x = b1 +^ b2 by Th6;
reconsider y = b2 as Element of Bags o2 ;
take  y ; ::_thesis: S4[x,y]
take  b1 ; ::_thesis: ex b2 being Element of Bags o2 st
( x = b1 +^ b2 & y = b2 )
take  b2 ; ::_thesis: ( x = b1 +^ b2 & y = b2 )
thus  x = b1 +^ b2 by A175; ::_thesis: y = b2
thus  y = b2 ; ::_thesis: verum
end;
consider kk being Function of (Bags (o1 +^ o2)),(Bags o2) such that
A176: for b being Element of Bags (o1 +^ o2) holds S4[b,kk . b] from FUNCT_2:sch_3(A174);
 Support t c= kk .: (Support s)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support t or x in kk .: (Support s) )
assume A177: x in Support t ; ::_thesis: x in kk .: (Support s)
then reconsider b2 = x as Element of Bags o2 ;
set b = b1 +^ b2;
 t . x <> 0. L by A177, POLYNOM1:def_3;
then  s . (b1 +^ b2) <> 0. L by A173;
then A178: ( dom kk = Bags (o1 +^ o2) & b1 +^ b2 in Support s ) by FUNCT_2:def_1, POLYNOM1:def_3;
 ex b19 being Element of Bags o1 ex b29 being Element of Bags o2 st
( b1 +^ b2 = b19 +^ b29 & kk . (b1 +^ b2) = b29 ) by A176;
then  x = kk . (b1 +^ b2) by Th7;
hence  x in kk .: (Support s) by A178, FUNCT_1:def_6; ::_thesis: verum
end;
then  t is Polynomial of o2,L by POLYNOM1:def_4;
then reconsider t99 = t as Element of (Polynom-Ring (o2,L)) by POLYNOM1:def_10;
reconsider t9 = t as Function ;
take  t99 ; ::_thesis: S3[x,t99]
take  t9 ; ::_thesis: ( t9 = t99 & ( for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds
t9 . b2 = s . b ) )
thus  t99 = t9 ; ::_thesis: for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds
t9 . b2 = s . b
let b2 be Element of Bags o2; ::_thesis: for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds
t9 . b2 = s . b
let b be Element of Bags (o1 +^ o2); ::_thesis: ( b = x +^ b2 implies t9 . b2 = s . b )
assume  b = x +^ b2 ; ::_thesis: t9 . b2 = s . b
hence  t9 . b2 = s . b by A173; ::_thesis: verum
end;
consider g being Function of (Bags o1), the carrier of (Polynom-Ring (o2,L)) such that
A179: for x being Element of Bags o1 holds S3[x,g . x] from FUNCT_2:sch_3(A171);
reconsider g = g as Function of (Bags o1),(Polynom-Ring (o2,L)) ;
A180: Support g c= kk .: (Support s)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support g or x in kk .: (Support s) )
assume A181: x in Support g ; ::_thesis: x in kk .: (Support s)
then reconsider b1 = x as Element of Bags o1 ;
consider h being Function such that
A182: h = g . b1 and
A183: for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = b1 +^ b2 holds
h . b2 = s . b by A179;
reconsider h = h as Polynomial of o2,L by A182, POLYNOM1:def_10;
 g . b1 <> 0. (Polynom-Ring (o2,L)) by A181, POLYNOM1:def_3;
then  g . b1 <> 0_ (o2,L) by POLYNOM1:def_10;
then consider b2 being Element of Bags o2 such that
A184: b2 in Support h by A182, POLYNOM2:17, SUBSET_1:4;
set b = b1 +^ b2;
 h . b2 <> 0. L by A184, POLYNOM1:def_3;
then  s . (b1 +^ b2) <> 0. L by A183;
then A185: ( dom kk = Bags (o1 +^ o2) & b1 +^ b2 in Support s ) by FUNCT_2:def_1, POLYNOM1:def_3;
 ex b19 being Element of Bags o1 ex b29 being Element of Bags o2 st
( b1 +^ b2 = b19 +^ b29 & kk . (b1 +^ b2) = b19 ) by A170;
then  x = kk . (b1 +^ b2) by Th7;
hence  x in kk .: (Support s) by A185, FUNCT_1:def_6; ::_thesis: verum
end;
then  g is Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def_4;
then reconsider g = g as Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by POLYNOM1:def_10;
reconsider g9 = g as Polynomial of o1,(Polynom-Ring (o2,L)) by A180, POLYNOM1:def_4;
now__::_thesis:_for_b_being_Element_of_Bags_(o1_+^_o2)_holds_s_._b_=_(Compress_g9)_._b
let b be Element of Bags (o1 +^ o2); ::_thesis: s . b = (Compress g9) . b
consider b1 being Element of Bags o1, b2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A186: ( Q1 = g9 . b1 & b = b1 +^ b2 & (Compress g9) . b = Q1 . b2 ) by Def2;
 ex h being Function st
( h = g9 . b1 & ( for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = b1 +^ b2 holds
h . b2 = s . b ) ) by A179;
hence  s . b = (Compress g9) . b by A186; ::_thesis: verum
end;
then A187: y = Compress g9 by FUNCT_2:63
.= f . g by A2 ;
 dom f = the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def_1;
hence  y in rng f by A187, FUNCT_1:3; ::_thesis: verum
end;
end;