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

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

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

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

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

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

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

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

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, y be VECTOR of (REAL-NS 1); :: thesis: for a, b being Real st J . x = a & J . y = b holds 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;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

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