:: by Agata Darmochwa{\l}

::

:: Received November 21, 1991

:: Copyright (c) 1991 Association of Mizar Users

begin

definition

let n be Nat;

func REAL n -> FinSequence-DOMAIN of REAL equals :: EUCLID:def 1

n -tuples_on REAL;

coherence

n -tuples_on REAL is FinSequence-DOMAIN of REAL ;

end;
func REAL n -> FinSequence-DOMAIN of REAL equals :: EUCLID:def 1

n -tuples_on REAL;

coherence

n -tuples_on REAL is FinSequence-DOMAIN of REAL ;

:: deftheorem defines REAL EUCLID:def 1 :

for n being Nat holds REAL n = n -tuples_on REAL;

registration

let n be Nat;

cluster -> n -element Element of REAL n;

coherence

for b_{1} being Element of REAL n holds b_{1} is n -element
;

end;
cluster -> n -element Element of REAL n;

coherence

for b

definition

func absreal -> Function of REAL,REAL means :Def2: :: EUCLID:def 2

for r being real number holds it . r = abs r;

existence

ex b_{1} being Function of REAL,REAL st

for r being real number holds b_{1} . r = abs r

for b_{1}, b_{2} being Function of REAL,REAL st ( for r being real number holds b_{1} . r = abs r ) & ( for r being real number holds b_{2} . r = abs r ) holds

b_{1} = b_{2}

end;
for r being real number holds it . r = abs r;

existence

ex b

for r being real number holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines absreal EUCLID:def 2 :

for b

