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 x, y being Element of R st x in M & y in M holds
x + y in M

proof

let x, y be Element of R; :: thesis: ( x in M & y in M implies x + y in M )
assume that
A1: x in M and
A2: y in M ; :: thesis: x + y in M
consider s being FinSequence of the carrier of R such that
A3: x = Sum s and
A4: 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 ) by A1;
consider t being FinSequence of the carrier of R such that
A5: y = Sum t and
A6: for i being Element of NAT st 1 <= i & i <= len t holds
ex a, b being Element of R st
( t . i = a * b & a in I & b in J ) by A2;
set q = s ^ t;

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

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len (s ^ t) implies ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J ) )
assume that
A8: 1 <= i and
A9: i <= len (s ^ t) ; :: thesis: ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J )
thus ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J ) :: thesis: verum

proof

per cases ( i <= len s or len s < i ) ;

suppose A10: i <= len s ; :: thesis: ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J )

then i in Seg (len s) by A8, FINSEQ_1:1;
then i in dom s by FINSEQ_1:def 3;
then (s ^ t) . i = s . i by FINSEQ_1:def 7;
hence ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J ) by A4, A8, A10; :: thesis: verum

end;

suppose A11: len s < i ; :: thesis: ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J )

then reconsider j = i - (len s) as Element of NAT by INT_1:5;
(len s) - (len s) < j by A11, XREAL_1:9;
then A12: 1 <= j by NAT_1:14;
i <= (len s) + (len t) by A9, FINSEQ_1:22;
then A13: j <= ((len s) + (len t)) - (len s) by XREAL_1:9;
t . j = (s ^ t) . i by A9, A11, FINSEQ_1:24;
hence ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J ) by A6, A12, A13; :: thesis: verum

end;

end;

end;

end;

Sum (s ^ t) = x + y by A3, A5, RLVECT_1:41;
hence x + y in M by A7; :: thesis: verum

end;

hence I *' J is add-closed ; :: thesis: verum