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

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

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

( term ((a * a') | n,L) = EmptyBag n & coefficient ((a * a') | n,L) = a * a' ) by POLYNOM7:23;
then A2: (a * a') | n,L = Monom (a * a'),(EmptyBag n) by POLYNOM7:11;
( term (a | n,L) = EmptyBag n & coefficient (a | n,L) = a ) by POLYNOM7:23;
then A3: a | n,L = Monom a,(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 POLYNOM1:57;
hence (a * a') | n,L = (a | n,L) *' (a' | n,L) by A1, A2, A3, A4, Th3; :: thesis: verum

end;

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

end;