let A be non empty Subset of REAL; :: thesis: for x being Real
for y being R_eal st x = y & 0 <= y holds
sup (x ** A) = y * (sup A)
let x be Real; :: thesis: for y being R_eal st x = y & 0 <= y holds
sup (x ** A) = y * (sup A)
let y be R_eal; :: thesis: ( x = y & 0 <= y implies sup (x ** A) = y * (sup A) )
assume that
A1: x = y and
A2: 0 <= y ; :: thesis: sup (x ** A) = y * (sup A)
reconsider Y = x ** A as non empty Subset of REAL ;

per cases ( not A is bounded_above or A is bounded_above ) ;

suppose A3: not A is bounded_above ; :: thesis: sup (x ** A) = y * (sup A)

per cases ( y = 0 or y > 0 ) by A2;

suppose A4: y = 0 ; :: thesis: sup (x ** A) = y * (sup A)

then x ** A = {0} by A1, INTEGRA2:40;
hence sup (x ** A) = 0 by XXREAL_2:11
.= y * (sup A) by A4 ;
:: thesis: verum

end;

suppose A5: y > 0 ; :: thesis: sup (x ** A) = y * (sup A)

then not Y is bounded_above by A1, A3, Lm1;
hence sup (x ** A) = +infty by XXREAL_2:73
.= y * +infty by A5, XXREAL_3:def 5
.= y * (sup A) by A3, XXREAL_2:73 ;
:: thesis: verum

end;

end;

end;

suppose A is bounded_above ; :: thesis: sup (x ** A) = y * (sup A)

then reconsider X = A as non empty real-membered bounded_above set ;
reconsider u = upper_bound X as Real ;
x ** X is bounded_above by A1, A2, INTEGRA2:9;
then reconsider Y = Y as non empty real-membered bounded_above set ;
thus sup (x ** A) = upper_bound Y
.= x * u by A1, A2, INTEGRA2:13
.= y * (sup A) by A1, EXTREAL1:1 ; :: thesis: verum

end;

end;