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 10;
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:44
.= b ;
A10: b2 = <*b,b9*> . 2 by A5, A7, FINSEQ_1:44
.= b9 ;
A11: (Monom (a9,b9)) . b9 = (Monom (a9,b9)) . (term (Monom (a9,b9))) by POLYNOM7:10
.= coefficient (Monom (a9,b9)) by POLYNOM7:def 6
.= a9 by POLYNOM7:9 ;

A12: now :: thesis: for u being bag of n st u <> b9 holds
not (Monom (a9,b9)) . u <> 0. L

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 3;
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 1;
then A16: not a * a9 is zero by STRUCT_0:def 12;
A17: (Monom (a,b)) . b = (Monom (a,b)) . (term (Monom (a,b))) by POLYNOM7:10
.= coefficient (Monom (a,b)) by POLYNOM7:def 6
.= a by POLYNOM7:9 ;

A18: now :: thesis: for u being bag of n st u <> b holds
not (Monom (a,b)) . u <> 0. L

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

end;

A22: now :: thesis: for k being Element of NAT st k in dom s & k <> k9 holds
s /. k = 0. L

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

A27: now :: thesis: ( b1 = b implies not b2 = b9 )

assume A28: ( b1 = b & b2 = b9 ) ; :: thesis: contradiction
(decomp (b + b9)) . k = (decomp (b + b9)) /. k by A6, A23, PARTFUN1:def 6
.= (decomp (b + b9)) . k9 by A4, A5, A25, A28, PARTFUN1:def 6 ;
hence contradiction by A6, A4, A23, A24, FUNCT_1:def 4; :: thesis: verum

end;

now :: thesis: ( ( b1 <> b & ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L ) or ( b2 <> b9 & ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L ) )

per cases ( b1 <> b or b2 <> b9 ) by A27;

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

then (Monom (a,b)) . b1 = 0. L by A18;
hence ((Monom (a,b)) . b1) * ((Monom (a9,b9)) . b2) = 0. L ; :: 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 ; :: thesis: verum

end;

end;

end;

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

end;

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