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 object 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 object st x in M holds
x in the carrier of R
proof
let x be object ; :: 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