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) ) )

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

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) ) )

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;||.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

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)

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;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

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) ) )

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;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

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)

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;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

now :: thesis: for x being VECTOR of (REAL-NS 1)

for a being Real st x = I . a holds

- x = I . (- a)

hence
( ( 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;- 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

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