set P = upm (n,R);

set CR = the carrier of R;

set PNR = Polynom-Ring (n,R);

set CPNR = the carrier of (Polynom-Ring (n,R));

thus upm (n,R) is multiplicative :: thesis: verum

set CR = the carrier of R;

set PNR = Polynom-Ring (n,R);

set CPNR = the carrier of (Polynom-Ring (n,R));

thus upm (n,R) is multiplicative :: thesis: verum

proof

let x9, y9 be Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))); :: according to GROUP_6:def 6 :: thesis: (upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9)

reconsider x = x9, y = y9, xy = x9 * y9 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

reconsider Pxy = (upm (n,R)) . (x9 * y9), PxPy = ((upm (n,R)) . x9) * ((upm (n,R)) . y9), Px = (upm (n,R)) . x9, Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def 11;

A3: xy = x *' y by POLYNOM3:def 10;

A4: PxPy = Px *' Py by POLYNOM1:def 11;

end;reconsider x = x9, y = y9, xy = x9 * y9 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

reconsider Pxy = (upm (n,R)) . (x9 * y9), PxPy = ((upm (n,R)) . x9) * ((upm (n,R)) . y9), Px = (upm (n,R)) . x9, Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def 11;

A3: xy = x *' y by POLYNOM3:def 10;

A4: PxPy = Px *' Py by POLYNOM1:def 11;

now :: thesis: for b9 being object st b9 in Bags (n + 1) holds

Pxy . b9 = PxPy . b9

hence
(upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9)
by FUNCT_2:12; :: thesis: verumPxy . b9 = PxPy . b9

let b9 be object ; :: thesis: ( b9 in Bags (n + 1) implies Pxy . b9 = PxPy . b9 )

assume b9 in Bags (n + 1) ; :: thesis: Pxy . b9 = PxPy . b9

then reconsider b = b9 as Element of Bags (n + 1) ;

consider r being FinSequence of the carrier of (Polynom-Ring (n,R)) such that

A5: len r = (b . n) + 1 and

A6: xy . (b . n) = Sum r and

A7: for k being Element of NAT st k in dom r holds

r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A3, POLYNOM3:def 9;

n < n + 1 by NAT_1:13;

then reconsider bn = b | n as Element of Bags n by Th3;

defpred S_{1}[ object , object ] means for p, q being Polynomial of n,R

for fcr being FinSequence of the carrier of R

for i being Element of NAT st i = R & p = x . (i -' 1) & q = y . (((b . n) + 1) -' i) & fcr = n holds

( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds

ex b1, b2 being bag of n st

( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) );

reconsider xybn = xy . (b . n) as Polynomial of n,R by POLYNOM1:def 11;

consider u being FinSequence of the carrier of R such that

A8: PxPy . b = Sum u and

A9: len u = len (decomp b) and

A10: for k being Element of NAT st k in dom u holds

ex b1, b2 being bag of n + 1 st

( (decomp b) /. k = <*b1,b2*> & u /. k = (Px . b1) * (Py . b2) ) by A4, POLYNOM1:def 10;

A14: for e being object st e in dom r holds

S_{1}[e,s . e]
from FUNCT_2:sch 1(A11);

A15: rng s c= the carrier of R * ;

A16: dom s = dom r by FUNCT_2:def 1;

then ex n being Nat st dom s = Seg n by FINSEQ_1:def 2;

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

then reconsider s = s as FinSequence of the carrier of R * by A15, FINSEQ_1:def 4;

consider g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R such that

A17: for p being Polynomial of n,R holds g . p = p . bn and

A18: xybn . bn = Sum (g * r) by A6, Th29;

A19: Sum (g * r) = Pxy . b by A18, Def6;

0 + 1 <= len r by A5, XREAL_1:6;

then A20: 1 in dom s by A16, FINSEQ_3:25;

_{2}[ object , object ] means for i, n1 being Element of NAT

for b1 being bag of n + 1 st n1 = R & b1 = (divisors b) . n1 & i in dom (divisors bn) & (divisors bn) . i = b1 | n holds

( (b1 . n) + 1 in dom s & i in dom (s . ((b1 . n) + 1)) & n = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i );

set t = FlattenSeq s;

A35: for x being object st x in dom u holds

S_{2}[x,p . x]
from FUNCT_2:sch 1(A23);

1 in dom (Card s) by A20, CARD_3:def 2;

then Sum (Card s) >= (Card s) . 1 by POLYNOM3:4;

then Sum (Card s) > 0 by A20, A21, CARD_3:def 2;

then len (FlattenSeq s) > 0 by PRE_POLY:27;

then A36: FlattenSeq s <> {} ;

then A37: dom p = dom u by FUNCT_2:def 1;

dom (FlattenSeq s) c= rng p

len (Sum s) = len s by MATRLIN:def 6;

then A78: dom (Sum s) = dom r by A16, FINSEQ_3:29;

then Sum s = g * r by A78, A79, FINSEQ_1:13;

then A110: Sum (FlattenSeq s) = Pxy . b by A19, POLYNOM1:14;

A111: len u = card (dom u) by CARD_1:62

.= card p by A37, CARD_1:62

.= card (dom (FlattenSeq s)) by A54, A77, PRE_POLY:19

.= len (FlattenSeq s) by CARD_1:62 ;

