theorem Th27: :: NDIFF_5:27

for r being Real
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
r (#) (f * (reproj ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))