let X be non empty set ; :: thesis: for r being non zero Real

for f being Function of X,ExtREAL holds

( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )

let r be non zero Real; :: thesis: for f being Function of X,ExtREAL holds

( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )

let f be Function of X,ExtREAL; :: thesis: ( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )

for f being Function of X,ExtREAL holds

( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )

let r be non zero Real; :: thesis: for f being Function of X,ExtREAL holds

( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )

let f be Function of X,ExtREAL; :: thesis: ( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )