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 n
for a, a' being non zero Element of 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 n
for a, a' being non zero Element of holds Monom (a * a'),(b + b') = (Monom a,b) *' (Monom a',b')
let b, b' be bag of n; :: thesis: for a, a' being non zero Element of holds Monom (a * a'),(b + b') = (Monom a,b) *' (Monom a',b')
let a, a' be non zero Element of ; :: 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');
consider s being FinSequence of such that
A1: ((Monom a,b) *' (Monom a',b')) . (b + b') = Sum s and
A2: len s = len (decomp (b + 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 + b')) /. k = <*b1,b2*> & s /. k = ((Monom a,b) . b1) * ((Monom a',b') . b2) ) by POLYNOM1:def 26;
set u = b + b';
consider k' being Element of NAT such that
A4: k' in dom (decomp (b + b')) and
A5: (decomp (b + b')) /. k' = <*b,b'*> by PRE_POLY:69;
A6: dom s = Seg (len (decomp (b + b'))) by A2, FINSEQ_1:def 3
.= dom (decomp (b + b')) by FINSEQ_1:def 3 ;
then consider b1, b2 being bag of n such that
A7: (decomp (b + b')) /. k' = <*b1,b2*> and
A8: s /. k' = ((Monom a,b) . b1) * ((Monom a',b') . b2) by A3, A4;
A9: b1 = <*b,b'*> . 1 by A5, A7, FINSEQ_1:61
.= b by FINSEQ_1:61 ;
A10: b2 = <*b,b'*> . 2 by A5, A7, FINSEQ_1:61
.= b' by FINSEQ_1:61 ;
A11: (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 ;

A12: now

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

end;

A16: ( a <> 0. L & a' <> 0. L ) by STRUCT_0:def 12;
then a * a' <> 0. L by VECTSP_2:def 5;
then A17: not a * a' is zero by STRUCT_0:def 12;
A18: (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 ;

A19: now

A20: (Monom a,b) . b <> 0. L by A18, STRUCT_0:def 12;
let u be bag of n; :: thesis: ( u <> b implies not (Monom a,b) . u <> 0. L )
assume A21: u <> b ; :: thesis: not (Monom a,b) . u <> 0. L
consider v being bag of n such that
A22: for b' being bag of n st b' <> v holds
(Monom a,b) . b' = 0. L by POLYNOM7:def 4;
assume (Monom a,b) . u <> 0. L ; :: thesis: contradiction
then u = v by A22;
hence contradiction by A21, A22, A20; :: thesis: verum

end;

A23: now

let k be Element of NAT ; :: thesis: ( k in dom s & k <> k' implies s /. k = 0. L )
assume that
A24: k in dom s and
A25: k <> k' ; :: thesis: s /. k = 0. L
consider b1, b2 being bag of n such that
A26: (decomp (b + b')) /. k = <*b1,b2*> and
A27: s /. k = ((Monom a,b) . b1) * ((Monom a',b') . b2) by A3, A24;

A28: now

assume A29: ( b1 = b & b2 = b' ) ; :: thesis: contradiction
(decomp (b + b')) . k = (decomp (b + b')) /. k by A6, A24, PARTFUN1:def 8
.= (decomp (b + b')) . k' by A4, A5, A26, A29, PARTFUN1:def 8 ;
hence contradiction by A6, A4, A24, A25, FUNCT_1:def 8; :: thesis: verum

end;

now

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

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

then (Monom a,b) . b1 = 0. L by A19;
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 A12;
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 A27; :: thesis: verum

end;

then Sum s = s /. k' by A6, A4, POLYNOM2:5;
then A30: ((Monom a,b) *' (Monom a',b')) . (b + b') <> 0. L by A16, A18, A11, A1, A8, A9, A10, VECTSP_2:def 5;
then A31: term ((Monom a,b) *' (Monom a',b')) = b + b' by POLYNOM7:def 6
.= term (Monom (a * a'),(b + b')) by A17, POLYNOM7:10 ;
A32: 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 A30, POLYNOM7:def 6
.= a * a' by A18, A11, A1, A6, A4, A8, A9, A10, A23, 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 A31, A32, POLYNOM7:11 ; :: thesis: verum