let n be Ordinal; 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 ; 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; (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 )
;
(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;
verum end; suppose A5:
(
a is
zero or
a9 is
zero )
;
(a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))now ( ( 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)) ) )end; hence
(a * a9) | (
n,
L)
= (a | (n,L)) *' (a9 | (n,L))
;
verum end; end;