euclid.miz



    begin

    reserve k,j,n for Nat,

r for Real;

    definition

      let n be Nat;

      :: EUCLID:def1

      func REAL n -> FinSequenceSet of REAL equals (n -tuples_on REAL );

      coherence ;

    end

    registration

      let n be Nat;

      cluster ( REAL n) -> non empty;

      coherence ;

    end

    registration

      let n;

      cluster -> n -element for Element of ( REAL n);

      coherence ;

    end

    definition

      :: EUCLID:def2

      func absreal -> Function of REAL , REAL means

      : Def2: for r holds (it . r) = |.r.|;

      existence

      proof

        deffunc F( Real) = ( In ( |.$1.|, REAL ));

        consider f be Function of REAL , REAL such that

         A1: for r be Element of REAL holds (f . r) = F(r) from FUNCT_2:sch 4;

        take f;

        let r;

        r in REAL by XREAL_0:def 1;

        

        hence (f . r) = ( In ( |.r.|, REAL )) by A1

        .= |.r.|;

      end;

      uniqueness

      proof

        let f,g be Function of REAL , REAL such that

         A2: for r holds (f . r) = |.r.| and

         A3: for r holds (g . r) = |.r.|;

        now

          let x be Element of REAL ;

          

          thus (f . x) = |.x.| by A2

          .= (g . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let x be real-valued FinSequence;

      :: original: abs

      redefine

      :: EUCLID:def3

      func abs x -> FinSequence of REAL equals ( absreal * x);

      coherence

      proof

        thus ( rng ( abs x)) c= REAL ;

      end;

      compatibility

      proof

        set g = ( absreal * x);

        ( dom absreal ) = REAL by FUNCT_2:def 1;

        then ( rng x) c= ( dom absreal );

        then

         A1: ( dom ( abs x)) = ( dom x) & ( dom g) = ( dom x) by RELAT_1: 27, VALUED_1:def 11;

        now

          let a be object;

          assume

           A2: a in ( dom ( abs x));

          

          thus (( abs x) . a) = |.(x . a).| by VALUED_1: 18

          .= ( absreal . (x . a)) by Def2

          .= (g . a) by A1, A2, FUNCT_1: 12;

        end;

        hence thesis by A1, FUNCT_1: 2;

      end;

    end

    definition

      let n;

      :: EUCLID:def4

      func 0* n -> real-valued FinSequence equals (n |-> ( In ( 0 , REAL )));

      coherence ;

    end

    definition

      let n;

      :: original: 0*

      redefine

      func 0* n -> Element of ( REAL n) ;

      coherence ;

    end

    reserve x,x1,x2,y for Element of ( REAL n);

    definition

      let n, x;

      :: original: -

      redefine

      func - x -> Element of ( REAL n) ;

      coherence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider R1 = x as Element of (n -tuples_on REAL );

        ( - R1) in (n -tuples_on REAL );

        hence thesis;

      end;

    end

    definition

      let n, x, y;

      :: original: +

      redefine

      func x + y -> Element of ( REAL n) ;

      coherence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider R1 = x, R2 = y as Element of (n -tuples_on REAL );

        (R1 + R2) in (n -tuples_on REAL );

        hence thesis;

      end;

      :: original: -

      redefine

      func x - y -> Element of ( REAL n) ;

      coherence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider R1 = x, R2 = y as Element of (n -tuples_on REAL );

        (R1 - R2) in (n -tuples_on REAL );

        hence thesis;

      end;

    end

    definition

      let n, x;

      let r be Real;

      :: original: *

      redefine

      func r * x -> Element of ( REAL n) ;

      coherence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider R = x as Element of (n -tuples_on REAL );

        (r * R) in (n -tuples_on REAL );

        hence thesis;

      end;

    end

    definition

      let n, x;

      :: original: abs

      redefine

      func abs x -> Element of (n -tuples_on REAL ) ;

      coherence by FINSEQ_2: 113;

    end

    definition

      let n, x;

      :: original: sqr

      redefine

      func sqr x -> Element of (n -tuples_on REAL ) ;

      coherence by FINSEQ_2: 113;

    end

    reserve f for real-valued FinSequence;

    definition

      let f;

      :: EUCLID:def5

      func |.f.| -> Real equals ( sqrt ( Sum ( sqr f)));

      coherence ;

    end

    

     Lm1: f is Element of ( REAL ( len f))

    proof

      ( rng f) c= REAL ;

      then f is FinSequence of REAL by FINSEQ_1:def 4;

      then f is Element of ( REAL * ) by FINSEQ_1:def 11;

      then f in (( len f) -tuples_on REAL );

      hence thesis;

    end;

    ::$Canceled

    theorem :: EUCLID:4

    ( abs ( 0* n)) = (n |-> 0 qua Real)

    proof

      reconsider m = n as Element of NAT by ORDINAL1:def 12;

      

      thus ( abs ( 0* n)) = (m |-> ( absreal . 0 qua Real)) by FINSEQOP: 16

      .= (n |-> |. 0 .|) by Def2

      .= (n |-> 0 ) by ABSVALUE: 2;

    end;

    theorem :: EUCLID:5

    

     Th2: for f be complex-valued Function holds ( abs ( - f)) = ( abs f)

    proof

      let f be complex-valued Function;

      

       A1: ( dom ( abs ( - f))) = ( dom ( - f)) by VALUED_1:def 11;

      

       A2: ( dom ( abs f)) = ( dom f) by VALUED_1:def 11;

      

       A3: ( dom ( - f)) = ( dom f) by VALUED_1: 8;

      now

        let x be object;

        assume x in ( dom ( abs ( - f)));

        

        thus (( abs ( - f)) . x) = |.(( - f) . x).| by VALUED_1: 18

        .= |.( - (f . x)).| by VALUED_1: 8

        .= |.(f . x).| by COMPLEX1: 52

        .= (( abs f) . x) by VALUED_1: 18;

      end;

      hence thesis by A1, A2, A3, FUNCT_1: 2;

    end;

    theorem :: EUCLID:6

    

     Th3: ( abs (r * f)) = ( |.r.| * ( abs f)) by RFUNCT_1: 25;

    theorem :: EUCLID:7

    

     Th4: |.( 0* n).| = 0

    proof

      

      thus |.( 0* n).| = ( sqrt ( Sum (n |-> ( 0 ^2 )))) by RVSUM_1: 56

      .= ( sqrt (n * 0 )) by RVSUM_1: 80

      .= 0 by SQUARE_1: 17;

    end;

    

     Lm2: ( sqr ( abs f)) = ( sqr f)

    proof

      set n = ( len f);

      reconsider x = f as Element of ( REAL n) by Lm1;

      now

        let k;

        assume k in ( Seg n);

        

        thus (( sqr ( abs x)) . k) = ((( abs x) . k) ^2 ) by VALUED_1: 11

        .= ( |.(x . k).| ^2 ) by VALUED_1: 18

        .= ((x . k) ^2 ) by COMPLEX1: 75

        .= (( sqr x) . k) by VALUED_1: 11;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: EUCLID:8

    

     Th5: |.x.| = 0 implies x = ( 0* n)

    proof

      assume

       A1: |.x.| = 0 ;

      now

        let j;

        assume j in ( Seg n);

        reconsider r = (x . j) as Element of REAL by XREAL_0:def 1;

        ( Sum ( sqr x)) = 0 by A1, RVSUM_1: 86, SQUARE_1: 24;

        then ( Sum ( sqr ( abs x))) = 0 by Lm2;

        then (( abs x) . j) = ((n |-> 0 ) . j) by RVSUM_1: 91;

        then |.r.| = ((n |-> 0 ) . j) by VALUED_1: 18;

        then |.r.| = 0 ;

        then r = 0 by ABSVALUE: 2;

        hence (x . j) = ((n |-> 0 qua Real) . j);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: EUCLID:9

    

     Th6: |.f.| >= 0

    proof

       0 <= ( Sum ( sqr f)) by RVSUM_1: 86;

      hence thesis by SQUARE_1:def 2;

    end;

    registration

      let f;

      cluster |.f.| -> non negative;

      coherence by Th6;

    end

    theorem :: EUCLID:10

    

     Th7: |.( - f).| = |.f.|

    proof

      

      thus |.( - f).| = ( sqrt ( Sum ( sqr ( abs ( - f))))) by Lm2

      .= ( sqrt ( Sum ( sqr ( abs f)))) by Th2

      .= |.f.| by Lm2;

    end;

    theorem :: EUCLID:11

     |.(r * f).| = ( |.r.| * |.f.|)

    proof

      set n = ( len f);

      reconsider x = f as Element of ( REAL n) by Lm1;

      

       A1: 0 <= ( |.r.| ^2 ) & 0 <= ( Sum ( sqr ( abs x))) by RVSUM_1: 86, XREAL_1: 63;

      

      thus |.(r * f).| = ( sqrt ( Sum ( sqr ( abs (r * x))))) by Lm2

      .= ( sqrt ( Sum ( sqr ( |.r.| * ( abs x))))) by Th3

      .= ( sqrt ( Sum (( |.r.| ^2 ) * ( sqr ( abs x))))) by RVSUM_1: 58

      .= ( sqrt (( |.r.| ^2 ) * ( Sum ( sqr ( abs x))))) by RVSUM_1: 87

      .= (( sqrt ( |.r.| ^2 )) * ( sqrt ( Sum ( sqr ( abs x))))) by A1, SQUARE_1: 29

      .= ( |.r.| * ( sqrt ( Sum ( sqr ( abs x))))) by COMPLEX1: 46, SQUARE_1: 22

      .= ( |.r.| * |.f.|) by Lm2;

    end;

    theorem :: EUCLID:12

    

     Th9: |.(x1 + x2).| <= ( |.x1.| + |.x2.|)

    proof

      

       A1: 0 <= ( Sum ( sqr (x1 + x2))) by RVSUM_1: 86;

      

       A2: 0 <= ( Sum ( sqr ( abs x1))) by RVSUM_1: 86;

      then

       A3: 0 <= ( sqrt ( Sum ( sqr ( abs x1)))) by SQUARE_1:def 2;

      

       A4: k in ( Seg n) implies (( sqr ( abs (x1 + x2))) . k) <= (( sqr (( abs x1) + ( abs x2))) . k)

      proof

        ( len (x1 + x2)) = n by CARD_1:def 7;

        then

         A5: ( dom (x1 + x2)) = ( Seg n) by FINSEQ_1:def 3;

        assume

         A6: k in ( Seg n);

        reconsider abs1 = (( abs x1) . k), abs2 = (( abs x2) . k) as Real;

        reconsider r12 = ((x1 + x2) . k) as Element of REAL by XREAL_0:def 1;

        reconsider r11 = (x1 . k), r22 = (x2 . k) as Element of REAL by XREAL_0:def 1;

         |.(r11 + r22).| <= ( |.r11.| + |.r22.|) by COMPLEX1: 56;

        then |.r12.| <= ( |.r11.| + |.r22.|) by A6, A5, VALUED_1:def 1;

        then |.r12.| <= ( |.r11.| + abs2) by VALUED_1: 18;

        then

         A7: |.r12.| <= (abs1 + abs2) by VALUED_1: 18;

        reconsider abs912 = (( abs (x1 + x2)) . k) as Real;

        reconsider abs12 = ((( abs x1) + ( abs x2)) . k) as Real;

        set r2 = (( sqr (( abs x1) + ( abs x2))) . k);

         |.r12.| >= 0 by COMPLEX1: 46;

        then

         A8: 0 <= abs912 by VALUED_1: 18;

        ( len (( abs x1) + ( abs x2))) = n by CARD_1:def 7;

        then ( dom (( abs x1) + ( abs x2))) = ( Seg n) by FINSEQ_1:def 3;

        then |.r12.| <= abs12 by A6, A7, VALUED_1:def 1;

        then abs912 <= abs12 by VALUED_1: 18;

        then (abs912 ^2 ) <= (abs12 ^2 ) by A8, SQUARE_1: 15;

        then (abs912 ^2 ) <= r2 by VALUED_1: 11;

        hence thesis by VALUED_1: 11;

      end;

       0 <= (( Sum ( mlt (( abs x1),( abs x2)))) ^2 ) by XREAL_1: 63;

      then

       A9: ( sqrt (( Sum ( mlt (( abs x1),( abs x2)))) ^2 )) <= ( sqrt (( Sum ( sqr ( abs x1))) * ( Sum ( sqr ( abs x2))))) by RVSUM_1: 92, SQUARE_1: 26;

      

       A10: k in ( Seg n) implies 0 <= (( mlt (( abs x1),( abs x2))) . k)

      proof

        assume k in ( Seg n);

        set r = (( mlt (( abs x1),( abs x2))) . k);

        reconsider r1 = (x1 . k), r2 = (x2 . k) as Element of REAL by XREAL_0:def 1;

        (( abs x1) . k) = |.r1.| & (( abs x2) . k) = |.r2.| by VALUED_1: 18;

        then

         A11: r = ( |.r1.| * |.r2.|) by RVSUM_1: 60;

         0 <= |.r1.| & 0 <= |.r2.| by COMPLEX1: 46;

        hence thesis by A11;

      end;

      ( len ( mlt (( abs x1),( abs x2)))) = n by CARD_1:def 7;

      then ( dom ( mlt (( abs x1),( abs x2)))) = ( Seg n) by FINSEQ_1:def 3;

      then ( Sum ( mlt (( abs x1),( abs x2)))) <= ( sqrt (( Sum ( sqr ( abs x1))) * ( Sum ( sqr ( abs x2))))) by A10, A9, RVSUM_1: 84, SQUARE_1: 22;

      then (2 * ( Sum ( mlt (( abs x1),( abs x2))))) <= (2 * ( sqrt (( Sum ( sqr ( abs x1))) * ( Sum ( sqr ( abs x2)))))) by XREAL_1: 64;

      then (( Sum ( sqr ( abs x1))) + (2 * ( Sum ( mlt (( abs x1),( abs x2)))))) <= (( Sum ( sqr ( abs x1))) + (2 * ( sqrt (( Sum ( sqr ( abs x1))) * ( Sum ( sqr ( abs x2))))))) by XREAL_1: 7;

      then

       A12: ((( Sum ( sqr ( abs x1))) + (2 * ( Sum ( mlt (( abs x1),( abs x2)))))) + ( Sum ( sqr ( abs x2)))) <= ((( Sum ( sqr ( abs x1))) + (2 * ( sqrt (( Sum ( sqr ( abs x1))) * ( Sum ( sqr ( abs x2))))))) + ( Sum ( sqr ( abs x2)))) by XREAL_1: 7;

      

       A13: 0 <= ( Sum ( sqr ( abs x2))) by RVSUM_1: 86;

      then

       A14: 0 <= ( sqrt ( Sum ( sqr ( abs x2)))) by SQUARE_1:def 2;

      ( Sum ( sqr (( abs x1) + ( abs x2)))) = ( Sum ((( sqr ( abs x1)) + (2 * ( mlt (( abs x1),( abs x2))))) + ( sqr ( abs x2)))) by RVSUM_1: 68

      .= (( Sum (( sqr ( abs x1)) + (2 * ( mlt (( abs x1),( abs x2)))))) + ( Sum ( sqr ( abs x2)))) by RVSUM_1: 89

      .= ((( Sum ( sqr ( abs x1))) + ( Sum (2 * ( mlt (( abs x1),( abs x2)))))) + ( Sum ( sqr ( abs x2)))) by RVSUM_1: 89

      .= ((( Sum ( sqr ( abs x1))) + (2 * ( Sum ( mlt (( abs x1),( abs x2)))))) + ( Sum ( sqr ( abs x2)))) by RVSUM_1: 87;

      then ( Sum ( sqr ( abs (x1 + x2)))) <= ((( Sum ( sqr ( abs x1))) + (2 * ( Sum ( mlt (( abs x1),( abs x2)))))) + ( Sum ( sqr ( abs x2)))) by A4, RVSUM_1: 82;

      then ( Sum ( sqr (x1 + x2))) <= ((( Sum ( sqr ( abs x1))) + (2 * ( Sum ( mlt (( abs x1),( abs x2)))))) + ( Sum ( sqr ( abs x2)))) by Lm2;

      then ( Sum ( sqr (x1 + x2))) <= ((( Sum ( sqr ( abs x1))) + (2 * ( sqrt (( Sum ( sqr ( abs x1))) * ( Sum ( sqr ( abs x2))))))) + ( Sum ( sqr ( abs x2)))) by A12, XXREAL_0: 2;

      then

       A15: ( Sum ( sqr (x1 + x2))) <= ((( Sum ( sqr ( abs x1))) + (2 * (( sqrt ( Sum ( sqr ( abs x1)))) * ( sqrt ( Sum ( sqr ( abs x2))))))) + ( Sum ( sqr ( abs x2)))) by A2, A13, SQUARE_1: 29;

      

       A16: (( sqrt ( Sum ( sqr ( abs x2)))) ^2 ) = ( Sum ( sqr ( abs x2))) by A13, SQUARE_1:def 2;

      ( Sum ( sqr ( abs x1))) = (( sqrt ( Sum ( sqr ( abs x1)))) ^2 ) by A2, SQUARE_1:def 2;

      then ( sqrt ( Sum ( sqr (x1 + x2)))) <= ( sqrt ((( sqrt ( Sum ( sqr ( abs x1)))) + ( sqrt ( Sum ( sqr ( abs x2))))) ^2 )) by A15, A16, A1, SQUARE_1: 26;

      then ( sqrt ( Sum ( sqr (x1 + x2)))) <= (( sqrt ( Sum ( sqr ( abs x1)))) + ( sqrt ( Sum ( sqr ( abs x2))))) by A3, A14, SQUARE_1: 22;

      then ( sqrt ( Sum ( sqr (x1 + x2)))) <= (( sqrt ( Sum ( sqr ( abs x1)))) + ( sqrt ( Sum ( sqr x2)))) by Lm2;

      hence thesis by Lm2;

    end;

    theorem :: EUCLID:13

    

     Th10: |.(x1 - x2).| <= ( |.x1.| + |.x2.|)

    proof

       |.(x1 - x2).| <= ( |.x1.| + |.( - x2).|) by Th9;

      hence thesis by Th7;

    end;

    theorem :: EUCLID:14

    ( |.x1.| - |.x2.|) <= |.(x1 + x2).|

    proof

      reconsider R1 = x1, R2 = x2 as Element of (n -tuples_on REAL );

      x1 = ((R1 + R2) - R2) by RVSUM_1: 42;

      then |.x1.| <= ( |.(x1 + x2).| + |.x2.|) by Th10;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: EUCLID:15

    ( |.x1.| - |.x2.|) <= |.(x1 - x2).|

    proof

      reconsider R1 = x1, R2 = x2 as Element of (n -tuples_on REAL );

      x1 = ((R1 - R2) + R2) by RVSUM_1: 43;

      then |.x1.| <= ( |.(x1 - x2).| + |.x2.|) by Th9;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: EUCLID:16

    

     Th13: |.(x1 - x2).| = 0 iff x1 = x2

    proof

      reconsider R1 = x1, R2 = x2 as Element of (n -tuples_on REAL );

      thus |.(x1 - x2).| = 0 implies x1 = x2

      proof

        assume |.(x1 - x2).| = 0 ;

        

        then (R1 - R2) = ( 0* n) by Th5

        .= (n |-> 0 );

        hence thesis by RVSUM_1: 38;

      end;

      assume x1 = x2;

      then (R1 - R2) = ( 0* n) by RVSUM_1: 37;

      hence thesis by Th4;

    end;

    registration

      let n, x1;

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

      coherence by Th13;

    end

    theorem :: EUCLID:17

    x1 <> x2 implies |.(x1 - x2).| > 0

    proof

      assume x1 <> x2;

      then 0 <> |.(x1 - x2).| by Th13;

      hence thesis;

    end;

    theorem :: EUCLID:18

    

     Th15: |.(x1 - x2).| = |.(x2 - x1).|

    proof

      reconsider R1 = x1, R2 = x2 as Element of (n -tuples_on REAL );

      

      thus |.(x1 - x2).| = |.( - (R2 - R1)).| by RVSUM_1: 35

      .= |.(x2 - x1).| by Th7;

    end;

    theorem :: EUCLID:19

    

     Th16: |.(x1 - x2).| <= ( |.(x1 - x).| + |.(x - x2).|)

    proof

      reconsider R1 = x1, R2 = x2, R = x as Element of (n -tuples_on REAL );

       |.(x1 - x2).| = |.(((R1 - R) + R) - R2).| by RVSUM_1: 43

      .= |.((x1 - x) + (x - x2)).| by RVSUM_1: 40;

      hence thesis by Th9;

    end;

    definition

      let n be Nat;

      :: EUCLID:def6

      func Pitag_dist n -> Function of [:( REAL n), ( REAL n):], REAL means

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

      existence

      proof

        deffunc F( Element of ( REAL n), Element of ( REAL n)) = ( In ( |.($1 - $2).|, REAL ));

        consider f be Function of [:( REAL n), ( REAL n):], REAL such that

         A1: for x,y be Element of ( REAL n) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take f;

        let x,y be Element of ( REAL n);

        (f . (x,y)) = F(x,y) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of [:( REAL n), ( REAL n):], REAL ;

        assume that

         A2: for x,y be Element of ( REAL n) holds (f . (x,y)) = |.(x - y).| and

         A3: for x,y be Element of ( REAL n) holds (g . (x,y)) = |.(x - y).|;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider f, g as Function of [:( REAL n), ( REAL n):], REAL ;

        now

          let x,y be Element of ( REAL n);

          

          thus (f . (x,y)) = |.(x - y).| by A2

          .= (g . (x,y)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: EUCLID:20

    for x,y be real-valued FinSequence holds ( sqr (x - y)) = ( sqr (y - x))

    proof

      let x,y be real-valued FinSequence;

      

      thus ((x - y) ^2 ) = (((x ^2 ) - (2 (#) (x (#) y))) + (y ^2 )) by RVSUM_1: 69

      .= (( sqr y) + (( - (2 * ( mlt (x,y)))) + ( sqr x)))

      .= ((( sqr y) - (2 * ( mlt (y,x)))) + ( sqr x)) by RFUNCT_1: 8

      .= ( sqr (y - x)) by RVSUM_1: 69;

    end;

    theorem :: EUCLID:21

    

     Th18: for n be Nat holds ( Pitag_dist n) is_metric_of ( REAL n)

    proof

      let n be Nat;

      let x,y,z be Element of ( REAL n);

      

       A1: (( Pitag_dist n) . (y,z)) = |.(y - z).| by Def6;

      (( Pitag_dist n) . (x,y)) = |.(x - y).| by Def6;

      hence (( Pitag_dist n) . (x,y)) = 0 iff x = y by Th13;

      

      thus (( Pitag_dist n) . (x,y)) = |.(x - y).| by Def6

      .= |.(y - x).| by Th15

      .= (( Pitag_dist n) . (y,x)) by Def6;

      (( Pitag_dist n) . (x,y)) = |.(x - y).| & (( Pitag_dist n) . (x,z)) = |.(x - z).| by Def6;

      hence (( Pitag_dist n) . (x,z)) <= ((( Pitag_dist n) . (x,y)) + (( Pitag_dist n) . (y,z))) by A1, Th16;

    end;

    definition

      let n be Nat;

      :: EUCLID:def7

      func Euclid n -> strict MetrSpace equals MetrStruct (# ( REAL n), ( Pitag_dist n) #);

      coherence

      proof

        ( SpaceMetr (( REAL n),( Pitag_dist n))) = MetrStruct (# ( REAL n), ( Pitag_dist n) #) by Th18, PCOMPS_1:def 7;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster ( Euclid n) -> non empty;

      coherence ;

    end

    definition

      let n be Nat;

      :: EUCLID:def8

      func TOP-REAL n -> strict RLTopStruct means

      : Def8: the TopStruct of it = ( TopSpaceMetr ( Euclid n)) & the RLSStruct of it = ( RealVectSpace ( Seg n));

      existence

      proof

        set V = ( RealVectSpace ( Seg n)), T = ( TopSpaceMetr ( Euclid n));

        reconsider t = the topology of T as Subset-Family of the carrier of V by FINSEQ_2: 93;

        take S = RLTopStruct (# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, t #);

        thus the TopStruct of S = ( TopSpaceMetr ( Euclid n)) by FINSEQ_2: 93;

        thus the RLSStruct of S = ( RealVectSpace ( Seg n));

      end;

      uniqueness ;

    end

    registration

      let n be Nat;

      cluster ( TOP-REAL n) -> non empty;

      coherence

      proof

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by Def8;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

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

      coherence

      proof

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by Def8;

        hence ( TOP-REAL n) is TopSpace-like by PRE_TOPC: 28;

         the RLSStruct of ( TOP-REAL n) = ( RealVectSpace ( Seg n)) by Def8;

        hence thesis by RSSPACE: 15;

      end;

    end

    reserve p,p1,p2,p3 for Point of ( TOP-REAL n),

x,x1,x2,y,y1,y2 for Real;

    theorem :: EUCLID:22

    

     Th19: the carrier of ( TOP-REAL n) = ( REAL n)

    proof

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by Def8;

      hence thesis;

    end;

    theorem :: EUCLID:23

    

     Th20: p is Function of ( Seg n), REAL

    proof

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by Def8;

      then p is Element of ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

      hence thesis;

    end;

    theorem :: EUCLID:24

    

     Th21: p is FinSequence of REAL

    proof

      p is Function of ( Seg n), REAL by Th20;

      hence thesis by FINSEQ_2: 25;

    end;

    registration

      let n;

      cluster ( TOP-REAL n) -> constituted-FinSeqs;

      coherence by Th21;

    end

    registration

      let n;

      cluster -> FinSequence-like for Point of ( TOP-REAL n);

      coherence ;

    end

    registration

      let n;

      cluster -> real-valued for Point of ( TOP-REAL n);

      coherence by Th21;

    end

    

     Lm3: for r1,r2 be real-valued Function st p1 = r1 & p2 = r2 holds (p1 + p2) = (r1 + r2)

    proof

      

       A1: ( REAL n) = ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

      let r1,r2 be real-valued Function such that

       A2: p1 = r1 & p2 = r2;

      reconsider s1 = r1, s2 = r2 as Element of ( REAL n) by A2, Th19;

       the RLSStruct of ( TOP-REAL n) = ( RealVectSpace ( Seg n)) by Def8;

      

      hence (p1 + p2) = (( RealFuncAdd ( Seg n)) . (r1,r2)) by A2, ALGSTR_0:def 1

      .= (s1 + s2) by A1, FUNCSDOM:def 1

      .= (r1 + r2);

    end;

    

     Lm4: for r be real-valued Function st p = r holds (x * p) = (x (#) r)

    proof

      reconsider x1 = x as Real;

      let r be real-valued Function such that

       A1: p = r;

      reconsider s = r as Element of ( REAL n) by A1, Th19;

      ( REAL n) = ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

      then

      reconsider f = s as Function of ( Seg n), REAL by FUNCT_2: 66;

       the RLSStruct of ( TOP-REAL n) = ( RealVectSpace ( Seg n)) by Def8;

      

      hence (x * p) = ( multreal [;] (x1,f)) by A1, FUNCSDOM:def 3

      .= ( multreal [;] (x,(( id REAL ) * f))) by PARTFUN1: 7

      .= (x * s) by FUNCOP_1: 34

      .= (x (#) r);

    end;

    registration

      let r,s be Real;

      let n;

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

      let f be real-valued FinSequence;

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

      compatibility by Lm4;

    end

    registration

      let n;

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

      let f,g be real-valued FinSequence;

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

      compatibility by Lm3;

    end

    registration

      let n;

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

      let f be real-valued FinSequence;

      identify - f with - p when p = f;

      compatibility

      proof

        assume

         A1: p = f;

        

        thus ( - p) = (( - 1) * p) by RLVECT_1: 16

        .= ( - f) by A1;

      end;

    end

    registration

      let n;

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

      let f,g be real-valued FinSequence;

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

      compatibility ;

    end

    registration

      let n;

      cluster -> n -element for Point of ( TOP-REAL n);

      coherence

      proof

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

        

         A1: p is Function of ( Seg n), REAL by Th20;

        ( Seg ( len p)) = ( dom p) by FINSEQ_1:def 3

        .= ( Seg n) by A1, FUNCT_2:def 1;

        hence ( len p) = n by FINSEQ_1: 6;

      end;

    end

    notation

      let n;

      synonym 0.REAL n for 0* n;

    end

    definition

      let n;

      :: original: 0.REAL

      redefine

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

      coherence

      proof

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by Def8;

        hence thesis;

      end;

    end

    theorem :: EUCLID:25

    for x be Element of ( REAL n) holds ( sqr ( abs x)) = ( sqr x) by Lm2;

    ::$Canceled

    reserve p,p1,p2 for Point of ( TOP-REAL 2);

    theorem :: EUCLID:51

    ex x,y be Element of REAL st p = <*x, y*>

    proof

       the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by Def8;

      then p is Tuple of 2, REAL by FINSEQ_2: 131;

      hence thesis by FINSEQ_2: 100;

    end;

    definition

      let p;

      :: EUCLID:def9

      func p `1 -> Real equals (p . 1);

      coherence ;

      :: EUCLID:def10

      func p `2 -> Real equals (p . 2);

      coherence ;

    end

    notation

      let x,y be Real;

      synonym |[x,y]| for <*x,y*>;

    end

    definition

      let x,y be Real;

      :: original: |[

      redefine

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

      coherence

      proof

        

         A1: y in REAL by XREAL_0:def 1;

         the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) & x in REAL by Def8, XREAL_0:def 1;

        hence thesis by A1, FINSEQ_2: 101;

      end;

    end

    theorem :: EUCLID:52

    ( |[x, y]| `1 ) = x & ( |[x, y]| `2 ) = y by FINSEQ_1: 44;

    theorem :: EUCLID:53

    

     Th25: p = |[(p `1 ), (p `2 )]|

    proof

       the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by Def8;

      then p is Tuple of 2, REAL by FINSEQ_2: 131;

      then

      consider x,y be Element of REAL such that

       A1: p = <*x, y*> by FINSEQ_2: 100;

      (p `1 ) = x by A1, FINSEQ_1: 44;

      hence thesis by A1, FINSEQ_1: 44;

    end;

    theorem :: EUCLID:54

    ( 0. ( TOP-REAL 2)) = |[ 0 , 0 ]|

    proof

       the RLSStruct of ( TOP-REAL 2) = ( RealVectSpace ( Seg 2)) & ( 0.REAL 2) = |[ 0 , 0 ]| by Def8, FINSEQ_2: 61;

      hence thesis;

    end;

    theorem :: EUCLID:55

    

     Th27: (p1 + p2) = |[((p1 `1 ) + (p2 `1 )), ((p1 `2 ) + (p2 `2 ))]|

    proof

       the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by Def8;

      then

      reconsider p19 = p1, p29 = p2 as Element of ( REAL 2);

      ( len (p19 + p29)) = 2 by CARD_1:def 7;

      then

       A1: ( dom (p19 + p29)) = ( Seg 2) by FINSEQ_1:def 3;

      2 in {1, 2} by TARSKI:def 2;

      then

       A2: ((p1 + p2) `2 ) = ((p1 `2 ) + (p2 `2 )) by A1, FINSEQ_1: 2, VALUED_1:def 1;

      1 in {1, 2} by TARSKI:def 2;

      then ((p1 + p2) `1 ) = ((p1 `1 ) + (p2 `1 )) by A1, FINSEQ_1: 2, VALUED_1:def 1;

      hence thesis by A2, Th25;

    end;

    theorem :: EUCLID:56

    ( |[x1, y1]| + |[x2, y2]|) = |[(x1 + x2), (y1 + y2)]|

    proof

      

       A1: ( |[x2, y2]| `1 ) = x2 & ( |[x2, y2]| `2 ) = y2 by FINSEQ_1: 44;

      ( |[x1, y1]| `1 ) = x1 & ( |[x1, y1]| `2 ) = y1 by FINSEQ_1: 44;

      hence thesis by A1, Th27;

    end;

    theorem :: EUCLID:57

    

     Th29: (x * p) = |[(x * (p `1 )), (x * (p `2 ))]|

    proof

      ((x * p) `1 ) = (x * (p `1 )) & ((x * p) `2 ) = (x * (p `2 )) by RVSUM_1: 44;

      hence thesis by Th25;

    end;

    theorem :: EUCLID:58

    (x * |[x1, y1]|) = |[(x * x1), (x * y1)]|

    proof

      ( |[x1, y1]| `1 ) = x1 & ( |[x1, y1]| `2 ) = y1 by FINSEQ_1: 44;

      hence thesis by Th29;

    end;

    theorem :: EUCLID:59

    

     Th31: ( - p) = |[( - (p `1 )), ( - (p `2 ))]|

    proof

      

      thus ( - p) = (( - 1) * p)

      .= |[(( - 1) * (p `1 )), (( - 1) * (p `2 ))]| by Th29

      .= |[( - (p `1 )), ( - (p `2 ))]|;

    end;

    theorem :: EUCLID:60

    ( - |[x1, y1]|) = |[( - x1), ( - y1)]|

    proof

      ( |[x1, y1]| `1 ) = x1 & ( |[x1, y1]| `2 ) = y1 by FINSEQ_1: 44;

      hence thesis by Th31;

    end;

    theorem :: EUCLID:61

    

     Th33: (p1 - p2) = |[((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 ))]|

    proof

      ( - p2) = |[( - (p2 `1 )), ( - (p2 `2 ))]| by Th31;

      then (( - p2) `1 ) = ( - (p2 `1 )) & (( - p2) `2 ) = ( - (p2 `2 )) by FINSEQ_1: 44;

      

      hence (p1 - p2) = |[((p1 `1 ) + ( - (p2 `1 ))), ((p1 `2 ) + ( - (p2 `2 )))]| by Th27

      .= |[((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 ))]|;

    end;

    theorem :: EUCLID:62

    ( |[x1, y1]| - |[x2, y2]|) = |[(x1 - x2), (y1 - y2)]|

    proof

      

       A1: ( |[x2, y2]| `1 ) = x2 & ( |[x2, y2]| `2 ) = y2 by FINSEQ_1: 44;

      ( |[x1, y1]| `1 ) = x1 & ( |[x1, y1]| `2 ) = y1 by FINSEQ_1: 44;

      hence thesis by A1, Th33;

    end;

    theorem :: EUCLID:63

    for P be Subset of ( TOP-REAL n), Q be non empty Subset of ( Euclid n) holds P = Q implies (( TOP-REAL n) | P) = ( TopSpaceMetr (( Euclid n) | Q))

    proof

      let P be Subset of ( TOP-REAL n), Q be non empty Subset of ( Euclid n);

      set M = ( TopSpaceMetr (( Euclid n) | Q));

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by Def8;

      then M is SubSpace of the TopStruct of ( TOP-REAL n) by TOPMETR: 13;

      then

      reconsider M = ( TopSpaceMetr (( Euclid n) | Q)) as SubSpace of ( TOP-REAL n) by PRE_TOPC: 29;

      assume P = Q;

      then ( [#] M) = P by TOPMETR:def 2;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: EUCLID:64

    for p1,p2 be Point of ( TOP-REAL n) holds for r1,r2 be real-valued Function st p1 = r1 & p2 = r2 holds (p1 + p2) = (r1 + r2);

    theorem :: EUCLID:65

    for p be Point of ( TOP-REAL n) holds for r be real-valued Function st p = r holds (x * p) = (x (#) r);

    theorem :: EUCLID:66

    

     Th38: ( 0.REAL n) = ( 0. ( TOP-REAL n))

    proof

       the RLSStruct of ( TOP-REAL n) = ( RealVectSpace ( Seg n)) by Def8;

      hence thesis;

    end;

    theorem :: EUCLID:67

    

     Th39: the carrier of ( Euclid n) = the carrier of ( TOP-REAL n)

    proof

      

      thus the carrier of ( Euclid n) = the carrier of ( TopSpaceMetr ( Euclid n))

      .= the carrier of the TopStruct of ( TOP-REAL n) by Def8

      .= the carrier of ( TOP-REAL n);

    end;

    theorem :: EUCLID:68

    for p1 be Point of ( TOP-REAL n) holds for r1 be real-valued Function st p1 = r1 holds ( - p1) = ( - r1);

    theorem :: EUCLID:69

    for p1,p2 be Point of ( TOP-REAL n) holds for r1,r2 be real-valued Function st p1 = r1 & p2 = r2 holds (p1 - p2) = (r1 - r2);

    theorem :: EUCLID:70

    ( 0. ( TOP-REAL n)) = ( 0* n) by Th38;

    theorem :: EUCLID:71

    for p be Point of ( TOP-REAL n) holds |.( - p).| = |.p.| by Th7;

    registration

      let n;

      let D be set;

      cluster (n -tuples_on D) -> FinSequence-membered;

      coherence ;

    end

    registration

      let n;

      cluster ( REAL n) -> FinSequence-membered;

      coherence ;

    end

    registration

      let n;

      cluster ( REAL n) -> real-functions-membered;

      coherence

      proof

        let x be object;

        assume x in ( REAL n);

        then

        reconsider x as Element of ( REAL n);

        x is real-valued;

        hence thesis;

      end;

    end

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    definition

      let n be Nat;

      :: EUCLID:def11

      func 1* n -> FinSequence of REAL equals (n |-> 1);

      coherence

      proof

        (n |-> jj) is FinSequence of REAL ;

        hence thesis;

      end;

    end

    definition

      let n be Nat;

      :: original: 1*

      redefine

      func 1* n -> Element of ( REAL n) ;

      coherence

      proof

        (n |-> jj) is Element of ( REAL n);

        hence thesis;

      end;

    end

    definition

      let n be Nat;

      :: EUCLID:def12

      func 1.REAL n -> Point of ( TOP-REAL n) equals ( 1* n);

      coherence by Th19;

    end

    theorem :: EUCLID:72

    ( abs ( 1* n)) = (n |-> 1)

    proof

      

      thus ( abs ( 1* n)) = ( abs (n |-> jj))

      .= (n |-> ( absreal . 1)) by FINSEQOP: 16

      .= (n |-> |.1.|) by Def2

      .= (n |-> 1) by ABSVALUE:def 1;

    end;

    theorem :: EUCLID:73

    

     Th45: |.( 1* n).| = ( sqrt n)

    proof

      reconsider j = (1 ^2 ) as Element of REAL by XREAL_0:def 1;

      reconsider f = (n |-> j) as FinSequence of REAL ;

      

      thus |.( 1* n).| = ( sqrt ( Sum f)) by RVSUM_1: 56

      .= ( sqrt (n * 1)) by RVSUM_1: 80

      .= ( sqrt n);

    end;

    theorem :: EUCLID:74

     |.( 1.REAL n).| = ( sqrt n) by Th45;

    theorem :: EUCLID:75

    1 <= n implies 1 <= |.( 1.REAL n).|

    proof

      assume

       A1: 1 <= n;

       |.( 1.REAL n).| = ( sqrt n) by Th45;

      hence thesis by A1, SQUARE_1: 18, SQUARE_1: 26;

    end;

    theorem :: EUCLID:76

    for f be FinSequence of REAL holds f is Element of ( REAL ( len f)) & f is Point of ( TOP-REAL ( len f))

    proof

      let f be FinSequence of REAL ;

      f is Element of ( REAL * ) by FINSEQ_1:def 11;

      then the carrier of ( TOP-REAL ( len f)) = the carrier of ( Euclid ( len f)) & f in (( len f) -tuples_on REAL ) by Th39;

      hence thesis;

    end;

    theorem :: EUCLID:77

    ( REAL 0 ) = {( 0. ( TOP-REAL 0 ))}

    proof

      

      thus ( REAL 0 ) = {( <*> REAL )} by FINSEQ_2: 94

      .= {( 0. ( TOP-REAL 0 ))};

    end;