let A be Subset of REAL; :: thesis: for a, x being Real st x in a ** A holds
ex b being Real st
( b in A & x = a * b )
let a, x be Real; :: thesis: ( x in a ** A implies ex b being Real st
( b in A & x = a * b ) )
assume x in a ** A ; :: thesis: ex b being Real st
( b in A & x = a * b )
then x in { (a * b) where b is Element of ExtREAL : b in A } by MEMBER_1:187;
then consider b being Element of ExtREAL such that
A1: ( x = a * b & b in A ) ;
reconsider b = b as Real by A1;
take b ; :: thesis: ( b in A & x = a * b )
x = a * b by A1, XXREAL_3:def 5;
hence ( b in A & x = a * b ) by A1; :: thesis: verum