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 ex i being Element of R st
( b = 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 ;
consider j9 being Element of I;
j9 in I ;
then reconsider j = j9 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