let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for m1, m2 being non-zero Monomial of n,L holds term (m1 *' m2) = (term m1) + (term m2)
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for m1, m2 being non-zero Monomial of n,L holds term (m1 *' m2) = (term m1) + (term m2)
let m1, m2 be non-zero Monomial of n,L; :: thesis: term (m1 *' m2) = (term m1) + (term m2)
set T = the connected TermOrder of n;
A1: HC (m2, the connected TermOrder of n) <> 0. L ;
HC (m1, the connected TermOrder of n) <> 0. L ;
then reconsider a = coefficient m1, b = coefficient m2 as non zero Element of L by A1, TERMORD:23;
a * b <> 0. L by VECTSP_2:def 1;
then reconsider c = a * b as non zero Element of L by STRUCT_0:def 12;
( m1 = Monom (a,(term m1)) & m2 = Monom (b,(term m2)) ) by POLYNOM7:11;
then term (m1 *' m2) = term (Monom (c,((term m1) + (term m2)))) by TERMORD:3;
hence term (m1 *' m2) = (term m1) + (term m2) by POLYNOM7:10; :: thesis: verum