then A112: dom u = dom (FlattenSeq s) by FINSEQ_3:29;

then p is Permutation of (dom u) by A54, A77, FUNCT_2:57;

hence Pxy . b9 = PxPy . b9 by A110, A8, A82, A111, A112, RLVECT_2:6; :: thesis: verum

end;assume b9 in Bags (n + 1) ; :: thesis: Pxy . b9 = PxPy . b9

then reconsider b = b9 as Element of Bags (n + 1) ;

consider r being FinSequence of the carrier of (Polynom-Ring (n,R)) such that

A5: len r = (b . n) + 1 and

A6: xy . (b . n) = Sum r and

A7: for k being Element of NAT st k in dom r holds

r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A3, POLYNOM3:def 9;

n < n + 1 by NAT_1:13;

then reconsider bn = b | n as Element of Bags n by Th3;

defpred S

for fcr being FinSequence of the carrier of R

for i being Element of NAT st i = R & p = x . (i -' 1) & q = y . (((b . n) + 1) -' i) & fcr = n holds

( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds

ex b1, b2 being bag of n st

( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) );

reconsider xybn = xy . (b . n) as Polynomial of n,R by POLYNOM1:def 11;

consider u being FinSequence of the carrier of R such that

A8: PxPy . b = Sum u and

A9: len u = len (decomp b) and

A10: for k being Element of NAT st k in dom u holds

ex b1, b2 being bag of n + 1 st

( (decomp b) /. k = <*b1,b2*> & u /. k = (Px . b1) * (Py . b2) ) by A4, POLYNOM1:def 10;

A11: now :: thesis: for e9 being object st e9 in dom r holds

ex u being object st

( u in the carrier of R * & S_{1}[e9,u] )

consider s being Function of (dom r),( the carrier of R *) such that ex u being object st

