set M = { (a * i) where i is Element of R : i in I } ;
{ (a * i) where i is Element of R : i in I } is Subset of R

proof

per cases ( I is empty or not I is empty ) ;

suppose A1: I is empty ; :: thesis: { (a * i) where i is Element of R : i in I } is Subset of R

{ (a * i) where i is Element of R : i in I } is empty

proof

assume not { (a * i) where i is Element of R : i in I } is empty ; :: thesis: contradiction
then reconsider M = { (a * i) where i is Element of R : i in I } as non empty set ;
set b = the Element of M;
the Element of M in { (a * i) where i is Element of R : i in I } ;
then ex i being Element of R st
( the Element of M = a * i & i in I ) ;
hence contradiction by A1; :: thesis: verum

end;

then for u being set st u in { (a * i) where i is Element of R : i in I } holds
u in the carrier of R ;
hence { (a * i) where i is Element of R : i in I } is Subset of R by TARSKI:def 3; :: thesis: verum

end;

suppose not I is empty ; :: thesis: { (a * i) where i is Element of R : i in I } is Subset of R

then reconsider I = I as non empty set ;
set j9 = the Element of I;
the Element of I in I ;
then reconsider j = the Element of I as Element of R ;
a * j in { (a * i) where i is Element of R : i in I } ;
then reconsider M = { (a * i) where i is Element of R : i in I } as non empty set ;
for x being set st x in M holds
x in the carrier of R

proof

let x be set ; :: thesis: ( x in M implies x in the carrier of R )
assume x in M ; :: thesis: x in the carrier of R
then ex i being Element of R st
( x = a * i & i in I ) ;
hence x in the carrier of R ; :: thesis: verum

end;

hence { (a * i) where i is Element of R : i in I } is Subset of R by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence { (a * i) where i is Element of R : i in I } is Subset of R ; :: thesis: verum