let J be Function of (REAL 1),REAL; ( 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)
; ( ( 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 ( ( 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);
for a, b being Real st J . x = a & J . y = b holds
J . (x + y) = a + blet a,
b be
Real;
( 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
;
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;
verum
end;
let x, y be VECTOR of (REAL-NS 1); for a, b being Real st J . x = a & J . y = b holds
J . (x - y) = a - b
let a, b be Real; ( 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
; 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
; verum