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
x * y in M

proof

let y, x be Element of R; :: thesis: ( x in M implies x * y in M )
assume x in M ; :: thesis: x * y 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 = s * y;
A3: Seg (len (s * y)) = dom (s * y) by FINSEQ_1:def 3
.= dom s by POLYNOM1:def 2
.= Seg (len s) by FINSEQ_1:def 3 ;
then A4: len (s * y) = len s by FINSEQ_1:6;

A5: now :: thesis: for i being Element of NAT st 1 <= i & i <= len (s * y) holds
ex b, r being Element of R st
( (s * y) . i = b * r & b in I & r in J )

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len (s * y) implies ex b, r being Element of R st
( (s * y) . i = b * r & b in I & r in J ) )
assume A6: ( 1 <= i & i <= len (s * y) ) ; :: thesis: ex b, r being Element of R st
( (s * y) . 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 (s * y)) by A6, FINSEQ_1:1;
then i in dom (s * y) by FINSEQ_1:def 3;
then A11: (s * y) . i = (s * y) /. i by PARTFUN1:def 6
.= (c * r9) * y by A9, A10, POLYNOM1:def 2
.= c * (r9 * y) by GROUP_1:def 3 ;
thus ex b, r being Element of R st
( (s * y) . i = b * r & b in I & r in J ) :: thesis: verum

proof

take c ; :: thesis: ex r being Element of R st
( (s * y) . i = c * r & c in I & r in J )
take r9 * y ; :: thesis: ( (s * y) . i = c * (r9 * y) & c in I & r9 * y in J )
thus ( (s * y) . i = c * (r9 * y) & c in I & r9 * y in J ) by A8, A11, Def3; :: thesis: verum

end;

end;

Sum (s * y) = (Sum s) * y by BINOM:5;
hence x * y in M by A1, A5; :: thesis: verum

end;

hence I *' J is right-ideal ; :: thesis: verum