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)
consider T being connected TermOrder of n;
( m1 <> 0_ n,L & m2 <> 0_ n,L ) by POLYNOM7:def 2;
then A1: ( HC m1,T <> 0. L & HC m2,T <> 0. L ) by TERMORD:17;
then reconsider a = coefficient m1, b = coefficient m2 as non zero Element of L by TERMORD:23;
( coefficient m1 <> 0. L & coefficient m2 <> 0. L ) by A1, TERMORD:23;
then a * b <> 0. L by VECTSP_2:def 5;
then reconsider c = a * b as non zero Element of L by STRUCT_0:def 15;
( 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