let R be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; for I being non empty add-closed right-ideal Subset of R
for J being Subset of R holds (I % J) *' J c= I
let I be non empty add-closed right-ideal Subset of R; for J being Subset of R holds (I % J) *' J c= I
let J be Subset of R; (I % J) *' J c= I
let u be object ; TARSKI:def 3 ( not u in (I % J) *' J or u in I )
assume
u in (I % J) *' J
; u in I
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 % J & 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;
A6:
now for j being Element of NAT st 0 <= j & j < len s & S1[j] holds
S1[j + 1]let j be
Element of
NAT ;
( 0 <= j & j < len s & S1[j] implies S1[j + 1] )assume that
0 <= j
and A7:
j < len s
;
( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
verumproof
A8:
(
j + 1
<= len s &
0 + 1
<= j + 1 )
by A7, NAT_1:13;
then consider a,
b being
Element of
R such that A9:
s . (j + 1) = a * b
and A10:
a in I % J
and A11:
b in J
by A2;
j + 1
in Seg (len s)
by A8, FINSEQ_1:1;
then
j + 1
in dom s
by FINSEQ_1:def 3;
then A12:
s . (j + 1) = s /. (j + 1)
by PARTFUN1:def 6;
then A13:
f . (j + 1) = (f . j) + (s /. (j + 1))
by A5, A7;
assume A14:
f . j in I
;
S1[j + 1]
consider d being
Element of
R such that A15:
a = d
and A16:
d * J c= I
by A10;
a * b in { (d * i) where i is Element of R : i in J }
by A11, A15;
hence
S1[
j + 1]
by A14, A12, A13, A9, A16, Def1;
verum
end; end;
A17:
S1[ 0 ]
by A4, Th3;
for j being Element of NAT st 0 <= j & j <= len s holds
S1[j]
from INT_1:sch 7(A17, A6);
hence
u in I
by A1, A3; verum