theorem Th26: :: NDIFF_5:26

for G being RealNormSpace-Sequence
for F being RealNormSpace
for f1, f2 being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )