let J be Function of (REAL 1),REAL ; :: thesis: ( J = proj 1,1 implies ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st J . x = y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) ) )
assume A1: J = proj 1,1 ; :: thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL st J . x = y holds
||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )

hereby :: thesis: ( ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )

let x be VECTOR of (REAL-NS 1); :: thesis: for y being Element of REAL st J . x = y holds
||.x.|| = abs y
let y be Element of REAL ; :: thesis: ( J . x = y implies ||.x.|| = abs y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
assume J . x = y ; :: thesis: ||.x.|| = abs y
then I . (J . xx) = I . y ;
then x = I . y by A1, Lm1, FUNCT_1:56;
hence ||.x.|| = abs y by Th3; :: thesis: verum

end;

hereby :: thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )

let x, y be VECTOR of (REAL-NS 1); :: thesis: for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x + y) = a + b
let a, b be Element of REAL ; :: thesis: ( J . x = a & J . y = b implies J . (x + y) = a + b )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def 4;
assume ( J . x = a & J . y = b ) ; :: thesis: J . (x + y) = a + b
then ( I . (J . xx) = I . a & I . (J . yy) = I . b ) ;
then ( x = I . a & y = I . b ) by A1, Lm1, FUNCT_1:56;
then J . (x + y) = J . (I . (a + b)) by Th3;
hence J . (x + y) = a + b by A1, Lm1, FUNCT_1:57; :: thesis: verum

end;

hereby :: thesis: ( ( for x being VECTOR of (REAL-NS 1)
for a being Element of REAL st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b ) )

let x be VECTOR of (REAL-NS 1); :: thesis: for y being Element of REAL
for a being Real st J . x = y holds
J . (a * x) = a * y
let y be Element of REAL ; :: thesis: for a being Real st J . x = y holds
J . (a * x) = a * y
let a be Real; :: thesis: ( J . x = y implies J . (a * x) = a * y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
assume J . x = y ; :: thesis: J . (a * x) = a * y
then I . (J . xx) = I . y ;
then x = I . y by A1, Lm1, FUNCT_1:56;
then J . (a * x) = J . (I . (a * y)) by Th3;
hence J . (a * x) = a * y by A1, Lm1, FUNCT_1:57; :: thesis: verum

end;

hereby :: thesis: for x, y being VECTOR of (REAL-NS 1)
for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b

let x be VECTOR of (REAL-NS 1); :: thesis: for y being Element of REAL st J . x = y holds
J . (- x) = - y
let y be Element of REAL ; :: thesis: ( J . x = y implies J . (- x) = - y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
assume J . x = y ; :: thesis: J . (- x) = - y
then I . y = I . (J . xx) ;
then x = I . y by A1, Lm1, FUNCT_1:56;
then J . (- x) = J . (I . (- y)) by Th3;
hence J . (- x) = - y by A1, Lm1, FUNCT_1:57; :: thesis: verum

end;

let x, y be VECTOR of (REAL-NS 1); :: thesis: for a, b being Element of REAL st J . x = a & J . y = b holds
J . (x - y) = a - b
let a, b be Element of REAL ; :: thesis: ( J . x = a & J . y = b implies J . (x - y) = a - b )
reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def 4;
assume ( J . x = a & J . y = b ) ; :: thesis: J . (x - y) = a - b
then ( I . (J . xx) = I . a & I . (J . yy) = I . b ) ;
then ( x = I . a & y = I . b ) by A1, Lm1, FUNCT_1:56;
then J . (x - y) = J . (I . (a - b)) by Th3;
hence J . (x - y) = a - b by A1, Lm1, FUNCT_1:57; :: thesis: verum