let m be non zero Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL
for r being Real st Z c= dom f & f is_continuous_on Z holds
r (#) f is_continuous_on Z
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL
for r being Real st Z c= dom f & f is_continuous_on Z holds
r (#) f is_continuous_on Z
let f be PartFunc of (REAL m),REAL; :: thesis: for r being Real st Z c= dom f & f is_continuous_on Z holds
r (#) f is_continuous_on Z
let r be Real; :: thesis: ( Z c= dom f & f is_continuous_on Z implies r (#) f is_continuous_on Z )
assume ( Z c= dom f & f is_continuous_on Z ) ; :: thesis: r (#) f is_continuous_on Z
then <>* f is_continuous_on Z by Th44;
then A1: r (#) (<>* f) is_continuous_on Z by Th34;
r (#) (<>* f) = <>* (r (#) f) by Th8;
hence r (#) f is_continuous_on Z by A1, Th44; :: thesis: verum