theorem Th3: :: PDIFF_1:3

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