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 & ( 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;
A2: Sum (s * y) = (Sum s) * y by BINOM:5;
A3: Seg (len (s * y)) = dom (s * y) by FINSEQ_1:def 3
.= dom s by POLYNOM1:def 3
.= Seg (len s) by FINSEQ_1:def 3 ;
then A4: len (s * y) = len s by FINSEQ_1:8;

now

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 A5: ( 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, r' being Element of R such that
A6: ( s . i = c * r' & c in I & r' in J ) by A1, A4;
( i in Seg (len s) & i in Seg (len (s * y)) ) by A3, A5, FINSEQ_1:3;
then A7: ( i in dom s & i in dom (s * y) ) by FINSEQ_1:def 3;
then A8: s /. i = c * r' by A6, PARTFUN1:def 8;
A9: (s * y) . i = (s * y) /. i by A7, PARTFUN1:def 8
.= (c * r') * y by A7, A8, POLYNOM1:def 3
.= c * (r' * y) by GROUP_1:def 4 ;
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 r' * y ; :: thesis: ( (s * y) . i = c * (r' * y) & c in I & r' * y in J )
thus ( (s * y) . i = c * (r' * y) & c in I & r' * y in J ) by A6, A9, Def3; :: thesis: verum

end;

end;

hence x * y in M by A1, A2; :: thesis: verum

end;

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