let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for b, b' being bag of
for a, a' being non zero Element of L holds Monom (a * a'),(b + b') = (Monom a,b) *' (Monom a',b')
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for b, b' being bag of
for a, a' being non zero Element of L holds Monom (a * a'),(b + b') = (Monom a,b) *' (Monom a',b')
let b, b' be bag of ; :: thesis: for a, a' being non zero Element of L holds Monom (a * a'),(b + b') = (Monom a,b) *' (Monom a',b')
let a, a' be non zero Element of L; :: thesis: Monom (a * a'),(b + b') = (Monom a,b) *' (Monom a',b')
set m1 = Monom a,b;
set m2 = Monom a',b';
set m = Monom (a * a'),(b + b');
set m3 = (Monom a,b) *' (Monom a',b');
A1: ( a <> 0. L & a' <> 0. L ) by STRUCT_0:def 15;
then a * a' <> 0. L by VECTSP_2:def 5;
then A2: not a * a' is zero by STRUCT_0:def 15;
A3: (Monom a,b) . b = (Monom a,b) . (term (Monom a,b)) by POLYNOM7:10
.= coefficient (Monom a,b) by POLYNOM7:def 7
.= a by POLYNOM7:9 ;
A4: (Monom a',b') . b' = (Monom a',b') . (term (Monom a',b')) by POLYNOM7:10
.= coefficient (Monom a',b') by POLYNOM7:def 7
.= a' by POLYNOM7:9 ;

A5: now

let u be bag of ; :: thesis: ( u <> b implies not (Monom a,b) . u <> 0. L )
assume A6: u <> b ; :: thesis: not (Monom a,b) . u <> 0. L
consider v being bag of such that
A7: for b' being bag of st b' <> v holds
(Monom a,b) . b' = 0. L by POLYNOM7:def 4;
assume (Monom a,b) . u <> 0. L ; :: thesis: contradiction
then A8: u = v by A7;
(Monom a,b) . b <> 0. L by A3, STRUCT_0:def 15;
hence contradiction by A6, A7, A8; :: thesis: verum

end;

A9: now

let u be bag of ; :: thesis: ( u <> b' implies not (Monom a',b') . u <> 0. L )
assume A10: u <> b' ; :: thesis: not (Monom a',b') . u <> 0. L
consider v being bag of such that
A11: for b' being bag of st b' <> v holds
(Monom a',b') . b' = 0. L by POLYNOM7:def 4;
assume (Monom a',b') . u <> 0. L ; :: thesis: contradiction
then A12: u = v by A11;
(Monom a',b') . b' <> 0. L by A4, STRUCT_0:def 15;
hence contradiction by A10, A11, A12; :: thesis: verum

end;

consider s being FinSequence of L such that
A13: ( ((Monom a,b) *' (Monom a',b')) . (b + b') = Sum s & len s = len (decomp (b + b')) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of st
( (decomp (b + b')) /. k = <*b1,b2*> & s /. k = ((Monom a,b) . b1) * ((Monom a',b') . b2) ) ) ) by POLYNOM1:def 26;
A14: dom s = Seg (len (decomp (b + b'))) by A13, FINSEQ_1:def 3
.= dom (decomp (b + b')) by FINSEQ_1:def 3 ;
set u = b + b';
consider k' being Element of NAT such that
A15: ( k' in dom (decomp (b + b')) & (decomp (b + b')) /. k' = <*b,b'*> ) by POLYNOM1:73;
consider b1, b2 being bag of such that
A16: ( (decomp (b + b')) /. k' = <*b1,b2*> & s /. k' = ((Monom a,b) . b1) * ((Monom a',b') . b2) ) by A13, A14, A15;
A17: b1 = <*b,b'*> . 1 by A15, A16, FINSEQ_1:61
.= b by FINSEQ_1:61 ;
A18: b2 = <*b,b'*> . 2 by A15, A16, FINSEQ_1:61
.= b' by FINSEQ_1:61 ;

A19: now

let k be Element of NAT ; :: thesis: ( k in dom s & k <> k' implies s /. k = 0. L )
assume A20: ( k in dom s & k <> k' ) ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of such that
A21: ( (decomp (b + b')) /. k = <*b1,b2*> & s /. k = ((Monom a,b) . b1) * ((Monom a',b') . b2) ) by A13;

A22: now

assume A23: ( b1 = b & b2 = b' ) ; :: thesis: contradiction
(decomp (b + b')) . k = (decomp (b + b')) /. k by A14, A20, PARTFUN1:def 8
.= (decomp (b + b')) . k' by A15, A21, A23, PARTFUN1:def 8 ;
hence contradiction by A14, A15, A20, FUNCT_1:def 8; :: thesis: verum

end;

now

per cases ( b1 <> b or b2 <> b' ) by A22;

case b1 <> b ; :: thesis: ((Monom a,b) . b1) * ((Monom a',b') . b2) = 0. L

then (Monom a,b) . b1 = 0. L by A5;
hence ((Monom a,b) . b1) * ((Monom a',b') . b2) = 0. L by BINOM:1; :: thesis: verum

end;

case b2 <> b' ; :: thesis: ((Monom a,b) . b1) * ((Monom a',b') . b2) = 0. L

then (Monom a',b') . b2 = 0. L by A9;
hence ((Monom a,b) . b1) * ((Monom a',b') . b2) = 0. L by BINOM:2; :: thesis: verum

end;

end;

end;

hence s /. k = 0. L by A21; :: thesis: verum

end;

then Sum s = s /. k' by A14, A15, POLYNOM2:5;
then A24: ((Monom a,b) *' (Monom a',b')) . (b + b') <> 0. L by A1, A3, A4, A13, A16, A17, A18, VECTSP_2:def 5;
then A25: term ((Monom a,b) *' (Monom a',b')) = b + b' by POLYNOM7:def 6
.= term (Monom (a * a'),(b + b')) by A2, POLYNOM7:10 ;
A26: coefficient ((Monom a,b) *' (Monom a',b')) = ((Monom a,b) *' (Monom a',b')) . (term ((Monom a,b) *' (Monom a',b'))) by POLYNOM7:def 7
.= ((Monom a,b) *' (Monom a',b')) . (b + b') by A24, POLYNOM7:def 6
.= a * a' by A3, A4, A13, A14, A15, A16, A17, A18, A19, POLYNOM2:5
.= coefficient (Monom (a * a'),(b + b')) by POLYNOM7:9 ;
thus Monom (a * a'),(b + b') = Monom (coefficient (Monom (a * a'),(b + b'))),(term (Monom (a * a'),(b + b'))) by POLYNOM7:11
.= (Monom a,b) *' (Monom a',b') by A25, A26, POLYNOM7:11 ; :: thesis: verum