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
A1: x = y and
A2: 0 <= y ; :: thesis: inf (x ** A) = y * (inf A)
reconsider Y = x ** A as non empty Subset of REAL ;

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

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

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

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

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

end;

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

then not Y is bounded_below by A1, A3, Lm2;
hence inf (x ** A) = -infty by XXREAL_2:74
.= y * -infty by A5, XXREAL_3:def 5
.= y * (inf A) by A3, XXREAL_2:74 ;
:: 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 ;
x ** X is bounded_below by A1, A2, INTEGRA2:11;
then reconsider Y = Y as non empty real-membered bounded_below set ;
thus inf (x ** A) = lower_bound Y
.= x * u by A1, A2, INTEGRA2:15
.= y * (inf A) by A1, EXTREAL1:1 ; :: thesis: verum

end;

end;