let A be non empty Subset of REAL ; :: thesis: for x being Real
for y being R_eal st x = y & 0 <= y holds
inf (x ** A) = y * (inf A)
let x be Real; :: thesis: for y being R_eal st x = y & 0 <= y holds
inf (x ** A) = y * (inf A)
let y be R_eal; :: thesis: ( x = y & 0 <= y implies inf (x ** A) = y * (inf A) )
assume that
Z1: x = y and
Z2: 0 <= y ; :: thesis: inf (x ** A) = y * (inf A)
reconsider Y = x ** A as non empty Subset of REAL by INTEGRA2:7;

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

suppose SS: not A is bounded_below ; :: thesis: inf (x ** A) = y * (inf A)

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

suppose S: y = 0 ; :: thesis: inf (x ** A) = y * (inf A)

then x ** A = {0 } by Z1, INTEGRA2:42;
hence inf (x ** A) = 0 by XXREAL_2:13
.= y * (inf A) by S ;
:: thesis: verum

end;

suppose S: y > 0 ; :: thesis: inf (x ** A) = y * (inf A)

not Y is bounded_below by Lx2, S, SS, Z1;
hence inf (x ** A) = -infty by XXREAL_2:78
.= y * -infty by S, XXREAL_3:def 5
.= y * (inf A) by SS, XXREAL_2:78 ;
:: thesis: verum

end;

end;

end;

suppose A is bounded_below ; :: thesis: inf (x ** A) = y * (inf A)

then reconsider X = A as non empty real-membered bounded_below set ;
reconsider u = lower_bound X as Real by XREAL_0:def 1;
x ** X is bounded_below by Z1, Z2, INTEGRA2:11;
then reconsider Y = Y as non empty real-membered bounded_below set ;
thus inf (x ** A) = lower_bound Y
.= x * u by Z1, Z2, INTEGRA2:15
.= y * (inf A) by Z1, EXTREAL1:13 ; :: thesis: verum

end;

end;