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

let x, y be Element of R; :: thesis:
assume that
A1: x in M and
A2: y in M ; :: thesis:
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;

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

end;

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:

end;

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

end;