theorem Th5: :: NDIFF12:5

for E, F being RealNormSpace
for s, t being Point of [:E,F:]
for a being Real holds
( s = [(s `1),(s `2)] & (s + t) `1 = (s `1) + (t `1) & (s + t) `2 = (s `2) + (t `2) & (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) & (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )