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