theorem Th27: :: PDIFF_1:27

for m, n being non zero Nat
for i being Nat
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))