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 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 :: thesis: 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 ; :: 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 A6: ( 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, 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 ) :: 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 r9 ; :: thesis: ( (y * s) . i = (y * c) * r9 & y * c in I & r9 in J )
thus ( (y * s) . i = (y * c) * r9 & y * c in I & r9 in J ) by A8, A11, Def2; :: thesis: verum

end;

end;

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

end;

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