theorem Th4: :: PDIFF_1:4

for J being Function of (REAL 1),REAL st J = proj (1,1) holds
( ( for x being VECTOR of (REAL-NS 1)
for y being Real st J . x = y holds
||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y, a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Real st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st J . x = a & J . y = b holds
J . (x - y) = a - b ) )