let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for b, b9 being bag of n
for a, a9 being non zero Element of L holds Monom (a * a9),(b + b9) = (Monom a,b) *' (Monom a9,b9)
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for b, b9 being bag of n
for a, a9 being non zero Element of L holds Monom (a * a9),(b + b9) = (Monom a,b) *' (Monom a9,b9)
let b, b9 be bag of n; :: thesis: for a, a9 being non zero Element of L holds Monom (a * a9),(b + b9) = (Monom a,b) *' (Monom a9,b9)
let a, a9 be non zero Element of L; :: thesis: Monom (a * a9),(b + b9) = (Monom a,b) *' (Monom a9,b9)
set m1 = Monom a,b;
set m2 = Monom a9,b9;
set m = Monom (a * a9),(b + b9);
set m3 = (Monom a,b) *' (Monom a9,b9);
consider s being FinSequence of L such that
A1: ((Monom a,b) *' (Monom a9,b9)) . (b + b9) = Sum s and
A2: len s = len (decomp (b + b9)) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp (b + b9)) /. k = <*b1,b2*> & s /. k = ((Monom a,b) . b1) * ((Monom a9,b9) . b2) ) by POLYNOM1:def 26;
set u = b + b9;
consider k9 being Element of NAT such that
A4: k9 in dom (decomp (b + b9)) and
A5: (decomp (b + b9)) /. k9 = <*b,b9*> by PRE_POLY:69;
A6: dom s = Seg (len (decomp (b + b9))) by A2, FINSEQ_1:def 3
.= dom (decomp (b + b9)) by FINSEQ_1:def 3 ;
then consider b1, b2 being bag of n such that
A7: (decomp (b + b9)) /. k9 = <*b1,b2*> and
A8: s /. k9 = ((Monom a,b) . b1) * ((Monom a9,b9) . b2) by A3, A4;
A9: b1 = <*b,b9*> . 1 by A5, A7, FINSEQ_1:61
.= b by FINSEQ_1:61 ;
A10: b2 = <*b,b9*> . 2 by A5, A7, FINSEQ_1:61
.= b9 by FINSEQ_1:61 ;
A11: (Monom a9,b9) . b9 = (Monom a9,b9) . (term (Monom a9,b9)) by POLYNOM7:10
.= coefficient (Monom a9,b9) by POLYNOM7:def 7
.= a9 by POLYNOM7:9 ;

A12: now

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

end;

a * a9 <> 0. L by VECTSP_2:def 5;
then A17: not a * a9 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;
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 b9 being bag of n st b9 <> v holds
(Monom a,b) . b9 = 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 <> k9 implies s /. k = 0. L )
assume that
A24: k in dom s and
A25: k <> k9 ; :: thesis: s /. k = 0. L
consider b1, b2 being bag of n such that
A26: (decomp (b + b9)) /. k = <*b1,b2*> and
A27: s /. k = ((Monom a,b) . b1) * ((Monom a9,b9) . b2) by A3, A24;

A28: now

assume A29: ( b1 = b & b2 = b9 ) ; :: thesis: contradiction
(decomp (b + b9)) . k = (decomp (b + b9)) /. k by A6, A24, PARTFUN1:def 8
.= (decomp (b + b9)) . k9 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 <> b9 ) by A28;

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

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

end;

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

then (Monom a9,b9) . b2 = 0. L by A12;
hence ((Monom a,b) . b1) * ((Monom a9,b9) . 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 /. k9 by A6, A4, POLYNOM2:5;
then A30: ((Monom a,b) *' (Monom a9,b9)) . (b + b9) <> 0. L by A18, A11, A1, A8, A9, A10, VECTSP_2:def 5;
then A31: term ((Monom a,b) *' (Monom a9,b9)) = b + b9 by POLYNOM7:def 6
.= term (Monom (a * a9),(b + b9)) by A17, POLYNOM7:10 ;
A32: coefficient ((Monom a,b) *' (Monom a9,b9)) = ((Monom a,b) *' (Monom a9,b9)) . (term ((Monom a,b) *' (Monom a9,b9))) by POLYNOM7:def 7
.= ((Monom a,b) *' (Monom a9,b9)) . (b + b9) by A30, POLYNOM7:def 6
.= a * a9 by A18, A11, A1, A6, A4, A8, A9, A10, A23, POLYNOM2:5
.= coefficient (Monom (a * a9),(b + b9)) by POLYNOM7:9 ;
thus Monom (a * a9),(b + b9) = Monom (coefficient (Monom (a * a9),(b + b9))),(term (Monom (a * a9),(b + b9))) by POLYNOM7:11
.= (Monom a,b) *' (Monom a9,b9) by A31, A32, POLYNOM7:11 ; :: thesis: verum