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() ) )

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

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

hence ( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) ) by Th16, Th18; :: thesis: verum

end;

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

hence ( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) ) by Th17, Th19; :: thesis: verum

end;

end;