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

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