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;
A1: HC m2,T <> 0. L ;
HC m1,T <> 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 5;
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