let r be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
upper_bound (r ** X) = r * ()

let X be non empty Subset of REAL; :: thesis: ( X is bounded_above & 0 <= r implies upper_bound (r ** X) = r * () )
assume that
A1: X is bounded_above and
A2: 0 <= r ; :: thesis: upper_bound (r ** X) = r * ()
A3: for a being Real st a in r ** X holds
a <= r * ()
proof
let a be Real; :: thesis: ( a in r ** X implies a <= r * () )
assume a in r ** X ; :: thesis: a <= r * ()
then a in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A4: a = r * x and
A5: x in X ;
x <= upper_bound X by ;
hence a <= r * () by ; :: thesis: verum
end;
for b being Real st ( for a being Real st a in r ** X holds
a <= b ) holds
r * () <= b
proof
consider x being Element of REAL such that
A6: x in X by SUBSET_1:4;
let b be Real; :: thesis: ( ( for a being Real st a in r ** X holds
a <= b ) implies r * () <= b )

assume A7: for a being Real st a in r ** X holds
a <= b ; :: thesis: r * () <= b
reconsider x = x as Real ;
r * x in { (r * y) where y is Real : y in X } by A6;
then A8: r * x in r ** X by Th8;
now :: thesis: r * () <= b
per cases ( r = 0 or r > 0 ) by A2;
suppose r = 0 ; :: thesis: r * () <= b
hence r * () <= b by A7, A8; :: thesis: verum
end;
suppose A9: r > 0 ; :: thesis: r * () <= b
for z being Real st z in X holds
z <= b / r
proof
let z be Real; :: thesis: ( z in X implies z <= b / r )
assume z in X ; :: thesis: z <= b / r
then r * z in { (r * y) where y is Real : y in X } ;
then r * z in r ** X by Th8;
hence z <= b / r by ; :: thesis: verum
end;
then upper_bound X <= b / r by SEQ_4:45;
then r * () <= (b / r) * r by ;
hence r * () <= b by ; :: thesis: verum
end;
end;
end;
hence r * () <= b ; :: thesis: verum
end;
hence upper_bound (r ** X) = r * () by ; :: thesis: verum