let R be non empty add-cancelable Abelian add-associative right_zeroed distributive associative commutative left_zeroed doubleLoopStr ; for I, J being non empty right-ideal Subset of R holds (I + J) *' (I /\ J) c= I *' J
let I, J be non empty right-ideal Subset of R; (I + J) *' (I /\ J) c= I *' J
A1:
now for u being object st u in (I *' (I /\ J)) + (J *' (I /\ J)) holds
u in I *' Jlet u be
object ;
( u in (I *' (I /\ J)) + (J *' (I /\ J)) implies u in I *' J )assume
u in (I *' (I /\ J)) + (J *' (I /\ J))
;
u in I *' Jthen consider a,
b being
Element of
R such that A2:
u = a + b
and A3:
a in I *' (I /\ J)
and A4:
b in J *' (I /\ J)
;
consider s being
FinSequence of the
carrier of
R such that A5:
b = Sum s
and A6:
for
i being
Element of
NAT st 1
<= i &
i <= len s holds
ex
a,
b being
Element of
R st
(
s . i = a * b &
a in J &
b in I /\ J )
by A4;
for
i being
Element of
NAT st 1
<= i &
i <= len s holds
ex
x,
y being
Element of
R st
(
s . i = x * y &
x in I &
y in J )
then A8:
Sum s in { (Sum t) where t is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len t holds
ex a, b being Element of R st
( t . i = a * b & a in I & b in J ) }
;
consider q being
FinSequence of the
carrier of
R such that A9:
a = Sum q
and A10:
for
i being
Element of
NAT st 1
<= i &
i <= len q holds
ex
a,
b being
Element of
R st
(
q . i = a * b &
a in I &
b in I /\ J )
by A3;
for
i being
Element of
NAT st 1
<= i &
i <= len q holds
ex
x,
y being
Element of
R st
(
q . i = x * y &
x in I &
y in J )
then
Sum q in { (Sum t) where t is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len t holds
ex a, b being Element of R st
( t . i = a * b & a in I & b in J ) }
;
hence
u in I *' J
by A2, A9, A5, A8, Def1;
verum end;
(I + J) *' (I /\ J) = (I *' (I /\ J)) + (J *' (I /\ J))
by Th80;
hence
(I + J) *' (I /\ J) c= I *' J
by A1; verum