let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for a, a9 being Element of L holds (a * a9) | n,L = (a | n,L) *' (a9 | n,L)
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for a, a9 being Element of L holds (a * a9) | n,L = (a | n,L) *' (a9 | n,L)
let a, a9 be Element of L; :: thesis: (a * a9) | n,L = (a | n,L) *' (a9 | n,L)

per cases ( ( not a is zero & not a9 is zero ) or a is zero or a9 is zero ) ;

suppose A1: ( not a is zero & not a9 is zero ) ; :: thesis: (a * a9) | n,L = (a | n,L) *' (a9 | n,L)

( term ((a * a9) | n,L) = EmptyBag n & coefficient ((a * a9) | n,L) = a * a9 ) by POLYNOM7:23;
then A2: (a * a9) | n,L = Monom (a * a9),(EmptyBag n) by POLYNOM7:11;
( term (a9 | n,L) = EmptyBag n & coefficient (a9 | n,L) = a9 ) by POLYNOM7:23;
then A3: a9 | n,L = Monom a9,(EmptyBag n) by POLYNOM7:11;
( term (a | n,L) = EmptyBag n & coefficient (a | n,L) = a ) by POLYNOM7:23;
then A4: a | n,L = Monom a,(EmptyBag n) by POLYNOM7:11;
(EmptyBag n) + (EmptyBag n) = EmptyBag n by PRE_POLY:53;
hence (a * a9) | n,L = (a | n,L) *' (a9 | n,L) by A1, A2, A4, A3, Th3; :: thesis: verum

end;

suppose A5: ( a is zero or a9 is zero ) ; :: thesis: (a * a9) | n,L = (a | n,L) *' (a9 | n,L)

now

per cases ( a = 0. L or a9 = 0. L ) by A5, STRUCT_0:def 12;

case A6: a = 0. L ; :: thesis: (a * a9) | n,L = (a | n,L) *' (a9 | n,L)

then a * a9 = 0. L by BINOM:1;
then A7: (a * a9) | n,L = 0_ n,L by POLYNOM7:19;
a | n,L = 0_ n,L by A6, POLYNOM7:19;
hence (a * a9) | n,L = (a | n,L) *' (a9 | n,L) by A7, Th2; :: thesis: verum

end;

case A8: a9 = 0. L ; :: thesis: (a * a9) | n,L = (a | n,L) *' (a9 | n,L)

then a * a9 = 0. L by BINOM:2;
then A9: (a * a9) | n,L = 0_ n,L by POLYNOM7:19;
a9 | n,L = 0_ n,L by A8, POLYNOM7:19;
hence (a * a9) | n,L = (a | n,L) *' (a9 | n,L) by A9, POLYNOM1:87; :: thesis: verum

end;

end;

end;

hence (a * a9) | n,L = (a | n,L) *' (a9 | n,L) ; :: thesis: verum

end;

end;