let X be non empty set ; :: thesis: for r being Real
for f being V120() V121() Function of X,ExtREAL holds
( r (#) f is V120() & r (#) f is V121() )
let r be Real; :: thesis: for f being V120() V121() Function of X,ExtREAL holds
( r (#) f is V120() & r (#) f is V121() )
let f be V120() V121() Function of X,ExtREAL; :: thesis: ( r (#) f is V120() & r (#) f is V121() )

per cases ( r >= 0 or r < 0 ) ;

suppose r >= 0 ; :: thesis: ( r (#) f is V120() & r (#) f is V121() )

hence ( r (#) f is V120() & r (#) f is V121() ) ; :: thesis: verum

end;

suppose r < 0 ; :: thesis: ( r (#) f is V120() & r (#) f is V121() )

hence ( r (#) f is V120() & r (#) f is V121() ) ; :: thesis: verum

end;

end;