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; :: thesis: ( x in M implies y * x in M )
assume x in M ; :: thesis: y * x 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 = y * s;
A2: Sum (y * s) = y * (Sum s) by BINOM:4;
A3: Seg (len (y * s)) = dom (y * s) by FINSEQ_1:def 3
.= dom s by POLYNOM1:def 2
.= Seg (len s) by FINSEQ_1:def 3 ;
then A4: len (y * s) = len s by FINSEQ_1:8;

now

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

proof

take y * c ; :: thesis: ex r being Element of R st
( (y * s) . i = (y * c) * r & y * c in I & r in J )
take r' ; :: thesis: ( (y * s) . i = (y * c) * r' & y * c in I & r' in J )
thus ( (y * s) . i = (y * c) * r' & y * c in I & r' in J ) by A6, A9, Def2; :: thesis: verum

end;

end;

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

end;

hence I *' J is left-ideal by Def2; :: thesis: verum