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 * (upper_bound X)
let X be non empty Subset of REAL ; :: thesis: ( X is bounded_above & 0 <= r implies upper_bound (r ** X) = r * (upper_bound X) )
assume A1: ( X is bounded_above & 0 <= r ) ; :: thesis: upper_bound (r ** X) = r * (upper_bound X)
A2: for a being real number st a in r ** X holds
a <= r * (upper_bound X)

proof

let a be real number ; :: thesis: ( a in r ** X implies a <= r * (upper_bound X) )
assume a in r ** X ; :: thesis: a <= r * (upper_bound X)
then a in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A3: ( a = r * x & x in X ) ;
x <= upper_bound X by A1, A3, SEQ_4:def 4;
hence a <= r * (upper_bound X) by A1, A3, XREAL_1:66; :: thesis: verum

end;

A4: for b being real number st ( for a being real number st a in r ** X holds
a <= b ) holds
r * (upper_bound X) <= b

proof

let b be real number ; :: thesis: ( ( for a being real number st a in r ** X holds
a <= b ) implies r * (upper_bound X) <= b )
assume A5: for a being real number st a in r ** X holds
a <= b ; :: thesis: r * (upper_bound X) <= b
consider x being Real such that
A6: x in X by SUBSET_1:10;
r * x in { (r * y) where y is Real : y in X } by A6;
then A7: r * x in r ** X by Th8;

now

per cases ( r = 0 or r > 0 ) by A1;

suppose r = 0 ; :: thesis: r * (upper_bound X) <= b

hence r * (upper_bound X) <= b by A5, A7; :: thesis: verum

end;

suppose A8: r > 0 ; :: thesis: r * (upper_bound X) <= b

for z being real number st z in X holds
z <= b / r

proof

let z be real number ; :: 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;
then r * z <= b by A5;
hence z <= b / r by A8, XREAL_1:79; :: thesis: verum

end;

then upper_bound X <= b / r by SEQ_4:62;
then r * (upper_bound X) <= (b / r) * r by A8, XREAL_1:66;
hence r * (upper_bound X) <= b by A8, XCMPLX_1:88; :: thesis: verum

end;

end;

end;

hence r * (upper_bound X) <= b ; :: thesis: verum

end;

r ** X is non empty Subset of REAL by Th7;
hence upper_bound (r ** X) = r * (upper_bound X) by A2, A4, SEQ_4:63; :: thesis: verum