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 A1: ( x in M & y in M ) ; :: thesis: x + y in M
then consider s being FinSequence of the carrier of R such that
A2: ( 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 ) ) ) ;
consider t being FinSequence of the carrier of R such that
A3: ( y = Sum t & ( 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 A1;
set q = s ^ t;
A4: Sum (s ^ t) = x + y by A2, A3, RLVECT_1:58;

now

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 A5: ( 1 <= i & 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 A6: 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 A5, FINSEQ_1:3;
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 A2, A5, A6; :: thesis: verum

end;

suppose A7: 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:18;
(len s) - (len s) < j by A7, XREAL_1:11;
then A8: 1 <= j by NAT_1:14;
i <= (len s) + (len t) by A5, FINSEQ_1:35;
then A9: j <= ((len s) + (len t)) - (len s) by XREAL_1:11;
t . j = (s ^ t) . i by A5, A7, FINSEQ_1:37;
hence ex a, r being Element of R st
( (s ^ t) . i = a * r & a in I & r in J ) by A3, A8, A9; :: thesis: verum

end;

end;

end;

end;

hence x + y in M by A4; :: thesis: verum

end;

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