let n be Ordinal; :: thesis: for L being non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L
for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p
let L be non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L
for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p
let p be Series of n,L; :: thesis: for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p
let b be bag of n; :: thesis: for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p
let a be Element of L; :: thesis: a * (b *' p) = (Monom (a,b)) *' p
set q = a * (b *' p);
set q9 = (Monom (a,b)) *' p;
set m = Monom (a,b);

per cases ( a <> 0. L or a = 0. L ) ;

suppose a <> 0. L ; :: thesis: a * (b *' p) = (Monom (a,b)) *' p

then reconsider a = a as non zero Element of L by STRUCT_0:def 12;

A1: now :: thesis: for u being object st u in dom (a * (b *' p)) holds
(a * (b *' p)) . u = ((Monom (a,b)) *' p) . u

let u be object ; :: thesis: ( u in dom (a * (b *' p)) implies (a * (b *' p)) . u = ((Monom (a,b)) *' p) . u )
assume u in dom (a * (b *' p)) ; :: thesis: (a * (b *' p)) . u = ((Monom (a,b)) *' p) . u
then reconsider s = u as bag of n ;
consider t being FinSequence of the carrier of L such that
A2: ((Monom (a,b)) *' p) . s = Sum t and
A3: len t = len (decomp s) and
A4: for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of n st
( (decomp s) /. k = <*b1,b2*> & t /. k = ((Monom (a,b)) . b1) * (p . b2) ) by POLYNOM1:def 10;
A5: dom t = Seg (len (decomp s)) by A3, FINSEQ_1:def 3
.= dom (decomp s) by FINSEQ_1:def 3 ;
A6: term (Monom (a,b)) = b by POLYNOM7:10;

now :: thesis: ( ( b divides s & (a * (b *' p)) . s = ((Monom (a,b)) *' p) . s ) or ( not b divides s & (a * (b *' p)) . u = ((Monom (a,b)) *' p) . u ) )

per cases ( b divides s or not b divides s ) ;

case A7: b divides s ; :: thesis: (a * (b *' p)) . s = ((Monom (a,b)) *' p) . s

A8: (a * (b *' p)) . s = a * ((b *' p) . s) by POLYNOM7:def 9
.= a * (p . (s -' b)) by A7, Def1 ;
consider s9 being bag of n such that
A9: b + s9 = s by A7, TERMORD:1;
consider i being Element of NAT such that
A10: i in dom (decomp s) and
A11: (decomp s) /. i = <*b,s9*> by A9, PRE_POLY:69;
consider b1, b2 being bag of n such that
A12: (decomp s) /. i = <*b1,b2*> and
A13: t /. i = ((Monom (a,b)) . b1) * (p . b2) by A4, A5, A10;
A14: b2 = <*b,s9*> . 2 by A11, A12, FINSEQ_1:44
.= s9 ;
A15: s -' b = s9 by A9, PRE_POLY:48;

A16: now :: thesis: for i9 being Element of NAT st i9 in dom t & i9 <> i holds
t /. i9 = 0. L

let i9 be Element of NAT ; :: thesis: ( i9 in dom t & i9 <> i implies t /. i9 = 0. L )
assume that
A17: i9 in dom t and
A18: i9 <> i ; :: thesis: t /. i9 = 0. L
consider b19, b29 being bag of n such that
A19: (decomp s) /. i9 = <*b19,b29*> and
A20: t /. i9 = ((Monom (a,b)) . b19) * (p . b29) by A4, A17;
consider h1, h2 being bag of n such that
A21: (decomp s) /. i9 = <*h1,h2*> and
A22: s = h1 + h2 by A5, A17, PRE_POLY:68;
A23: s -' h1 = h2 by A22, PRE_POLY:48;
A24: h1 = <*b19,b29*> . 1 by A19, A21, FINSEQ_1:44
.= b19 ;

now :: thesis: not (Monom (a,b)) . b19 <> 0. L

assume (Monom (a,b)) . b19 <> 0. L ; :: thesis: contradiction
then b19 = b by A6, POLYNOM7:def 5;
then (decomp s) . i9 = (decomp s) /. i by A5, A11, A15, A17, A21, A24, A23, PARTFUN1:def 6
.= (decomp s) . i by A10, PARTFUN1:def 6 ;
hence contradiction by A5, A10, A17, A18, FUNCT_1:def 4; :: thesis: verum

end;

hence t /. i9 = 0. L by A20; :: thesis: verum

end;

b1 = <*b,s9*> . 1 by A11, A12, FINSEQ_1:44
.= b ;
then Sum t = (coefficient (Monom (a,b))) * (p . (s -' b)) by A6, A5, A10, A15, A13, A14, A16, POLYNOM2:3
.= a * (p . (s -' b)) by POLYNOM7:9 ;
hence (a * (b *' p)) . s = ((Monom (a,b)) *' p) . s by A2, A8; :: thesis: verum

end;

case A25: not b divides s ; :: thesis: (a * (b *' p)) . u = ((Monom (a,b)) *' p) . u

consider t being FinSequence of the carrier of L such that
A26: ((Monom (a,b)) *' p) . s = Sum t and
A27: len t = len (decomp s) and
A28: for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of n st
( (decomp s) /. k = <*b1,b2*> & t /. k = ((Monom (a,b)) . b1) * (p . b2) ) by POLYNOM1:def 10;

A29: now :: thesis: for k being Nat st k in dom t holds
t /. k = 0. L

let k be Nat; :: thesis: ( k in dom t implies t /. k = 0. L )
assume A30: k in dom t ; :: thesis: t /. k = 0. L
then consider b19, b29 being bag of n such that
A31: (decomp s) /. k = <*b19,b29*> and
A32: t /. k = ((Monom (a,b)) . b19) * (p . b29) by A28;
A33: dom t = Seg (len (decomp s)) by A27, FINSEQ_1:def 3
.= dom (decomp s) by FINSEQ_1:def 3 ;

now :: thesis: ( ( b19 = term (Monom (a,b)) & contradiction ) or ( b19 <> term (Monom (a,b)) & (Monom (a,b)) . b19 = 0. L ) )

per cases ( b19 = term (Monom (a,b)) or b19 <> term (Monom (a,b)) ) ;

case A34: b19 = term (Monom (a,b)) ; :: thesis: contradiction

consider h1, h2 being bag of n such that
A35: (decomp s) /. k = <*h1,h2*> and
A36: s = h1 + h2 by A30, A33, PRE_POLY:68;
h1 = <*b19,b29*> . 1 by A31, A35, FINSEQ_1:44
.= b19 ;
hence contradiction by A6, A25, A34, A36, TERMORD:1; :: thesis: verum

end;

case b19 <> term (Monom (a,b)) ; :: thesis: (Monom (a,b)) . b19 = 0. L

hence (Monom (a,b)) . b19 = 0. L by Lm8; :: thesis: verum

end;

end;

end;

hence t /. k = 0. L by A32; :: thesis: verum

end;

(a * (b *' p)) . s = a * ((b *' p) . s) by POLYNOM7:def 9
.= a * (0. L) by A25, Def1
.= 0. L ;
hence (a * (b *' p)) . u = ((Monom (a,b)) *' p) . u by A26, A29, MATRLIN:11; :: thesis: verum

end;

end;

end;

hence (a * (b *' p)) . u = ((Monom (a,b)) *' p) . u ; :: thesis: verum

end;

dom (a * (b *' p)) = Bags n by FUNCT_2:def 1
.= dom ((Monom (a,b)) *' p) by FUNCT_2:def 1 ;
hence a * (b *' p) = (Monom (a,b)) *' p by A1, FUNCT_1:2; :: thesis: verum

end;

suppose A37: a = 0. L ; :: thesis: a * (b *' p) = (Monom (a,b)) *' p

A38: now :: thesis: for u being object st u in dom (Monom (a,b)) holds
(Monom (a,b)) . u = (0_ (n,L)) . u

let u be object ; :: thesis: ( u in dom (Monom (a,b)) implies (Monom (a,b)) . u = (0_ (n,L)) . u )
assume u in dom (Monom (a,b)) ; :: thesis: (Monom (a,b)) . u = (0_ (n,L)) . u
then reconsider u9 = u as Element of Bags n ;

now :: thesis: ( ( u9 = term (Monom (a,b)) & (Monom (a,b)) . u = (0_ (n,L)) . u ) or ( u9 <> term (Monom (a,b)) & (Monom (a,b)) . u = (0_ (n,L)) . u ) )

per cases ( u9 = term (Monom (a,b)) or u9 <> term (Monom (a,b)) ) ;

case A39: u9 = term (Monom (a,b)) ; :: thesis: (Monom (a,b)) . u = (0_ (n,L)) . u

coefficient (Monom (a,b)) = 0. L by A37, POLYNOM7:8;
hence (Monom (a,b)) . u = (0_ (n,L)) . u by A39, POLYNOM1:22; :: thesis: verum

end;

case u9 <> term (Monom (a,b)) ; :: thesis: (Monom (a,b)) . u = (0_ (n,L)) . u

then (Monom (a,b)) . u9 = 0. L by Lm8
.= (0_ (n,L)) . u9 by POLYNOM1:22 ;
hence (Monom (a,b)) . u = (0_ (n,L)) . u ; :: thesis: verum

end;

end;

end;

hence (Monom (a,b)) . u = (0_ (n,L)) . u ; :: thesis: verum

end;

dom (Monom (a,b)) = Bags n by FUNCT_2:def 1
.= dom (0_ (n,L)) by FUNCT_2:def 1 ;
then A40: Monom (a,b) = 0_ (n,L) by A38, FUNCT_1:2;

A41: now :: thesis: for u being object st u in dom (a * (b *' p)) holds
(a * (b *' p)) . u = (0_ (n,L)) . u

let u be object ; :: thesis: ( u in dom (a * (b *' p)) implies (a * (b *' p)) . u = (0_ (n,L)) . u )
assume u in dom (a * (b *' p)) ; :: thesis: (a * (b *' p)) . u = (0_ (n,L)) . u
then reconsider u9 = u as bag of n ;
(a * (b *' p)) . u9 = (0. L) * ((b *' p) . u9) by A37, POLYNOM7:def 9
.= 0. L
.= (0_ (n,L)) . u9 by POLYNOM1:22 ;
hence (a * (b *' p)) . u = (0_ (n,L)) . u ; :: thesis: verum

end;

dom (a * (b *' p)) = Bags n by FUNCT_2:def 1
.= dom (0_ (n,L)) by FUNCT_2:def 1 ;
then a * (b *' p) = 0_ (n,L) by A41, FUNCT_1:2;
hence a * (b *' p) = (Monom (a,b)) *' p by A40, Th5; :: thesis: verum

end;

end;