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 :: thesis: ( ( a = 0. L & (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) ) or ( a9 = 0. L & (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L)) ) )

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 ;
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 ;
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:28; :: thesis: verum

end;

end;

end;

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

end;

end;