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 Real st J . x = y holds
||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y, a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Real st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being 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 Real st J . x = y holds
||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being Real st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y, a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Real st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being 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 Real st J . x = a & J . y = b holds
J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)
for y, a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Real st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being 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 Real st J . x = y holds
||.x.|| = |.y.|
let y be Real; :: thesis: ( J . x = y implies ||.x.|| = |.y.| )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
assume J . x = y ; :: thesis: ||.x.|| = |.y.|
then I . (J . xx) = I . y ;
then x = I . y by A1, Lm1, FUNCT_1:34;
hence ||.x.|| = |.y.| by Th3; :: thesis: verum

end;

hereby :: thesis: ( ( for x being VECTOR of (REAL-NS 1)
for y, a being Real st J . x = y holds
J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)
for a being Real st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being 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 Real st J . x = a & J . y = b holds
J . (x + y) = a + b
let a, b be 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;
reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;
assume that
A2: J . x = a and
A3: J . y = b ; :: thesis: J . (x + y) = a + b
I . (J . yy) = I . b by A3;
then A4: y = I . b by A1, Lm1, FUNCT_1:34;
I . (J . xx) = I . a by A2;
then x = I . a by A1, Lm1, FUNCT_1:34;
then J . (x + y) = J . (I . (a + b)) by A4, Th3;
then J . (x + y) = J . (I . (aa + bb)) ;
hence J . (x + y) = a + b by A1, Lm1, FUNCT_1:35; :: thesis: verum

end;

hereby :: thesis: ( ( for x being VECTOR of (REAL-NS 1)
for a being Real st J . x = a holds
J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)
for a, b being 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, a being Real st J . x = y holds
J . (a * x) = a * y
let y, 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;
reconsider yy = y, aa = a as Element of REAL by XREAL_0:def 1;
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:34;
then J . (a * x) = J . (I . (a * y)) by Th3;
then J . (a * x) = aa * yy by A1, Lm1, FUNCT_1:35;
hence J . (a * x) = a * y ; :: thesis: verum

end;

hereby :: thesis: for x, y being VECTOR of (REAL-NS 1)
for a, b being 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 Real st J . x = y holds
J . (- x) = - y
let y be Real; :: thesis: ( J . x = y implies J . (- x) = - y )
reconsider xx = x as Element of REAL 1 by REAL_NS1:def 4;
reconsider yy = y as Element of REAL by XREAL_0:def 1;
assume J . x = y ; :: thesis: J . (- x) = - y
then I . y = I . (J . xx) ;
then x = I . y by A1, Lm1, FUNCT_1:34;
then J . (- x) = J . (I . (- y)) by Th3;
then J . (- x) = - yy by A1, Lm1, FUNCT_1:35;
hence J . (- x) = - y ; :: thesis: verum

end;

let x, y be VECTOR of (REAL-NS 1); :: thesis: for a, b being Real st J . x = a & J . y = b holds
J . (x - y) = a - b
let a, b be 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;
reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;
assume that
A5: J . x = a and
A6: J . y = b ; :: thesis: J . (x - y) = a - b
I . (J . yy) = I . b by A6;
then A7: y = I . b by A1, Lm1, FUNCT_1:34;
I . (J . xx) = I . a by A5;
then x = I . a by A1, Lm1, FUNCT_1:34;
then J . (x - y) = J . (I . (a - b)) by A7, Th3;
then J . (x - y) = aa - bb by A1, Lm1, FUNCT_1:35;
hence J . (x - y) = a - b ; :: thesis: verum