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
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;
now :: thesis: for b9 being object st b9 in Bags (n + 1) holds
Pxy . 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 ;
n < n + 1 by NAT_1:13;
then reconsider bn = b | n as Element of Bags n by Th3;
defpred S1[ 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 () and
A10: for k being Element of NAT st k in dom u holds
ex b1, b2 being bag of n + 1 st
( () /. k = <*b1,b2*> & u /. k = (Px . b1) * (Py . b2) ) by ;
A11: now :: thesis: for e9 being object st e9 in dom r holds
ex u being object st
( u in the carrier of R * & S1[e9,u] )
let e9 be object ; :: thesis: ( e9 in dom r implies ex u being object st
( u in the carrier of R * & S1[e9,u] ) )

assume e9 in dom r ; :: thesis: ex u being object st
( u in the carrier of R * & S1[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;
S1[e,fcr] by A12;
hence ex u being object st
( u in the carrier of R * & S1[e9,u] ) by A13; :: thesis: verum
end;
consider s being Function of (dom r),( the carrier of R *) such that
A14: for e being object st e in dom r holds
S1[e,s . e] from 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 ;
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 ;
A19: Sum (g * r) = Pxy . b by ;
0 + 1 <= len r by ;
then A20: 1 in dom s by ;
A21: now :: thesis: len (s . 1) <> 0
reconsider 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 ;
( p9 = x . (1 -' 1) & q9 = y . (((b . n) + 1) -' 1) ) ;
hence len (s . 1) <> 0 by A14, A16, A20, A22; :: thesis: verum
end;
defpred S2[ object , object ] means for i, n1 being Element of NAT
for b1 being bag of n + 1 st n1 = R & b1 = () . 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 () & S2[n19,n29] )
let n19 be object ; :: thesis: ( n19 in dom u implies ex n29 being object st
( n29 in dom () & S2[n19,n29] ) )

assume A24: n19 in dom u ; :: thesis: ex n29 being object st
( n29 in dom () & S2[n19,n29] )

then reconsider n1 = n19 as Element of NAT ;
dom u = dom () by
.= dom () by PRE_POLY:def 17 ;
then A25: (divisors b) . n1 in rng () by ;
then reconsider b1 = () . n1 as bag of n + 1 ;
A26: b1 divides b by ;
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 ;
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 ;
then s . ((b1 . n) + 1) is Element of the carrier of R * by ;
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 () by ;
for i9, n19 being Element of NAT
for b19 being bag of n + 1 st n19 = n1 & b19 = () . 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 ;
hence ex n29 being object st
( n29 in dom () & S2[n19,n29] ) by A34; :: thesis: verum
end;
consider p being Function of (dom u),(dom ()) such that
A35: for x being object st x in dom u holds
S2[x,p . x] from 1 in dom (Card s) by ;
then Sum (Card s) >= (Card s) . 1 by POLYNOM3:4;
then Sum (Card s) > 0 by ;
then len () > 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
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 ;
then reconsider n1 = n19, n2 = n29 as Element of NAT by ;
A41: dom u = dom () by
.= dom () by PRE_POLY:def 17 ;
then A42: (divisors b) . n1 in rng () by ;
then reconsider b1 = () . n1 as bag of n + 1 ;
A43: (divisors b) . n2 in rng () by ;
then reconsider b2 = () . 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 ;
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 ;
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 ;
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 ; :: thesis: verum
end;
then A54: p is one-to-one by FUNCT_1:def 4;
dom () c= rng p
proof
let n19 be object ; :: according to TARSKI:def 3 :: thesis: ( not n19 in dom () or n19 in rng p )
assume A55: n19 in dom () ; :: 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 = () . n1 by ;
s . i in the carrier of R * by ;
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 ;
then A61: ((bj bag_extend (i -' 1)) . n) + 1 = i by ;
A62: dom u = dom () by
.= dom () 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 ;
then bj in rng (divisors bn) by ;
then A65: bj divides bn by Th7;
now :: thesis: for k being object holds (bj bag_extend (i -' 1)) . k <= b . k
let k be object ; :: thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1
per cases ( k in n + 1 or not k in n + 1 ) ;
suppose A66: k in n + 1 ; :: thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1
now :: thesis: (bj bag_extend (i -' 1)) . k <= b . k
per cases ( k in n or not k in n ) ;
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
.= bj . k by Def1 ;
hence (bj bag_extend (i -' 1)) . k <= b . k by ; :: thesis: verum
end;
suppose A69: not k in n ; :: thesis: (bj bag_extend (i -' 1)) . k <= b . k
A70: 1 <= i by ;
i <= (b . n) + 1 by ;
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 ;
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 ; :: thesis: verum
end;
end;
end;
hence (bj bag_extend (i -' 1)) . k <= b . k ; :: thesis: verum
end;
suppose A73: not k in n + 1 ; :: thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1
dom (bj bag_extend (i -' 1)) = n + 1 by PARTFUN1:def 2;
hence (bj bag_extend (i -' 1)) . k <= b . k by ; :: thesis: verum
end;
end;
end;
then bj bag_extend (i -' 1) divides b by PRE_POLY:def 11;
then bj bag_extend (i -' 1) in rng () by Th7;
then consider k being object such that
A74: k in dom () and
A75: bj bag_extend (i -' 1) = () . k by FUNCT_1:def 3;
A76: dom p = dom u by ;
(divisors bn) . j = (bj bag_extend (i -' 1)) | n by ;
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 ; :: thesis: verum
end;
then A77: rng p = dom () by XBOOLE_0:def 10;
len (Sum s) = len s by MATRLIN:def 6;
then A78: dom (Sum s) = dom r by ;
A79: now :: thesis: for k being Nat st k in dom r holds
(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
.= pq9 by POLYNOM1:def 11 ;
( (Sum s) /. k = (Sum s) . k & s /. k = s . k ) by ;
hence (Sum s) . k = Sum sk by
.= (p *' q) . bn by
.= g . (r . k) by
.= (g * r) . k by ;
:: thesis: verum
end;
A82: now :: thesis: for n1 being Nat st n1 in dom u holds
u . n1 = () . (p . n1)
let n1 be Nat; :: thesis: ( n1 in dom u implies u . n1 = () . (p . n1) )
reconsider b19 = () /. n1 as bag of n + 1 ;
assume A83: n1 in dom u ; :: thesis: u . n1 = () . (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 () by ;
then A87: <*b1,b2*> = <*b19,(b -' b19)*> by ;
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
.= (xb1n . b1n) * (Py . b2) by Def6
.= (xb1n . b1n) * (yb2n . b2n) by Def6 ;
A90: b2 = b -' b19 by ;
A91: n1 in dom () by ;
then A92: b1 = () . n1 by ;
then b1 in rng () by ;
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 ;
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
.= b2 . n by ;
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 ;
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 ;
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 ;
then A107: B1 = B19 by FINSEQ_1:77;
then A108: B1 = b1n by ;
yb2n = y . (((b . n) + 1) -' ((b1 . n) + 1)) by A97;
then len sb1n1 = len (decomp bn) by ;
then A109: dom sb1n1 = dom (divisors bn) by ;
B2 = bn -' B19 by ;
then B2 = b2n by ;
hence u . n1 = () . (p . n1) by ; :: thesis: verum
end;
dom r = dom (g * r) by FINSEQ_3:120;
then Sum s = g * r by ;
then A110: Sum () = Pxy . b by ;
A111: len u = card (dom u) by CARD_1:62
.= card p by
.= card (dom ()) by
.= len () by CARD_1:62 ;
then A112: dom u = dom () by FINSEQ_3:29;
then p is Permutation of (dom u) by ;
hence Pxy . b9 = PxPy . b9 by ; :: thesis: verum
end;
hence (upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9) by FUNCT_2:12; :: thesis: verum
end;