let R be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: for J being Subset of R holds (I % J) *' J c= I
let J be Subset of R; :: thesis: (I % J) *' J c= I
now let u be
set ;
:: thesis: ( u in (I % J) *' J implies u in I )assume
u in (I % J) *' J
;
:: thesis: u in Ithen consider s being
FinSequence of the
carrier of
R such that A1:
(
Sum s = u & ( 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
Function of
NAT ,the
carrier of
R such that A2:
(
Sum s = f . (len s) &
f . 0 = 0. R & ( for
j being
Element of
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 13;
defpred S1[
Element of
NAT ]
means f . $1
in I;
A3:
S1[
0 ]
by A2, Th3;
A4:
now let j be
Element of
NAT ;
:: thesis: ( 0 <= j & j < len s & S1[j] implies S1[j + 1] )assume A5:
(
0 <= j &
j < len s )
;
:: thesis: ( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
:: thesis: verumproof
assume A6:
f . j in I
;
:: thesis: S1[j + 1]
A7:
j + 1
<= len s
by A5, NAT_1:13;
A8:
0 + 1
<= j + 1
by XREAL_1:8;
then
j + 1
in Seg (len s)
by A7, FINSEQ_1:3;
then
j + 1
in dom s
by FINSEQ_1:def 3;
then A9:
s . (j + 1) = s /. (j + 1)
by PARTFUN1:def 8;
then A10:
f . (j + 1) = (f . j) + (s /. (j + 1))
by A2, A5;
consider a,
b being
Element of
R such that A11:
(
s . (j + 1) = a * b &
a in I % J &
b in J )
by A1, A7, A8;
consider d being
Element of
R such that A12:
(
a = d &
d * J c= I )
by A11;
a * b in { (d * i) where i is Element of R : i in J }
by A11, A12;
hence
S1[
j + 1]
by A6, A9, A10, A11, A12, Def1;
:: thesis: verum
end; end;
for
j being
Element of
NAT st
0 <= j &
j <= len s holds
S1[
j]
from POLYNOM2:sch 4(A3, A4);
hence
u in I
by A1, A2;
:: thesis: verum end;
hence
(I % J) *' J c= I
by TARSKI:def 3; :: thesis: verum