( u in the carrier of R * & S

let e9 be object ; :: thesis: ( e9 in dom r implies ex u being object st

( u in the carrier of R * & S_{1}[e9,u] ) )

assume e9 in dom r ; :: thesis: ex u being object st

( u in the carrier of R * & S_{1}[e9,u] )

then reconsider e = e9 as Element of NAT ;

reconsider p = x . (e -' 1), q = y . (((b . n) + 1) -' e) as Polynomial of n,R by POLYNOM1:def 11;

consider fcr being FinSequence of the carrier of R such that

A12: ( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds

ex b1, b2 being bag of n st

( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) ) by POLYNOM1:def 10;

A13: fcr in the carrier of R * by FINSEQ_1:def 11;

S_{1}[e,fcr]
by A12;

hence ex u being object st

( u in the carrier of R * & S_{1}[e9,u] )
by A13; :: thesis: verum

end;( u in the carrier of R * & S

assume e9 in dom r ; :: thesis: ex u being object st

( u in the carrier of R * & S

then reconsider e = e9 as Element of NAT ;

reconsider p = x . (e -' 1), q = y . (((b . n) + 1) -' e) as Polynomial of n,R by POLYNOM1:def 11;

consider fcr being FinSequence of the carrier of R such that

A12: ( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds

ex b1, b2 being bag of n st

( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) ) by POLYNOM1:def 10;

A13: fcr in the carrier of R * by FINSEQ_1:def 11;

S

hence ex u being object st

( u in the carrier of R * & S

A14: for e being object st e in dom r holds

S

A15: rng s c= the carrier of R * ;

A16: dom s = dom r by FUNCT_2:def 1;

then ex n being Nat st dom s = Seg n by FINSEQ_1:def 2;

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

then reconsider s = s as FinSequence of the carrier of R * by A15, FINSEQ_1:def 4;

consider g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R such that

A17: for p being Polynomial of n,R holds g . p = p . bn and

A18: xybn . bn = Sum (g * r) by A6, Th29;

A19: Sum (g * r) = Pxy . b by A18, Def6;

0 + 1 <= len r by A5, XREAL_1:6;

then A20: 1 in dom s by A16, FINSEQ_3:25;

A21: now :: thesis: len (s . 1) <> 0

defpred Sreconsider p9 = x . (1 -' 1), q9 = y . (((b . n) + 1) -' 1) as Polynomial of n,R by POLYNOM1:def 11;

s /. 1 is FinSequence of the carrier of R ;

then A22: s . 1 is FinSequence of the carrier of R by A20, PARTFUN1:def 6;

( p9 = x . (1 -' 1) & q9 = y . (((b . n) + 1) -' 1) ) ;

hence len (s . 1) <> 0 by A14, A16, A20, A22; :: thesis: verum

end;s /. 1 is FinSequence of the carrier of R ;

then A22: s . 1 is FinSequence of the carrier of R by A20, PARTFUN1:def 6;

( p9 = x . (1 -' 1) & q9 = y . (((b . n) + 1) -' 1) ) ;

hence len (s . 1) <> 0 by A14, A16, A20, A22; :: thesis: verum

for b1 being bag of n + 1 st n1 = R & b1 = (divisors b) . n1 & i in dom (divisors bn) & (divisors bn) . i = b1 | n holds

( (b1 . n) + 1 in dom s & i in dom (s . ((b1 . n) + 1)) & n = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i );

set t = FlattenSeq s;

A23: now :: thesis: for n19 being object st n19 in dom u holds

ex n29 being object st

( n29 in dom (FlattenSeq s) & S_{2}[n19,n29] )

consider p being Function of (dom u),(dom (FlattenSeq s)) such that ex n29 being object st

( n29 in dom (FlattenSeq s) & S

let n19 be object ; :: thesis: ( n19 in dom u implies ex n29 being object st

( n29 in dom (FlattenSeq s) & S_{2}[n19,n29] ) )

assume A24: n19 in dom u ; :: thesis: ex n29 being object st

( n29 in dom (FlattenSeq s) & S_{2}[n19,n29] )

then reconsider n1 = n19 as Element of NAT ;

dom u = dom (decomp b) by A9, FINSEQ_3:29

.= dom (divisors b) by PRE_POLY:def 17 ;

then A25: (divisors b) . n1 in rng (divisors b) by A24, FUNCT_1:def 3;

then reconsider b1 = (divisors b) . n1 as bag of n + 1 ;

A26: b1 divides b by A25, Th7;

then b1 . n <= b . n by PRE_POLY:def 11;

then A27: (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6;

n < n + 1 by NAT_1:13;

then reconsider b1n = b1 | n as Element of Bags n by Th3;

reconsider p = x . (((b1 . n) + 1) -' 1), q = y . (((b . n) + 1) -' ((b1 . n) + 1)) as Polynomial of n,R by POLYNOM1:def 11;

A28: ( p = x . (((b1 . n) + 1) -' 1) & q = y . (((b . n) + 1) -' ((b1 . n) + 1)) ) ;

b1n divides bn by A26, Th4;

then b1n in rng (divisors bn) by Th7;

then consider i being object such that

A29: i in dom (divisors bn) and

A30: b1n = (divisors bn) . i by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A29;

set n2 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i;

A31: (b1 . n) + 1 >= 1 + 0 by XREAL_1:6;

then A32: (b1 . n) + 1 in dom s by A5, A16, A27, FINSEQ_3:25;

then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5;

then len (s . ((b1 . n) + 1)) = len (decomp bn) by A14, A16, A32, A28;

then A33: dom (s . ((b1 . n) + 1)) = dom (decomp bn) by FINSEQ_3:29

.= dom (divisors bn) by PRE_POLY:def 17 ;

then A34: (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i in dom (FlattenSeq s) by A29, A32, PRE_POLY:30;

for i9, n19 being Element of NAT

for b19 being bag of n + 1 st n19 = n1 & b19 = (divisors b) . n19 & i9 in dom (divisors bn) & (divisors bn) . i9 = b19 | n holds

( (b19 . n) + 1 in dom s & i9 in dom (s . ((b19 . n) + 1)) & (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i = (Sum (Card (s | (((b19 . n) + 1) -' 1)))) + i9 ) by A5, A16, A29, A30, A27, A31, A33, FINSEQ_3:25, FUNCT_1:def 4;

hence ex n29 being object st

( n29 in dom (FlattenSeq s) & S_{2}[n19,n29] )
by A34; :: thesis: verum

end;( n29 in dom (FlattenSeq s) & S

assume A24: n19 in dom u ; :: thesis: ex n29 being object st

( n29 in dom (FlattenSeq s) & S

then reconsider n1 = n19 as Element of NAT ;

dom u = dom (decomp b) by A9, FINSEQ_3:29

.= dom (divisors b) by PRE_POLY:def 17 ;

then A25: (divisors b) . n1 in rng (divisors b) by A24, FUNCT_1:def 3;

then reconsider b1 = (divisors b) . n1 as bag of n + 1 ;

A26: b1 divides b by A25, Th7;

then b1 . n <= b . n by PRE_POLY:def 11;

then A27: (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6;

n < n + 1 by NAT_1:13;

then reconsider b1n = b1 | n as Element of Bags n by Th3;

reconsider p = x . (((b1 . n) + 1) -' 1), q = y . (((b . n) + 1) -' ((b1 . n) + 1)) as Polynomial of n,R by POLYNOM1:def 11;

A28: ( p = x . (((b1 . n) + 1) -' 1) & q = y . (((b . n) + 1) -' ((b1 . n) + 1)) ) ;

b1n divides bn by A26, Th4;

then b1n in rng (divisors bn) by Th7;

then consider i being object such that

A29: i in dom (divisors bn) and

A30: b1n = (divisors bn) . i by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A29;

set n2 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i;

A31: (b1 . n) + 1 >= 1 + 0 by XREAL_1:6;

then A32: (b1 . n) + 1 in dom s by A5, A16, A27, FINSEQ_3:25;

then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5;

then len (s . ((b1 . n) + 1)) = len (decomp bn) by A14, A16, A32, A28;

then A33: dom (s . ((b1 . n) + 1)) = dom (decomp bn) by FINSEQ_3:29

.= dom (divisors bn) by PRE_POLY:def 17 ;

then A34: (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i in dom (FlattenSeq s) by A29, A32, PRE_POLY:30;

for i9, n19 being Element of NAT

for b19 being bag of n + 1 st n19 = n1 & b19 = (divisors b) . n19 & i9 in dom (divisors bn) & (divisors bn) . i9 = b19 | n holds

( (b19 . n) + 1 in dom s & i9 in dom (s . ((b19 . n) + 1)) & (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i = (Sum (Card (s | (((b19 . n) + 1) -' 1)))) + i9 ) by A5, A16, A29, A30, A27, A31, A33, FINSEQ_3:25, FUNCT_1:def 4;

hence ex n29 being object st

( n29 in dom (FlattenSeq s) & S

A35: for x being object st x in dom u holds

S

1 in dom (Card s) by A20, CARD_3:def 2;

then Sum (Card s) >= (Card s) . 1 by POLYNOM3:4;

then Sum (Card s) > 0 by A20, A21, CARD_3:def 2;

then len (FlattenSeq s) > 0 by PRE_POLY:27;

then A36: FlattenSeq s <> {} ;

then A37: dom p = dom u by FUNCT_2:def 1;

now :: thesis: for n19, n29 being object st n19 in dom p & n29 in dom p & p . n19 = p . n29 holds

n19 = n29

then A54:
p is one-to-one
by FUNCT_1:def 4;n19 = n29

let n19, n29 be object ; :: thesis: ( n19 in dom p & n29 in dom p & p . n19 = p . n29 implies n19 = n29 )

assume that

A38: n19 in dom p and

A39: n29 in dom p and

A40: p . n19 = p . n29 ; :: thesis: n19 = n29

dom p = dom u by A36, FUNCT_2:def 1;

then reconsider n1 = n19, n2 = n29 as Element of NAT by A38, A39;

A41: dom u = dom (decomp b) by A9, FINSEQ_3:29

.= dom (divisors b) by PRE_POLY:def 17 ;

then A42: (divisors b) . n1 in rng (divisors b) by A38, FUNCT_1:def 3;

then reconsider b1 = (divisors b) . n1 as bag of n + 1 ;

A43: (divisors b) . n2 in rng (divisors b) by A39, A41, FUNCT_1:def 3;

then reconsider b2 = (divisors b) . n2 as bag of n + 1 ;

n < n + 1 by NAT_1:13;

then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3;

A44: ( (Card s) | (((b1 . n) + 1) -' 1) = Card (s | (((b1 . n) + 1) -' 1)) & (Card s) | (((b2 . n) + 1) -' 1) = Card (s | (((b2 . n) + 1) -' 1)) ) by POLYNOM3:16;

b2 divides b by A43, Th7;

then b2n divides bn by Th4;

then b2n in rng (divisors bn) by Th7;

then consider i2 being object such that

A45: i2 in dom (divisors bn) and

A46: b2n = (divisors bn) . i2 by FUNCT_1:def 3;

reconsider i2 = i2 as Element of NAT by A45;

A47: ( (b2 . n) + 1 in dom s & i2 in dom (s . ((b2 . n) + 1)) ) by A35, A39, A45, A46;

b1 divides b by A42, Th7;

then b1n divides bn by Th4;

then b1n in rng (divisors bn) by Th7;

then consider i1 being object such that

A48: i1 in dom (divisors bn) and

A49: b1n = (divisors bn) . i1 by FUNCT_1:def 3;

reconsider i1 = i1 as Element of NAT by A48;

A50: p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i1 by A35, A38, A48, A49;

A51: p . n2 = (Sum (Card (s | (((b2 . n) + 1) -' 1)))) + i2 by A35, A39, A45, A46;

A52: b2 is Element of Bags (n + 1) by PRE_POLY:def 12;

( (b1 . n) + 1 in dom s & i1 in dom (s . ((b1 . n) + 1)) ) by A35, A38, A48, A49;

then A53: ( (b1 . n) + 1 = (b2 . n) + 1 & i1 = i2 ) by A40, A50, A47, A51, A44, POLYNOM3:22;

b1 is Element of Bags (n + 1) by PRE_POLY:def 12;

then b1 = b1n bag_extend (b1 . n) by Def1

.= b2 by A49, A46, A53, A52, Def1 ;

hence n19 = n29 by A38, A39, A41, FUNCT_1:def 4; :: thesis: verum

end;assume that

A38: n19 in dom p and

A39: n29 in dom p and

A40: p . n19 = p . n29 ; :: thesis: n19 = n29

dom p = dom u by A36, FUNCT_2:def 1;

then reconsider n1 = n19, n2 = n29 as Element of NAT by A38, A39;

A41: dom u = dom (decomp b) by A9, FINSEQ_3:29

.= dom (divisors b) by PRE_POLY:def 17 ;

then A42: (divisors b) . n1 in rng (divisors b) by A38, FUNCT_1:def 3;

then reconsider b1 = (divisors b) . n1 as bag of n + 1 ;

A43: (divisors b) . n2 in rng (divisors b) by A39, A41, FUNCT_1:def 3;

then reconsider b2 = (divisors b) . n2 as bag of n + 1 ;

n < n + 1 by NAT_1:13;

then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3;

A44: ( (Card s) | (((b1 . n) + 1) -' 1) = Card (s | (((b1 . n) + 1) -' 1)) & (Card s) | (((b2 . n) + 1) -' 1) = Card (s | (((b2 . n) + 1) -' 1)) ) by POLYNOM3:16;

b2 divides b by A43, Th7;

then b2n divides bn by Th4;

then b2n in rng (divisors bn) by Th7;

then consider i2 being object such that

A45: i2 in dom (divisors bn) and

A46: b2n = (divisors bn) . i2 by FUNCT_1:def 3;

reconsider i2 = i2 as Element of NAT by A45;

A47: ( (b2 . n) + 1 in dom s & i2 in dom (s . ((b2 . n) + 1)) ) by A35, A39, A45, A46;

b1 divides b by A42, Th7;

then b1n divides bn by Th4;

then b1n in rng (divisors bn) by Th7;

then consider i1 being object such that

A48: i1 in dom (divisors bn) and

A49: b1n = (divisors bn) . i1 by FUNCT_1:def 3;

reconsider i1 = i1 as Element of NAT by A48;

A50: p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i1 by A35, A38, A48, A49;

A51: p . n2 = (Sum (Card (s | (((b2 . n) + 1) -' 1)))) + i2 by A35, A39, A45, A46;

A52: b2 is Element of Bags (n + 1) by PRE_POLY:def 12;

( (b1 . n) + 1 in dom s & i1 in dom (s . ((b1 . n) + 1)) ) by A35, A38, A48, A49;

then A53: ( (b1 . n) + 1 = (b2 . n) + 1 & i1 = i2 ) by A40, A50, A47, A51, A44, POLYNOM3:22;

b1 is Element of Bags (n + 1) by PRE_POLY:def 12;

then b1 = b1n bag_extend (b1 . n) by Def1

.= b2 by A49, A46, A53, A52, Def1 ;

hence n19 = n29 by A38, A39, A41, FUNCT_1:def 4; :: thesis: verum

dom (FlattenSeq s) c= rng p

proof

then A77:
rng p = dom (FlattenSeq s)
by XBOOLE_0:def 10;
let n19 be object ; :: according to TARSKI:def 3 :: thesis: ( not n19 in dom (FlattenSeq s) or n19 in rng p )

assume A55: n19 in dom (FlattenSeq s) ; :: thesis: n19 in rng p

then reconsider n1 = n19 as Element of NAT ;

consider i, j being Nat such that

A56: i in dom s and

A57: j in dom (s . i) and

A58: n1 = (Sum (Card (s | (i -' 1)))) + j and

(s . i) . j = (FlattenSeq s) . n1 by A55, PRE_POLY:29;

s . i in the carrier of R * by A16, A56, FUNCT_2:5;

then A59: s . i is FinSequence of the carrier of R by FINSEQ_1:def 11;

reconsider bj = (divisors bn) /. j as bag of n ;

set bij = bj bag_extend (i -' 1);

reconsider p9 = x . (i -' 1), q9 = y . (((b . n) + 1) -' i) as Polynomial of n,R by POLYNOM1:def 11;

A60: (bj bag_extend (i -' 1)) . n = i -' 1 by Def1;

1 <= i by A56, FINSEQ_3:25;

then A61: ((bj bag_extend (i -' 1)) . n) + 1 = i by A60, XREAL_1:235;

A62: dom u = dom (decomp b) by A9, FINSEQ_3:29

.= dom (divisors b) by PRE_POLY:def 17 ;

( p9 = x . (i -' 1) & q9 = y . (((b . n) + 1) -' i) ) ;

then len (s . i) = len (decomp bn) by A14, A16, A56, A59;

then A63: dom (s . i) = dom (decomp bn) by FINSEQ_3:29

.= dom (divisors bn) by PRE_POLY:def 17 ;

then A64: bj = (divisors bn) . j by A57, PARTFUN1:def 6;

then bj in rng (divisors bn) by A57, A63, FUNCT_1:def 3;

then A65: bj divides bn by Th7;

then bj bag_extend (i -' 1) in rng (divisors b) by Th7;

then consider k being object such that

A74: k in dom (divisors b) and

A75: bj bag_extend (i -' 1) = (divisors b) . k by FUNCT_1:def 3;

A76: dom p = dom u by A36, FUNCT_2:def 1;

(divisors bn) . j = (bj bag_extend (i -' 1)) | n by A64, Def1;

then p . k = (Sum (Card (s | ((((bj bag_extend (i -' 1)) . n) + 1) -' 1)))) + j by A35, A57, A63, A74, A75, A62;

hence n19 in rng p by A58, A74, A76, A62, A61, FUNCT_1:def 3; :: thesis: verum

end;assume A55: n19 in dom (FlattenSeq s) ; :: thesis: n19 in rng p

then reconsider n1 = n19 as Element of NAT ;

consider i, j being Nat such that

A56: i in dom s and

A57: j in dom (s . i) and

A58: n1 = (Sum (Card (s | (i -' 1)))) + j and

(s . i) . j = (FlattenSeq s) . n1 by A55, PRE_POLY:29;

s . i in the carrier of R * by A16, A56, FUNCT_2:5;

then A59: s . i is FinSequence of the carrier of R by FINSEQ_1:def 11;

reconsider bj = (divisors bn) /. j as bag of n ;

set bij = bj bag_extend (i -' 1);

reconsider p9 = x . (i -' 1), q9 = y . (((b . n) + 1) -' i) as Polynomial of n,R by POLYNOM1:def 11;

A60: (bj bag_extend (i -' 1)) . n = i -' 1 by Def1;

1 <= i by A56, FINSEQ_3:25;

then A61: ((bj bag_extend (i -' 1)) . n) + 1 = i by A60, XREAL_1:235;

A62: dom u = dom (decomp b) by A9, FINSEQ_3:29

.= dom (divisors b) by PRE_POLY:def 17 ;

( p9 = x . (i -' 1) & q9 = y . (((b . n) + 1) -' i) ) ;

then len (s . i) = len (decomp bn) by A14, A16, A56, A59;

then A63: dom (s . i) = dom (decomp bn) by FINSEQ_3:29

.= dom (divisors bn) by PRE_POLY:def 17 ;

then A64: bj = (divisors bn) . j by A57, PARTFUN1:def 6;

then bj in rng (divisors bn) by A57, A63, FUNCT_1:def 3;

then A65: bj divides bn by Th7;

now :: thesis: for k being object holds (bj bag_extend (i -' 1)) . k <= b . k

then
bj bag_extend (i -' 1) divides b
by PRE_POLY:def 11;let k be object ; :: thesis: (bj bag_extend (i -' 1)) . b_{1} <= b . b_{1}

end;per cases
( k in n + 1 or not k in n + 1 )
;

end;

suppose A66:
k in n + 1
; :: thesis: (bj bag_extend (i -' 1)) . b_{1} <= b . b_{1}

end;

now :: thesis: (bj bag_extend (i -' 1)) . k <= b . kend;

hence
(bj bag_extend (i -' 1)) . k <= b . k
; :: thesis: verumper cases
( k in n or not k in n )
;

end;

suppose A67:
k in n
; :: thesis: (bj bag_extend (i -' 1)) . k <= b . k

then A68:
b . k = bn . k
by FUNCT_1:49;

(bj bag_extend (i -' 1)) . k = ((bj bag_extend (i -' 1)) | n) . k by A67, FUNCT_1:49

.= bj . k by Def1 ;

hence (bj bag_extend (i -' 1)) . k <= b . k by A65, A68, PRE_POLY:def 11; :: thesis: verum

end;(bj bag_extend (i -' 1)) . k = ((bj bag_extend (i -' 1)) | n) . k by A67, FUNCT_1:49

.= bj . k by Def1 ;

hence (bj bag_extend (i -' 1)) . k <= b . k by A65, A68, PRE_POLY:def 11; :: thesis: verum

suppose A69:
not k in n
; :: thesis: (bj bag_extend (i -' 1)) . k <= b . k

A70:
1 <= i
by A56, FINSEQ_3:25;

i <= (b . n) + 1 by A5, A16, A56, FINSEQ_3:25;

then A71: i - 1 <= ((b . n) + 1) - 1 by XREAL_1:9;

Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

then k in {n} by A66, A69, XBOOLE_0:def 3;

then A72: k = n by TARSKI:def 1;

then (bj bag_extend (i -' 1)) . k = i -' 1 by Def1;

hence (bj bag_extend (i -' 1)) . k <= b . k by A72, A70, A71, XREAL_1:233; :: thesis: verum

end;i <= (b . n) + 1 by A5, A16, A56, FINSEQ_3:25;

then A71: i - 1 <= ((b . n) + 1) - 1 by XREAL_1:9;

Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

then k in {n} by A66, A69, XBOOLE_0:def 3;

then A72: k = n by TARSKI:def 1;

then (bj bag_extend (i -' 1)) . k = i -' 1 by Def1;

hence (bj bag_extend (i -' 1)) . k <= b . k by A72, A70, A71, XREAL_1:233; :: thesis: verum

suppose A73:
not k in n + 1
; :: thesis: (bj bag_extend (i -' 1)) . b_{1} <= b . b_{1}

dom (bj bag_extend (i -' 1)) = n + 1
by PARTFUN1:def 2;

hence (bj bag_extend (i -' 1)) . k <= b . k by A73, FUNCT_1:def 2; :: thesis: verum

end;hence (bj bag_extend (i -' 1)) . k <= b . k by A73, FUNCT_1:def 2; :: thesis: verum

then bj bag_extend (i -' 1) in rng (divisors b) by Th7;

then consider k being object such that

A74: k in dom (divisors b) and

A75: bj bag_extend (i -' 1) = (divisors b) . k by FUNCT_1:def 3;

A76: dom p = dom u by A36, FUNCT_2:def 1;

(divisors bn) . j = (bj bag_extend (i -' 1)) | n by A64, Def1;

then p . k = (Sum (Card (s | ((((bj bag_extend (i -' 1)) . n) + 1) -' 1)))) + j by A35, A57, A63, A74, A75, A62;

hence n19 in rng p by A58, A74, A76, A62, A61, FUNCT_1:def 3; :: thesis: verum

len (Sum s) = len s by MATRLIN:def 6;

then A78: dom (Sum s) = dom r by A16, FINSEQ_3:29;

A79: now :: thesis: for k being Nat st k in dom r holds

(Sum s) . k = (g * r) . k

(Sum s) . k = (g * r) . k

let k be Nat; :: thesis: ( k in dom r implies (Sum s) . k = (g * r) . k )

reconsider p = x . (k -' 1), q = y . (((b . n) + 1) -' k) as Polynomial of n,R by POLYNOM1:def 11;

reconsider pq9 = p *' q as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def 11;

assume A80: k in dom r ; :: thesis: (Sum s) . k = (g * r) . k

then reconsider sk = s . k as Element of the carrier of R * by FUNCT_2:5;

reconsider sk = sk as FinSequence of the carrier of R ;

A81: r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A7, A80

.= pq9 by POLYNOM1:def 11 ;

( (Sum s) /. k = (Sum s) . k & s /. k = s . k ) by A16, A78, A80, PARTFUN1:def 6;

hence (Sum s) . k = Sum sk by A78, A80, MATRLIN:def 6

.= (p *' q) . bn by A14, A80

.= g . (r . k) by A17, A81

.= (g * r) . k by A80, FUNCT_1:13 ;

:: thesis: verum

end;reconsider p = x . (k -' 1), q = y . (((b . n) + 1) -' k) as Polynomial of n,R by POLYNOM1:def 11;

reconsider pq9 = p *' q as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def 11;

assume A80: k in dom r ; :: thesis: (Sum s) . k = (g * r) . k

then reconsider sk = s . k as Element of the carrier of R * by FUNCT_2:5;

reconsider sk = sk as FinSequence of the carrier of R ;

A81: r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A7, A80

.= pq9 by POLYNOM1:def 11 ;

( (Sum s) /. k = (Sum s) . k & s /. k = s . k ) by A16, A78, A80, PARTFUN1:def 6;

hence (Sum s) . k = Sum sk by A78, A80, MATRLIN:def 6

.= (p *' q) . bn by A14, A80

.= g . (r . k) by A17, A81

.= (g * r) . k by A80, FUNCT_1:13 ;

:: thesis: verum

A82: now :: thesis: for n1 being Nat st n1 in dom u holds

u . n1 = (FlattenSeq s) . (p . n1)

dom r = dom (g * r)
by FINSEQ_3:120;u . n1 = (FlattenSeq s) . (p . n1)

let n1 be Nat; :: thesis: ( n1 in dom u implies u . n1 = (FlattenSeq s) . (p . n1) )

reconsider b19 = (divisors b) /. n1 as bag of n + 1 ;

assume A83: n1 in dom u ; :: thesis: u . n1 = (FlattenSeq s) . (p . n1)

then consider b1, b2 being bag of n + 1 such that

A84: (decomp b) /. n1 = <*b1,b2*> and

A85: u /. n1 = (Px . b1) * (Py . b2) by A10;

A86: dom u = dom (decomp b) by A9, FINSEQ_3:29;

then A87: <*b1,b2*> = <*b19,(b -' b19)*> by A83, A84, PRE_POLY:def 17;

then A88: b1 = b19 by FINSEQ_1:77;

reconsider xb1n = x . (b1 . n), yb2n = y . (b2 . n) as Polynomial of n,R by POLYNOM1:def 11;

n < n + 1 by NAT_1:13;

then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3;

A89: u . n1 = (Px . b1) * (Py . b2) by A83, A85, PARTFUN1:def 6

.= (xb1n . b1n) * (Py . b2) by Def6

.= (xb1n . b1n) * (yb2n . b2n) by Def6 ;

A90: b2 = b -' b19 by A87, FINSEQ_1:77;

A91: n1 in dom (divisors b) by A83, A86, PRE_POLY:def 17;

then A92: b1 = (divisors b) . n1 by A88, PARTFUN1:def 6;

then b1 in rng (divisors b) by A91, FUNCT_1:def 3;

then A93: b1 divides b by Th7;

then b1n divides bn by Th4;

then b1n in rng (divisors bn) by Th7;

then consider i being object such that

A94: i in dom (divisors bn) and

A95: b1n = (divisors bn) . i by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A94;

A96: b1 . n <= b . n by A93, PRE_POLY:def 11;

then (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6;

then A97: ((b . n) + 1) -' ((b1 . n) + 1) = ((b . n) + 1) - ((b1 . n) + 1) by XREAL_1:233

.= (((b . n) - (b1 . n)) + 1) - 1

.= (b . n) -' (b1 . n) by A96, XREAL_1:233

.= b2 . n by A88, A90, PRE_POLY:def 6 ;

A98: ((b1 . n) + 1) -' 1 = ((b1 . n) + 1) - 1 by NAT_D:37

.= b1 . n ;

then A99: xb1n = x . (((b1 . n) + 1) -' 1) ;

A100: (b1 . n) + 1 in dom s by A35, A83, A92, A94, A95;

then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5;

then reconsider sb1n1 = s . ((b1 . n) + 1) as FinSequence of the carrier of R ;

A101: i in dom (s . ((b1 . n) + 1)) by A35, A83, A92, A94, A95;

then consider B1, B2 being bag of n such that

A102: (decomp bn) /. i = <*B1,B2*> and

A103: sb1n1 /. i = (xb1n . B1) * (yb2n . B2) by A14, A16, A100, A98, A97;

p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i by A35, A83, A92, A94, A95;

then A104: (FlattenSeq s) . (p . n1) = (s . ((b1 . n) + 1)) . i by A100, A101, PRE_POLY:30;

reconsider B19 = (divisors bn) /. i as bag of n ;

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

then A106: <*B1,B2*> = <*B19,(bn -' B19)*> by A94, A102, PRE_POLY:def 17;

then A107: B1 = B19 by FINSEQ_1:77;

then A108: B1 = b1n by A94, A95, PARTFUN1:def 6;

yb2n = y . (((b . n) + 1) -' ((b1 . n) + 1)) by A97;

then len sb1n1 = len (decomp bn) by A14, A16, A100, A99;

then A109: dom sb1n1 = dom (divisors bn) by A105, FINSEQ_3:29;

B2 = bn -' B19 by A106, FINSEQ_1:77;

then B2 = b2n by A88, A90, A107, A108, Th5;

hence u . n1 = (FlattenSeq s) . (p . n1) by A89, A94, A104, A103, A108, A109, PARTFUN1:def 6; :: thesis: verum

end;reconsider b19 = (divisors b) /. n1 as bag of n + 1 ;

assume A83: n1 in dom u ; :: thesis: u . n1 = (FlattenSeq s) . (p . n1)

then consider b1, b2 being bag of n + 1 such that

A84: (decomp b) /. n1 = <*b1,b2*> and

A85: u /. n1 = (Px . b1) * (Py . b2) by A10;

A86: dom u = dom (decomp b) by A9, FINSEQ_3:29;

then A87: <*b1,b2*> = <*b19,(b -' b19)*> by A83, A84, PRE_POLY:def 17;

then A88: b1 = b19 by FINSEQ_1:77;

reconsider xb1n = x . (b1 . n), yb2n = y . (b2 . n) as Polynomial of n,R by POLYNOM1:def 11;

n < n + 1 by NAT_1:13;

then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3;

A89: u . n1 = (Px . b1) * (Py . b2) by A83, A85, PARTFUN1:def 6

.= (xb1n . b1n) * (Py . b2) by Def6

.= (xb1n . b1n) * (yb2n . b2n) by Def6 ;

A90: b2 = b -' b19 by A87, FINSEQ_1:77;

A91: n1 in dom (divisors b) by A83, A86, PRE_POLY:def 17;

then A92: b1 = (divisors b) . n1 by A88, PARTFUN1:def 6;

then b1 in rng (divisors b) by A91, FUNCT_1:def 3;

then A93: b1 divides b by Th7;

then b1n divides bn by Th4;

then b1n in rng (divisors bn) by Th7;

then consider i being object such that

A94: i in dom (divisors bn) and

A95: b1n = (divisors bn) . i by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A94;

A96: b1 . n <= b . n by A93, PRE_POLY:def 11;

then (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6;

then A97: ((b . n) + 1) -' ((b1 . n) + 1) = ((b . n) + 1) - ((b1 . n) + 1) by XREAL_1:233

.= (((b . n) - (b1 . n)) + 1) - 1

.= (b . n) -' (b1 . n) by A96, XREAL_1:233

.= b2 . n by A88, A90, PRE_POLY:def 6 ;

A98: ((b1 . n) + 1) -' 1 = ((b1 . n) + 1) - 1 by NAT_D:37

.= b1 . n ;

then A99: xb1n = x . (((b1 . n) + 1) -' 1) ;

A100: (b1 . n) + 1 in dom s by A35, A83, A92, A94, A95;

then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5;

then reconsider sb1n1 = s . ((b1 . n) + 1) as FinSequence of the carrier of R ;

A101: i in dom (s . ((b1 . n) + 1)) by A35, A83, A92, A94, A95;

then consider B1, B2 being bag of n such that

A102: (decomp bn) /. i = <*B1,B2*> and

A103: sb1n1 /. i = (xb1n . B1) * (yb2n . B2) by A14, A16, A100, A98, A97;

p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i by A35, A83, A92, A94, A95;

then A104: (FlattenSeq s) . (p . n1) = (s . ((b1 . n) + 1)) . i by A100, A101, PRE_POLY:30;

reconsider B19 = (divisors bn) /. i as bag of n ;

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

then A106: <*B1,B2*> = <*B19,(bn -' B19)*> by A94, A102, PRE_POLY:def 17;

then A107: B1 = B19 by FINSEQ_1:77;

then A108: B1 = b1n by A94, A95, PARTFUN1:def 6;

yb2n = y . (((b . n) + 1) -' ((b1 . n) + 1)) by A97;

then len sb1n1 = len (decomp bn) by A14, A16, A100, A99;

then A109: dom sb1n1 = dom (divisors bn) by A105, FINSEQ_3:29;

B2 = bn -' B19 by A106, FINSEQ_1:77;

then B2 = b2n by A88, A90, A107, A108, Th5;

hence u . n1 = (FlattenSeq s) . (p . n1) by A89, A94, A104, A103, A108, A109, PARTFUN1:def 6; :: thesis: verum

then Sum s = g * r by A78, A79, FINSEQ_1:13;

then A110: Sum (FlattenSeq s) = Pxy . b by A19, POLYNOM1:14;

A111: len u = card (dom u) by CARD_1:62

.= card p by A37, CARD_1:62

.= card (dom (FlattenSeq s)) by A54, A77, PRE_POLY:19

.= len (FlattenSeq s) by CARD_1:62 ;

then A112: dom u = dom (FlattenSeq s) by FINSEQ_3:29;

then p is Permutation of (dom u) by A54, A77, FUNCT_2:57;

hence Pxy . b9 = PxPy . b9 by A110, A8, A82, A111, A112, RLVECT_2:6; :: thesis: verum