theorem Th3: :: NDIFF_3:3
for F being RealNormSpace
for L1, L2 being LinearFunc of F holds
( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F )