let R be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R holds I *' J c= I /\ J
let I be non empty add-closed right-ideal Subset of R; :: thesis: for J being non empty add-closed left-ideal Subset of R holds I *' J c= I /\ J
let J be non empty add-closed left-ideal Subset of R; :: thesis: I *' J c= I /\ J
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in I *' J or u in I /\ J )
assume u in I *' J ; :: thesis: u in I /\ J
then consider s being FinSequence of the carrier of R such that
A1: Sum s = u and
A2: 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 I & b in J ) ;
consider f being sequence of the carrier of R such that
A3: Sum s = f . (len s) and
A4: f . 0 = 0. R and
A5: for j being Nat
for v being Element of R st j < len s & v = s . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S1[ Element of NAT ] means ( f . $1 in I & f . $1 in J );
A6: now :: thesis: for j being Element of NAT st 0 <= j & j < len s & S1[j] holds
S1[j + 1]
let j be Element of NAT ; :: thesis: ( 0 <= j & j < len s & S1[j] implies S1[j + 1] )
assume that
0 <= j and
A7: j < len s ; :: thesis: ( S1[j] implies S1[j + 1] )
thus ( S1[j] implies S1[j + 1] ) :: thesis: verum
proof
A8: ( j + 1 <= len s & 0 + 1 <= j + 1 ) by A7, NAT_1:13;
then j + 1 in Seg (len s) by FINSEQ_1:1;
then j + 1 in dom s by FINSEQ_1:def 3;
then A9: s . (j + 1) = s /. (j + 1) by PARTFUN1:def 6;
ex a, b being Element of R st
( s . (j + 1) = a * b & a in I & b in J ) by A2, A8;
then A10: ( s /. (j + 1) in I & s /. (j + 1) in J ) by A9, Def2, Def3;
assume A11: ( f . j in I & f . j in J ) ; :: thesis: S1[j + 1]
f . (j + 1) = (f . j) + (s /. (j + 1)) by A5, A7, A9;
hence S1[j + 1] by A11, A10, Def1; :: thesis: verum
end;
end;
A12: S1[ 0 ] by A4, Th2, Th3;
for j being Element of NAT st 0 <= j & j <= len s holds
S1[j] from INT_1:sch 7(A12, A6);
 then ( Sum s in I & Sum s in J ) by A3;
hence u in I /\ J by A1; :: thesis: verum