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;