let n be Element of NAT ; :: thesis: for X being set
for r being Real
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let X be set ; :: thesis: for r being Real
for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let r be Real; :: thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let f be PartFunc of REAL,(REAL n); :: thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )
assume AS: ( X c= dom f & f | X is continuous ) ; :: thesis: (r (#) f) | X is continuous
reconsider g = f as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;
g | X is continuous PartFunc of REAL, the carrier of (REAL-NS n) by AS, Def2Th;
then P1: (r (#) g) | X is continuous by AS, NFCONT_3:21;
r (#) g = r (#) f by LM003B;
hence (r (#) f) | X is continuous by P1, Def2Th; :: thesis: verum