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 Element of REAL st x = I . y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of 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 Element of REAL st x = I . y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of 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 Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of 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 Element of REAL st x = I . y holds
||.x.|| = abs y
let y be Element of REAL ; :: thesis: ( x = I . y implies ||.x.|| = abs y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
assume x = I . y ; :: thesis: ||.x.|| = abs y
then xx = <*y*> by A1, Lm1;
then sqrt (Sum (sqr xx)) = sqrt (Sum <*(y ^2 )*>) by RVSUM_1:81;
then A2: sqrt (Sum (sqr xx)) = sqrt (y ^2 ) by RVSUM_1:103;
||.x.|| = |.xx.| by REAL_NS1:1;
hence ||.x.|| = abs y by A2, COMPLEX1:158; :: thesis: verum

end;

hereby :: thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of 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 Element of REAL st x = I . a & y = I . b holds
x + y = I . (a + b)
let a, b be Element of 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;
assume ( x = I . a & y = I . b ) ; :: thesis: x + y = I . (a + b)
then ( <*a*> = xx & <*b*> = yy ) by A1, Lm1;
then x + y = <*a*> + <*b*> by REAL_NS1:2;
then x + y = <*(a + b)*> by RVSUM_1:29;
hence x + y = I . (a + b) by A1, Lm1; :: thesis: verum

end;

A3: now

let x be VECTOR of (REAL-NS 1); :: thesis: for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y)
let y be Element of REAL ; :: thesis: for a being Real st x = I . y holds
a * x = I . (a * y)
let 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 A4: xx = <*y*> by A1, Lm1;
a * x = a * xx by REAL_NS1:3;
then a * x = <*(a * y)*> by A4, RVSUM_1:69;
hence a * x = I . (a * y) by A1, Lm1; :: thesis: verum

end;

A5: now

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

end;

now

let x, y be VECTOR of (REAL-NS 1); :: thesis: for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b)
let a, b be Element of 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;
assume ( x = I . a & y = I . b ) ; :: thesis: x - y = I . (a - b)
then ( <*a*> = xx & <*b*> = yy ) by A1, Lm1;
then x - y = <*a*> - <*b*> by REAL_NS1:5;
then x - y = <*(a - b)*> by RVSUM_1:50;
hence x - y = I . (a - b) by A1, Lm1; :: thesis: verum

end;

hence ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st x = I . y holds
a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st x = I . a holds
- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st x = I . a & y = I . b holds
x - y = I . (a - b) ) ) by A3, A5; :: thesis: verum