( b

definition

let x be real-valued FinSequence;

:: original: |.

redefine func abs x -> FinSequence of REAL equals :: EUCLID:def 3

absreal * x;

coherence

|.x.| is FinSequence of REAL

for b_{1} being FinSequence of REAL holds

( b_{1} = |.x.| iff b_{1} = absreal * x )

end;
:: original: |.

redefine func abs x -> FinSequence of REAL equals :: EUCLID:def 3

absreal * x;

coherence

|.x.| is FinSequence of REAL

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines abs EUCLID:def 3 :

for x being real-valued FinSequence holds abs x = absreal * x;

definition

let n be Nat;

func 0* n -> real-valued FinSequence equals :: EUCLID:def 4

n |-> 0;

coherence

n |-> 0 is real-valued FinSequence ;

end;
func 0* n -> real-valued FinSequence equals :: EUCLID:def 4

n |-> 0;

coherence

n |-> 0 is real-valued FinSequence ;

:: deftheorem defines 0* EUCLID:def 4 :

for n being Nat holds 0* n = n |-> 0;

definition

let n be Nat;

:: original: 0*

redefine func 0* n -> Element of REAL n;

coherence

0* n is Element of REAL n ;

end;
:: original: 0*

redefine func 0* n -> Element of REAL n;

coherence

0* n is Element of REAL n ;

definition

let n be Nat;

let x be Element of REAL n;

:: original: -

redefine func - x -> Element of REAL n;

coherence

- x is Element of REAL n

end;
let x be Element of REAL n;

:: original: -

redefine func - x -> Element of REAL n;

coherence

- x is Element of REAL n

proof end;

definition

let n be Nat;

let x, y be Element of REAL n;

:: original: +

redefine func x + y -> Element of REAL n;

coherence

x + y is Element of REAL n

redefine func x - y -> Element of REAL n;

coherence

x - y is Element of REAL n

end;
let x, y be Element of REAL n;

:: original: +

redefine func x + y -> Element of REAL n;

coherence

x + y is Element of REAL n

proof end;

:: original: -redefine func x - y -> Element of REAL n;

coherence

x - y is Element of REAL n

proof end;

definition

let n be Nat;

let x be Element of REAL n;

let r be real number ;

:: original: (#)

redefine func r * x -> Element of REAL n;

coherence

r (#) x is Element of REAL n

end;
let x be Element of REAL n;

let r be real number ;

:: original: (#)

redefine func r * x -> Element of REAL n;

coherence

r (#) x is Element of REAL n

proof end;

definition

let n be Nat;

let x be Element of REAL n;

:: original: |.

redefine func abs x -> Element of n -tuples_on REAL;

coherence

|.x.| is Element of n -tuples_on REAL by FINSEQ_2:133;

end;
let x be Element of REAL n;

:: original: |.

redefine func abs x -> Element of n -tuples_on REAL;

coherence

|.x.| is Element of n -tuples_on REAL by FINSEQ_2:133;

definition

let n be Nat;

let x be Element of REAL n;

:: original: ^2

redefine func sqr x -> Element of n -tuples_on REAL;

coherence

x ^2 is Element of n -tuples_on REAL by FINSEQ_2:133;

end;
let x be Element of REAL n;

:: original: ^2

redefine func sqr x -> Element of n -tuples_on REAL;

coherence

x ^2 is Element of n -tuples_on REAL by FINSEQ_2:133;

definition

let f be real-valued FinSequence;

func |.f.| -> Real equals :: EUCLID:def 5

sqrt (Sum (sqr f));

coherence

sqrt (Sum (sqr f)) is Real ;

end;
func |.f.| -> Real equals :: EUCLID:def 5

sqrt (Sum (sqr f));

coherence

sqrt (Sum (sqr f)) is Real ;

:: deftheorem defines |. EUCLID:def 5 :

for f being real-valued FinSequence holds |.f.| = sqrt (Sum (sqr f));

theorem :: EUCLID:1

canceled;

theorem :: EUCLID:2

canceled;

theorem :: EUCLID:3

proof end;

theorem :: EUCLID:4

theorem :: EUCLID:5

canceled;

theorem :: EUCLID:6

Lm1: for f being real-valued FinSequence holds f is FinSequence of REAL

proof end;

Lm2: for f being real-valued FinSequence holds f is Element of REAL (len f)

proof end;

theorem :: EUCLID:7

proof end;

theorem Th8: :: EUCLID:8

proof end;

theorem Th9: :: EUCLID:9

for r being real number

for f being real-valued FinSequence holds abs (r * f) = (abs r) * (abs f) by RFUNCT_1:37;

for f being real-valued FinSequence holds abs (r * f) = (abs r) * (abs f) by RFUNCT_1:37;

theorem Th10: :: EUCLID:10

proof end;

Lm3: for f being real-valued FinSequence holds sqr (abs f) = sqr f

proof end;

theorem Th11: :: EUCLID:11

proof end;

theorem Th12: :: EUCLID:12

proof end;

registration

let f be real-valued FinSequence;

cluster |.f.| -> non negative ;

coherence

not |.f.| is negative by Th12;

end;
cluster |.f.| -> non negative ;

coherence

not |.f.| is negative by Th12;

theorem Th13: :: EUCLID:13

proof end;

theorem :: EUCLID:14

proof end;

theorem Th15: :: EUCLID:15

proof end;

theorem Th16: :: EUCLID:16

proof end;

theorem :: EUCLID:17

proof end;

theorem :: EUCLID:18

proof end;

theorem Th19: :: EUCLID:19

proof end;

registration

let n be Nat;

let x1 be Element of REAL n;

cluster |.(x1 - x1).| -> zero ;

coherence

|.(x1 - x1).| is empty by Th19;

end;
let x1 be Element of REAL n;

cluster |.(x1 - x1).| -> zero ;

coherence

|.(x1 - x1).| is empty by Th19;

theorem :: EUCLID:20

proof end;

theorem Th21: :: EUCLID:21

proof end;

theorem Th22: :: EUCLID:22

for n being Nat

for x1, x2, x being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|

for x1, x2, x being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|

proof end;

definition

let n be Nat;

func Pitag_dist n -> Function of [:(REAL n),(REAL n):],REAL means :Def6: :: EUCLID:def 6

for x, y being Element of REAL n holds it . (x,y) = |.(x - y).|;

existence

ex b_{1} being Function of [:(REAL n),(REAL n):],REAL st

for x, y being Element of REAL n holds b_{1} . (x,y) = |.(x - y).|

for b_{1}, b_{2} being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b_{1} . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds b_{2} . (x,y) = |.(x - y).| ) holds

b_{1} = b_{2}

end;
func Pitag_dist n -> Function of [:(REAL n),(REAL n):],REAL means :Def6: :: EUCLID:def 6

for x, y being Element of REAL n holds it . (x,y) = |.(x - y).|;

existence

ex b

for x, y being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Pitag_dist EUCLID:def 6 :

for n being Nat

for b

( b

theorem :: EUCLID:23

proof end;

theorem Th24: :: EUCLID:24

proof end;

definition

let n be Nat;

func Euclid n -> strict MetrSpace equals :: EUCLID:def 7

MetrStruct(# (REAL n),(Pitag_dist n) #);

coherence

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrSpace

end;
func Euclid n -> strict MetrSpace equals :: EUCLID:def 7

MetrStruct(# (REAL n),(Pitag_dist n) #);

coherence

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrSpace

proof end;

:: deftheorem defines Euclid EUCLID:def 7 :

for n being Nat holds Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #);

registration
end;

definition

let n be Nat;

func TOP-REAL n -> strict RLTopStruct means :Def8: :: EUCLID:def 8

( TopStruct(# the carrier of it, the topology of it #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );

existence

ex b_{1} being strict RLTopStruct st

( TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = RealVectSpace (Seg n) )

for b_{1}, b_{2} being strict RLTopStruct st TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b_{2}, the topology of b_{2} #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = RealVectSpace (Seg n) holds

b_{1} = b_{2}
;

end;
func TOP-REAL n -> strict RLTopStruct means :Def8: :: EUCLID:def 8

( TopStruct(# the carrier of it, the topology of it #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );

existence

ex b

( TopStruct(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines TOP-REAL EUCLID:def 8 :

for n being Nat

for b

( b

registration
end;

registration

let n be Nat;

cluster TOP-REAL n -> TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;

coherence

( TOP-REAL n is TopSpace-like & TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )

end;
cluster TOP-REAL n -> TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;

coherence

( TOP-REAL n is TopSpace-like & TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )

proof end;

theorem Th25: :: EUCLID:25

proof end;

theorem Th26: :: EUCLID:26

proof end;

theorem Th27: :: EUCLID:27

proof end;

registration

let n be Nat;

cluster TOP-REAL n -> constituted-FinSeqs strict ;

coherence

TOP-REAL n is constituted-FinSeqs

end;
cluster TOP-REAL n -> constituted-FinSeqs strict ;

coherence

TOP-REAL n is constituted-FinSeqs

proof end;

registration

let n be Nat;

cluster -> FinSequence-like Element of the carrier of (TOP-REAL n);

coherence

for b_{1} being Point of (TOP-REAL n) holds b_{1} is FinSequence-like
;

end;
cluster -> FinSequence-like Element of the carrier of (TOP-REAL n);

coherence

for b

registration

let n be Nat;

cluster -> real-valued Element of the carrier of (TOP-REAL n);

coherence

for b_{1} being Point of (TOP-REAL n) holds b_{1} is real-valued
by Th27;

end;
cluster -> real-valued Element of the carrier of (TOP-REAL n);

coherence

for b

Lm4: for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds

p1 + p2 = r1 + r2

proof end;

Lm5: for n being Nat

for p being Point of (TOP-REAL n)

for x being real number

for r being real-valued Function st p = r holds

x * p = x (#) r

proof end;

registration

let r, s be real number ;

let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

identify r * p with s * f when r = s, p = f;

compatibility

( r = s & p = f implies r * p = s * f ) by Lm5;

end;
let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

identify r * p with s * f when r = s, p = f;

compatibility

( r = s & p = f implies r * p = s * f ) by Lm5;

registration

let n be Nat;

let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

identify p + q with f + g when p = f, q = g;

compatibility

( p = f & q = g implies p + q = f + g ) by Lm4;

end;
let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

identify p + q with f + g when p = f, q = g;

compatibility

( p = f & q = g implies p + q = f + g ) by Lm4;

registration

let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

identify - p with - f when p = f;

compatibility

( p = f implies - p = - f )

end;
let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

identify - p with - f when p = f;

compatibility

( p = f implies - p = - f )

proof end;

registration

let n be Nat;

let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

identify p - q with f - g when p = f, q = g;

compatibility

( p = f & q = g implies p - q = f - g ) ;

end;
let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

identify p - q with f - g when p = f, q = g;

compatibility

( p = f & q = g implies p - q = f - g ) ;

registration

let n be Nat;

cluster -> n -element Element of the carrier of (TOP-REAL n);

coherence

for b_{1} being Point of (TOP-REAL n) holds b_{1} is n -element

end;
cluster -> n -element Element of the carrier of (TOP-REAL n);

coherence

for b

proof end;

definition

let n be Nat;

:: original: 0*

redefine func 0.REAL n -> Point of (TOP-REAL n);

coherence

0* n is Point of (TOP-REAL n)

end;
:: original: 0*

redefine func 0.REAL n -> Point of (TOP-REAL n);

coherence

0* n is Point of (TOP-REAL n)

proof end;

theorem :: EUCLID:28

canceled;

theorem :: EUCLID:29

theorem :: EUCLID:30

for n being Nat

for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) + p3 = p1 + (p2 + p3) by RLVECT_1:def 6;

for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) + p3 = p1 + (p2 + p3) by RLVECT_1:def 6;

theorem :: EUCLID:31

for n being Nat

for p being Point of (TOP-REAL n) holds

( (0. (TOP-REAL n)) + p = p & p + (0. (TOP-REAL n)) = p ) by RLVECT_1:10;

for p being Point of (TOP-REAL n) holds

( (0. (TOP-REAL n)) + p = p & p + (0. (TOP-REAL n)) = p ) by RLVECT_1:10;

theorem :: EUCLID:32

for n being Nat

for x being real number holds x * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:23;

for x being real number holds x * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:23;

theorem :: EUCLID:33

for n being Nat

for p being Point of (TOP-REAL n) holds

( 1 * p = p & 0 * p = 0. (TOP-REAL n) ) by RLVECT_1:23, RLVECT_1:def 11;

for p being Point of (TOP-REAL n) holds

( 1 * p = p & 0 * p = 0. (TOP-REAL n) ) by RLVECT_1:23, RLVECT_1:def 11;

theorem :: EUCLID:34

for n being Nat

for p being Point of (TOP-REAL n)

for x, y being real number holds (x * y) * p = x * (y * p) by RLVECT_1:def 10;

for p being Point of (TOP-REAL n)

for x, y being real number holds (x * y) * p = x * (y * p) by RLVECT_1:def 10;

theorem :: EUCLID:35

for n being Nat

for p being Point of (TOP-REAL n)

for x being real number holds

( not x * p = 0. (TOP-REAL n) or x = 0 or p = 0. (TOP-REAL n) ) by RLVECT_1:24;

for p being Point of (TOP-REAL n)

for x being real number holds

( not x * p = 0. (TOP-REAL n) or x = 0 or p = 0. (TOP-REAL n) ) by RLVECT_1:24;

theorem :: EUCLID:36

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for x being real number holds x * (p1 + p2) = (x * p1) + (x * p2) by RLVECT_1:def 8;

for p1, p2 being Point of (TOP-REAL n)

for x being real number holds x * (p1 + p2) = (x * p1) + (x * p2) by RLVECT_1:def 8;

theorem :: EUCLID:37

for n being Nat

for p being Point of (TOP-REAL n)

for x, y being real number holds (x + y) * p = (x * p) + (y * p) by RLVECT_1:def 9;

for p being Point of (TOP-REAL n)

for x, y being real number holds (x + y) * p = (x * p) + (y * p) by RLVECT_1:def 9;

theorem :: EUCLID:38

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for x being real number holds

( not x * p1 = x * p2 or x = 0 or p1 = p2 ) by RLVECT_1:50;

for p1, p2 being Point of (TOP-REAL n)

for x being real number holds

( not x * p1 = x * p2 or x = 0 or p1 = p2 ) by RLVECT_1:50;

theorem :: EUCLID:39

theorem :: EUCLID:40

theorem :: EUCLID:41

for n being Nat

for p1, p2 being Point of (TOP-REAL n) st p1 + p2 = 0. (TOP-REAL n) holds

p1 = - p2 by RLVECT_1:19;

for p1, p2 being Point of (TOP-REAL n) st p1 + p2 = 0. (TOP-REAL n) holds

p1 = - p2 by RLVECT_1:19;

theorem :: EUCLID:42

for n being Nat

for p1, p2 being Point of (TOP-REAL n) holds - (p1 + p2) = (- p1) - p2 by RLVECT_1:44;

for p1, p2 being Point of (TOP-REAL n) holds - (p1 + p2) = (- p1) - p2 by RLVECT_1:44;

theorem :: EUCLID:43

theorem :: EUCLID:44

for n being Nat

for p being Point of (TOP-REAL n)

for x being real number holds

( - (x * p) = (- x) * p & - (x * p) = x * (- p) ) by RLVECT_1:39, RLVECT_1:98;

for p being Point of (TOP-REAL n)

for x being real number holds

( - (x * p) = (- x) * p & - (x * p) = x * (- p) ) by RLVECT_1:39, RLVECT_1:98;

theorem :: EUCLID:45

theorem :: EUCLID:46

theorem :: EUCLID:47

for n being Nat

for p1, p2 being Point of (TOP-REAL n) st p1 - p2 = 0. (TOP-REAL n) holds

p1 = p2 by RLVECT_1:35;

for p1, p2 being Point of (TOP-REAL n) st p1 - p2 = 0. (TOP-REAL n) holds

p1 = p2 by RLVECT_1:35;

theorem :: EUCLID:48

for n being Nat

for p1, p2 being Point of (TOP-REAL n) holds

( - (p1 - p2) = p2 - p1 & - (p1 - p2) = (- p1) + p2 ) by RLVECT_1:47;

for p1, p2 being Point of (TOP-REAL n) holds

( - (p1 - p2) = p2 - p1 & - (p1 - p2) = (- p1) + p2 ) by RLVECT_1:47;

theorem :: EUCLID:49

for n being Nat

for p1, p2, p3 being Point of (TOP-REAL n) holds p1 + (p2 - p3) = (p1 + p2) - p3 by RLVECT_1:def 6;

for p1, p2, p3 being Point of (TOP-REAL n) holds p1 + (p2 - p3) = (p1 + p2) - p3 by RLVECT_1:def 6;

theorem :: EUCLID:50

for n being Nat

for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 + p3) = (p1 - p2) - p3 by RLVECT_1:41;

for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 + p3) = (p1 - p2) - p3 by RLVECT_1:41;

theorem :: EUCLID:51

for n being Nat

for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 - p3) = (p1 - p2) + p3 by RLVECT_1:43;

for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 - p3) = (p1 - p2) + p3 by RLVECT_1:43;

theorem :: EUCLID:52

for n being Nat

for p, p1 being Point of (TOP-REAL n) holds

( p = (p + p1) - p1 & p = (p - p1) + p1 ) by RLVECT_4:1;

for p, p1 being Point of (TOP-REAL n) holds

( p = (p + p1) - p1 & p = (p - p1) + p1 ) by RLVECT_4:1;

theorem :: EUCLID:53

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for x being real number holds x * (p1 - p2) = (x * p1) - (x * p2) by RLVECT_1:48;

for p1, p2 being Point of (TOP-REAL n)

for x being real number holds x * (p1 - p2) = (x * p1) - (x * p2) by RLVECT_1:48;

theorem :: EUCLID:54

for n being Nat

for p being Point of (TOP-REAL n)

for x, y being real number holds (x - y) * p = (x * p) - (y * p) by RLVECT_1:49;

for p being Point of (TOP-REAL n)

for x, y being real number holds (x - y) * p = (x * p) - (y * p) by RLVECT_1:49;

theorem :: EUCLID:55

proof end;

definition

canceled;

canceled;

canceled;

canceled;

canceled;

let p be Point of (TOP-REAL 2);

func p `1 -> Real equals :: EUCLID:def 14

p . 1;

coherence

p . 1 is Real ;

func p `2 -> Real equals :: EUCLID:def 15

p . 2;

coherence

p . 2 is Real ;

end;
canceled;

canceled;

canceled;

canceled;

let p be Point of (TOP-REAL 2);

func p `1 -> Real equals :: EUCLID:def 14

p . 1;

coherence

p . 1 is Real ;

func p `2 -> Real equals :: EUCLID:def 15

p . 2;

coherence

p . 2 is Real ;

:: deftheorem EUCLID:def 9 :

canceled;

:: deftheorem EUCLID:def 10 :

canceled;

:: deftheorem EUCLID:def 11 :

canceled;

:: deftheorem EUCLID:def 12 :

canceled;

:: deftheorem EUCLID:def 13 :

canceled;

:: deftheorem defines `1 EUCLID:def 14 :

for p being Point of (TOP-REAL 2) holds p `1 = p . 1;

:: deftheorem defines `2 EUCLID:def 15 :

for p being Point of (TOP-REAL 2) holds p `2 = p . 2;

definition

let x, y be real number ;

:: original: |[

redefine func |[x,y]| -> Point of (TOP-REAL 2);

coherence

|[x,y]| is Point of (TOP-REAL 2)

end;
:: original: |[

redefine func |[x,y]| -> Point of (TOP-REAL 2);

coherence

|[x,y]| is Point of (TOP-REAL 2)

proof end;

theorem :: EUCLID:56

theorem Th57: :: EUCLID:57

proof end;

theorem :: EUCLID:58

proof end;

theorem Th59: :: EUCLID:59

proof end;

theorem :: EUCLID:60

proof end;

theorem Th61: :: EUCLID:61

for x being real number

for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1)),(x * (p `2))]|

for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1)),(x * (p `2))]|

proof end;

theorem :: EUCLID:62

proof end;

theorem Th63: :: EUCLID:63

proof end;

theorem :: EUCLID:64

proof end;

theorem Th65: :: EUCLID:65

proof end;

theorem :: EUCLID:66

proof end;

theorem :: EUCLID:67

for n being Nat

for P being Subset of (TOP-REAL n)

for Q being non empty Subset of (Euclid n) st P = Q holds

(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)

for P being Subset of (TOP-REAL n)

for Q being non empty Subset of (Euclid n) st P = Q holds

(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)

proof end;

theorem :: EUCLID:68

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds

p1 + p2 = r1 + r2 ;

for p1, p2 being Point of (TOP-REAL n)

for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds

p1 + p2 = r1 + r2 ;

theorem :: EUCLID:69

for n being Nat

for x being real number

for p being Point of (TOP-REAL n)

for r being real-valued Function st p = r holds

x * p = x (#) r ;

for x being real number

for p being Point of (TOP-REAL n)

for r being real-valued Function st p = r holds

x * p = x (#) r ;

theorem Th70: :: EUCLID:70

proof end;

theorem :: EUCLID:71

proof end;

theorem :: EUCLID:72

for n being Nat

for p1 being Point of (TOP-REAL n)

for r1 being real-valued Function st p1 = r1 holds

- p1 = - r1 ;

for p1 being Point of (TOP-REAL n)

for r1 being real-valued Function st p1 = r1 holds

- p1 = - r1 ;

theorem :: EUCLID:73

for n being Nat

for p1, p2 being Point of (TOP-REAL n)

for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds

p1 - p2 = r1 - r2 ;

for p1, p2 being Point of (TOP-REAL n)

for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds

p1 - p2 = r1 - r2 ;

theorem :: EUCLID:74

theorem :: EUCLID:75

registration

let n be Nat;

let D be set ;

cluster n -tuples_on D -> FinSequence-membered ;

coherence

n -tuples_on D is FinSequence-membered

end;
let D be set ;

cluster n -tuples_on D -> FinSequence-membered ;

coherence

n -tuples_on D is FinSequence-membered

proof end;

registration
end;

registration

let n be Nat;

cluster REAL n -> real-functions-membered ;

coherence

REAL n is real-functions-membered

end;
cluster REAL n -> real-functions-membered ;

coherence

REAL n is real-functions-membered

proof end;