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 ;
consider b being Element of M;
b in { (a * i) where i is Element of R : i in I } ;
then consider i being Element of R such that
A2: ( b = a * i & i in I ) ;
thus contradiction by A1, A2; :: 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 ;
consider j' being Element of I;
j' in I ;
then reconsider j = j' 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 consider i being Element of R such that
A3: ( x = a * i & i in I ) ;
thus x in the carrier of R by A3; :: 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