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

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