theorem Th6: :: PDIFF_6:6

for n, m being Nat
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for a being Real st f = g holds
a (#) f = a (#) g