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

proof

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

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

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

proof

assume not { (a * i) where i is Element of : i in I } is empty ; :: thesis: contradiction
then reconsider M = { (a * i) where i is Element of : i in I } as non empty set ;
consider b being Element of M;
b in { (a * i) where i is Element of : i in I } ;
then ex i being Element of 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 : i in I } holds
u in the carrier of R ;
hence { (a * i) where i is Element of : i in I } is Subset of by TARSKI:def 3; :: thesis: verum

end;

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

then reconsider I = I as non empty set ;
consider j' being Element of I;
j' in I ;
then reconsider j = j' as Element of ;
a * j in { (a * i) where i is Element of : i in I } ;
then reconsider M = { (a * i) where i is Element of : 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 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 : i in I } is Subset of by TARSKI:def 3; :: thesis: verum

end;

end;

end;

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