let R be non empty add-cancelable Abelian add-associative right_zeroed distributive associative commutative left_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: (I + J) *' (I /\ J) c= I *' J
A1: now :: thesis: for u being object st u in (I *' (I /\ J)) + (J *' (I /\ J)) holds
u in I *' J
let u be object ; :: thesis: ( u in (I *' (I /\ J)) + (J *' (I /\ J)) implies u in I *' J )
assume u in (I *' (I /\ J)) + (J *' (I /\ J)) ; :: thesis: u in I *' J
then 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 )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len s implies ex x, y being Element of R st
( s . i = x * y & x in I & y in J ) )
assume ( 1 <= i & i <= len s ) ; :: thesis: ex x, y being Element of R st
( s . i = x * y & x in I & y in J )
then A7: ex x, y being Element of R st
( s . i = x * y & x in J & y in I /\ J ) by A6;
I /\ J c= I by XBOOLE_1:17;
hence ex x, y being Element of R st
( s . i = x * y & x in I & y in J ) by A7; :: thesis: verum
end;
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 )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len q implies ex x, y being Element of R st
( q . i = x * y & x in I & y in J ) )
assume ( 1 <= i & i <= len q ) ; :: thesis: ex x, y being Element of R st
( q . i = x * y & x in I & y in J )
then A11: ex x, y being Element of R st
( q . i = x * y & x in I & y in I /\ J ) by A10;
I /\ J c= J by XBOOLE_1:17;
hence ex x, y being Element of R st
( q . i = x * y & x in I & y in J ) by A11; :: thesis: verum
end;
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; :: thesis: verum
end;
(I + J) *' (I /\ J) = (I *' (I /\ J)) + (J *' (I /\ J)) by Th80;
hence (I + J) *' (I /\ J) c= I *' J by A1; :: thesis: verum