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 ) } ;
not { (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 ) } is empty

proof

set p = <*> the carrier of R;
for i being Element of NAT st 1 <= i & i <= len (<*> the carrier of R) holds
ex a, b being Element of R st
( (<*> the carrier of R) . i = a * b & a in I & b in J ) ;
then Sum (<*> the carrier of R) in { (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 ) } ;
hence not { (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 ) } is empty ; :: thesis: verum

end;

hence not I *' J is empty ; :: thesis: verum