let R be non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr ; 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; 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; I *' J c= I /\ J
now let u be
set ;
( u in I *' J implies u in I /\ J )assume
u in I *' J
;
u in I /\ Jthen 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
Function of
NAT ,the
carrier of
R such that A3:
Sum s = f . (len s)
and A4:
f . 0 = 0. R
and A5:
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 &
f . $1
in J );
A6:
now 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, XREAL_1:8;
then
j + 1
in Seg (len s)
by 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;
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 )
;
S1[j + 1]
f . (j + 1) = (f . j) + (s /. (j + 1))
by A5, A7, A9;
hence
S1[
j + 1]
by A11, A10, Def1;
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 POLYNOM2:sch 4(A12, A6);
then
(
Sum s in I &
Sum s in J )
by A3;
hence
u in I /\ J
by A1;
verum end;
hence
I *' J c= I /\ J
by TARSKI:def 3; verum