let I be Function of REAL,(REAL 1); :: thesis: ( I = (proj (1,1)) " implies ( ( 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) ) ) )
assume A1: I = (proj (1,1)) " ; :: thesis: ( ( 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) ) )

hereby :: thesis: ( ( 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) ) )

let x be VECTOR of (REAL-NS 1); :: thesis: for y being Real st x = I . y holds
||.x.|| = |.y.|
let y be Real; :: thesis: ( x = I . y implies ||.x.|| = |.y.| )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
reconsider yy = y as Real ;
reconsider yy2 = yy ^2 as Real ;
assume x = I . y ; :: thesis: ||.x.|| = |.y.|
then xx = <*y*> by A1, Lm1;
then sqrt (Sum (sqr xx)) = sqrt (Sum <*yy2*>) by RVSUM_1:55;
then A2: sqrt (Sum (sqr xx)) = sqrt (y ^2) by RVSUM_1:73;
||.x.|| = |.xx.| by REAL_NS1:1;
hence ||.x.|| = |.y.| by A2, COMPLEX1:72; :: thesis: verum

end;

A3: now :: thesis: 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)

let x, y be VECTOR of (REAL-NS 1); :: thesis: for a, b being Real st x = I . a & y = I . b holds
x - y = I . (a - b)
let a, b be Real; :: thesis: ( x = I . a & y = I . b implies x - y = I . (a - b) )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def 4;
reconsider aa = a, bb = b as Real ;
assume that
A4: x = I . a and
A5: y = I . b ; :: thesis: x - y = I . (a - b)
A6: <*b*> = yy by A1, A5, Lm1;
<*a*> = xx by A1, A4, Lm1;
then x - y = <*aa*> - <*bb*> by A6, REAL_NS1:5;
then x - y = <*(a - b)*> by RVSUM_1:29;
hence x - y = I . (a - b) by A1, Lm1; :: thesis: verum

end;

hereby :: thesis: ( ( 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) ) )

let x, y be VECTOR of (REAL-NS 1); :: thesis: for a, b being Real st x = I . a & y = I . b holds
x + y = I . (a + b)
let a, b be Real; :: thesis: ( x = I . a & y = I . b implies x + y = I . (a + b) )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def 4;
reconsider aa = a, bb = b as Real ;
assume that
A7: x = I . a and
A8: y = I . b ; :: thesis: x + y = I . (a + b)
A9: <*b*> = yy by A1, A8, Lm1;
<*a*> = xx by A1, A7, Lm1;
then x + y = <*aa*> + <*bb*> by A9, REAL_NS1:2;
then x + y = <*(a + b)*> by RVSUM_1:13;
hence x + y = I . (a + b) by A1, Lm1; :: thesis: verum

end;

A10: now :: thesis: for x being VECTOR of (REAL-NS 1)
for y, a being Real st x = I . y holds
a * x = I . (a * y)

let x be VECTOR of (REAL-NS 1); :: thesis: for y, a being Real st x = I . y holds
a * x = I . (a * y)
let y, a be Real; :: thesis: ( x = I . y implies a * x = I . (a * y) )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
assume x = I . y ; :: thesis: a * x = I . (a * y)
then A11: xx = <*y*> by A1, Lm1;
a * x = a * xx by REAL_NS1:3;
then a * x = <*(a * y)*> by A11, RVSUM_1:47;
hence a * x = I . (a * y) by A1, Lm1; :: thesis: verum

end;

now :: thesis: for x being VECTOR of (REAL-NS 1)
for a being Real st x = I . a holds
- x = I . (- a)

let x be VECTOR of (REAL-NS 1); :: thesis: for a being Real st x = I . a holds
- x = I . (- a)
let a be Real; :: thesis: ( x = I . a implies - x = I . (- a) )
assume x = I . a ; :: thesis: - x = I . (- a)
then (- 1) * x = I . ((- 1) * a) by A10;
hence - x = I . (- a) by RLVECT_1:16; :: thesis: verum

end;

hence ( ( 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) ) ) by A10, A3; :: thesis: verum