set M = { (Sum s) where s is FinSequence of the carrier of R : 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 ) } ;
{ (Sum s) where s is FinSequence of the carrier of R : 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 ) } = I *' J
;
then reconsider M = { (Sum s) where s is FinSequence of the carrier of R : 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 ) } as non empty Subset of R ;
for y, x being Element of R st x in M holds
y * x in M
proof
let y,
x be
Element of
R;
( x in M implies y * x in M )
assume
x in M
;
y * x in M
then consider s being
FinSequence of the
carrier of
R such that A1:
x = 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 &
b in J )
;
set q =
y * s;
A3:
Seg (len (y * s)) =
dom (y * s)
by FINSEQ_1:def 3
.=
dom s
by POLYNOM1:def 1
.=
Seg (len s)
by FINSEQ_1:def 3
;
then A4:
len (y * s) = len s
by FINSEQ_1:6;
A5:
now for i being Element of NAT st 1 <= i & i <= len (y * s) holds
ex b, r being Element of R st
( (y * s) . i = b * r & b in I & r in J )let i be
Element of
NAT ;
( 1 <= i & i <= len (y * s) implies ex b, r being Element of R st
( (y * s) . i = b * r & b in I & r in J ) )assume A6:
( 1
<= i &
i <= len (y * s) )
;
ex b, r being Element of R st
( (y * s) . i = b * r & b in I & r in J )then consider c,
r9 being
Element of
R such that A7:
s . i = c * r9
and A8:
(
c in I &
r9 in J )
by A2, A4;
i in Seg (len s)
by A3, A6, FINSEQ_1:1;
then A9:
i in dom s
by FINSEQ_1:def 3;
then A10:
s /. i = c * r9
by A7, PARTFUN1:def 6;
i in Seg (len (y * s))
by A6, FINSEQ_1:1;
then
i in dom (y * s)
by FINSEQ_1:def 3;
then A11:
(y * s) . i =
(y * s) /. i
by PARTFUN1:def 6
.=
y * (c * r9)
by A9, A10, POLYNOM1:def 1
.=
(y * c) * r9
by GROUP_1:def 3
;
thus
ex
b,
r being
Element of
R st
(
(y * s) . i = b * r &
b in I &
r in J )
verum end;
Sum (y * s) = y * (Sum s)
by BINOM:4;
hence
y * x in M
by A1, A5;
verum
end;
hence
I *' J is left-ideal
; verum