real_ns1.miz



    begin

    reserve n for Nat;

    

     Lm1: for n be Nat holds ex ADD be BinOp of ( REAL n) st (for a,b be Element of ( REAL n) holds (ADD . (a,b)) = (a + b)) & ADD is commutative associative

    proof

      let n be Nat;

      deffunc P( Element of ( REAL n), Element of ( REAL n)) = ($1 + $2);

      consider ADD be BinOp of ( REAL n) such that

       A1: for a,b be Element of ( REAL n) holds (ADD . (a,b)) = P(a,b) from BINOP_1:sch 4;

      now

        let a,b,c be Element of ( REAL n);

        reconsider a1 = a, b1 = b, c1 = c as Element of (n -tuples_on REAL ) by EUCLID:def 1;

        

        thus (ADD . (a,(ADD . (b,c)))) = (a + (ADD . (b,c))) by A1

        .= (a + (b + c)) by A1

        .= ((a1 + b1) + c1) by RVSUM_1: 15

        .= ((ADD . (a,b)) + c) by A1

        .= (ADD . ((ADD . (a,b)),c)) by A1;

      end;

      then

       A2: ADD is associative;

      now

        let a,b be Element of ( REAL n);

        

        thus (ADD . (a,b)) = (a + b) by A1

        .= (ADD . (b,a)) by A1;

      end;

      then ADD is commutative;

      hence thesis by A1, A2;

    end;

    definition

      let n be Nat;

      :: REAL_NS1:def1

      func Euclid_add n -> BinOp of ( REAL n) means

      : Def1: for a,b be Element of ( REAL n) holds (it . (a,b)) = (a + b);

      existence

      proof

        consider ADD be BinOp of ( REAL n) such that

         A1: for a,b be Element of ( REAL n) holds (ADD . (a,b)) = (a + b) and ADD is commutative associative by Lm1;

        take ADD;

        thus thesis by A1;

      end;

      uniqueness

      proof

        deffunc O( Element of ( REAL n), Element of ( REAL n)) = ($1 + $2);

        for o1,o2 be BinOp of ( REAL n) st (for a,b be Element of ( REAL n) holds (o1 . (a,b)) = O(a,b)) & (for a,b be Element of ( REAL n) holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster ( Euclid_add n) -> commutative associative;

      coherence

      proof

        ex ADD be BinOp of ( REAL n) st (for a,b be Element of ( REAL n) holds (ADD . (a,b)) = (a + b)) & ADD is commutative associative by Lm1;

        hence thesis by Def1;

      end;

    end

    definition

      let n be Nat;

      :: REAL_NS1:def2

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

      : Def2: for r be Real, x be Element of ( REAL n) holds (it . (r,x)) = (r * x);

      existence

      proof

        deffunc F( Real, Element of ( REAL n)) = ($1 * $2);

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

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

        take f;

        let r be Real, x be Element of ( REAL n);

        reconsider r as Element of REAL by XREAL_0:def 1;

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

        hence thesis;

      end;

      uniqueness

      proof

        let mult1,mult2 be Function of [: REAL , ( REAL n):], ( REAL n) such that

         A2: for r be Real, x be Element of ( REAL n) holds (mult1 . (r,x)) = (r * x) and

         A3: for r be Real, x be Element of ( REAL n) holds (mult2 . (r,x)) = (r * x);

        for r be Element of REAL , x be Element of ( REAL n) holds (mult1 . (r,x)) = (mult2 . (r,x))

        proof

          let r be Element of REAL ;

          let x be Element of ( REAL n);

          

          thus (mult1 . (r,x)) = (r * x) by A2

          .= (mult2 . (r,x)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let n be Nat;

      :: REAL_NS1:def3

      func Euclid_norm n -> Function of ( REAL n), REAL means

      : Def3: for x be Element of ( REAL n) holds (it . x) = |.x.|;

      existence

      proof

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

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

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

        take f;

        let x be Element of ( REAL n);

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

        hence thesis;

      end;

      uniqueness

      proof

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

        assume that

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

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

        now

          let x be Element of ( REAL n);

          

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

          .= (g . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let n be Nat;

      :: REAL_NS1:def4

      func REAL-NS n -> strict non empty NORMSTR means

      : Def4: the carrier of it = ( REAL n) & ( 0. it ) = ( 0* n) & the addF of it = ( Euclid_add n) & the Mult of it = ( Euclid_mult n) & the normF of it = ( Euclid_norm n);

      existence

      proof

        take NORMSTR (# ( REAL n), ( 0* n), ( Euclid_add n), ( Euclid_mult n), ( Euclid_norm n) #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let n be non zero Nat;

      cluster ( REAL-NS n) -> non trivial;

      coherence

      proof

        the carrier of ( REAL-NS n) = ( REAL n) by Def4

        .= the carrier of ( TOP-REAL n) by EUCLID: 22;

        hence thesis;

      end;

    end

    theorem :: REAL_NS1:1

    

     Th1: for x be VECTOR of ( REAL-NS n), y be Element of ( REAL n) st x = y holds ||.x.|| = |.y.|

    proof

      let x be VECTOR of ( REAL-NS n);

      let y be Element of ( REAL n);

      assume

       A1: x = y;

      

      thus ||.x.|| = (the normF of ( REAL-NS n) . x)

      .= (( Euclid_norm n) . y) by A1, Def4

      .= |.y.| by Def3;

    end;

    theorem :: REAL_NS1:2

    

     Th2: for n be Nat holds for x,y be VECTOR of ( REAL-NS n), a,b be Element of ( REAL n) st x = a & y = b holds (x + y) = (a + b)

    proof

      let n be Nat;

      let x,y be VECTOR of ( REAL-NS n);

      let a,b be Element of ( REAL n);

      assume x = a & y = b;

      

      hence (x + y) = (( Euclid_add n) . (a,b)) by Def4

      .= (a + b) by Def1;

    end;

    theorem :: REAL_NS1:3

    

     Th3: for x be VECTOR of ( REAL-NS n), y be Element of ( REAL n), a be Real st x = y holds (a * x) = (a * y)

    proof

      let x be Point of ( REAL-NS n), y be Element of ( REAL n), a be Real;

      assume

       A1: x = y;

      reconsider a as Real;

      (a * x) = (( Euclid_mult n) . (a,x)) by Def4

      .= (a * y) by A1, Def2;

      hence thesis;

    end;

    registration

      let n be Nat;

      cluster ( REAL-NS n) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        reconsider x1 = ( 0. ( REAL-NS n)) as Element of ( REAL n) by Def4;

         |.x1.| = 0 iff x1 = ( 0* n) by EUCLID: 7, EUCLID: 8;

        hence ||.( 0. ( REAL-NS n)).|| = 0 by Def4, Th1;

        for x,y be Point of ( REAL-NS n), a be Real holds ( ||.x.|| = 0 iff x = ( 0. ( REAL-NS n))) & ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||)

        proof

          let x,y be Point of ( REAL-NS n);

          let a be Real;

          thus ||.x.|| = 0 iff x = ( 0. ( REAL-NS n))

          proof

            reconsider x1 = x as Element of ( REAL n) by Def4;

             |.x1.| = 0 iff x1 = ( 0* n) by EUCLID: 7, EUCLID: 8;

            hence thesis by Def4, Th1;

          end;

          thus ||.(a * x).|| = ( |.a.| * ||.x.||)

          proof

            reconsider x1 = x as Element of ( REAL n) by Def4;

            

            thus ||.(a * x).|| = |.(a * x1).| by Th1, Th3

            .= ( |.a.| * |.x1.|) by EUCLID: 11

            .= ( |.a.| * ||.x.||) by Th1;

          end;

          thus ||.(x + y).|| <= ( ||.x.|| + ||.y.||)

          proof

            reconsider x1 = x, y1 = y as Element of ( REAL n) by Def4;

             |.(x1 + y1).| <= ( |.x1.| + |.y1.|) by EUCLID: 12;

            then

             A1: |.(x1 + y1).| <= ( ||.x.|| + |.y1.|) by Th1;

             ||.(x + y).|| = |.(x1 + y1).| by Th1, Th2;

            hence thesis by A1, Th1;

          end;

        end;

        hence ( REAL-NS n) is discerning RealNormSpace-like by NORMSP_1:def 1;

        

         A2: for a,b be Real, v be VECTOR of ( REAL-NS n) holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let v be VECTOR of ( REAL-NS n);

          ((a + b) * v) = ((a * v) + (b * v))

          proof

            reconsider v1 = v as Element of ( REAL n) by Def4;

            reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

            

             A3: (a * v) = (a * v1) & (b * v) = (b * v1) by Th3;

            

            thus ((a + b) * v) = (( Euclid_mult n) . ((a + b),v)) by Def4

            .= ((a + b) * v2) by Def2

            .= ((a * v2) + (b * v2)) by RVSUM_1: 50

            .= ((a * v) + (b * v)) by A3, Th2;

          end;

          hence thesis;

        end;

        

         A4: for a be Real, v,w be VECTOR of ( REAL-NS n) holds (a * (v + w)) = ((a * v) + (a * w))

        proof

          let a be Real;

          reconsider a as Real;

          let v,w be VECTOR of ( REAL-NS n);

          (a * (v + w)) = ((a * v) + (a * w))

          proof

            reconsider v1 = v, w1 = w as Element of ( REAL n) by Def4;

            reconsider v2 = v1, w2 = w1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

            

             A5: (a * v) = (a * v1) & (a * w) = (a * w1) by Th3;

            

            thus (a * (v + w)) = (( Euclid_mult n) . (a,(v + w))) by Def4

            .= (( Euclid_mult n) . (a,(v1 + w1))) by Th2

            .= (a * (v2 + w2)) by Def2

            .= ((a * v2) + (a * w2)) by RVSUM_1: 51

            .= ((a * v) + (a * w)) by A5, Th2;

          end;

          hence thesis;

        end;

        

         A6: for a,b be Real, v be VECTOR of ( REAL-NS n) holds ((a * b) * v) = (a * (b * v))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let v be VECTOR of ( REAL-NS n);

          ((a * b) * v) = (a * (b * v))

          proof

            reconsider v1 = v as Element of ( REAL n) by Def4;

            reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

            

             A7: (b * v) = (b * v1) by Th3;

            ((a * b) * v) = (( Euclid_mult n) . ((a * b),v)) by Def4

            .= ((a * b) * v1) by Def2

            .= (a * (b * v2)) by RVSUM_1: 49;

            hence thesis by A7, Th3;

          end;

          hence thesis;

        end;

        for v be VECTOR of ( REAL-NS n) holds (1 * v) = v

        proof

          let v be VECTOR of ( REAL-NS n);

          thus (1 * v) = v

          proof

            reconsider v1 = v as Element of ( REAL n) by Def4;

            reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

            

            thus (1 * v) = (( Euclid_mult n) . (1,v)) by Def4

            .= (1 * v2) by Def2

            .= v by RVSUM_1: 52;

          end;

        end;

        hence ( REAL-NS n) is vector-distributive scalar-distributive scalar-associative scalar-unital by A4, A2, A6;

        for v,w be VECTOR of ( REAL-NS n) holds (v + w) = (w + v)

        proof

          let v,w be VECTOR of ( REAL-NS n);

          thus (v + w) = (w + v)

          proof

            reconsider v1 = v, w1 = w as Element of ( REAL n) by Def4;

            

            thus (v + w) = (( Euclid_add n) . (v,w)) by Def4

            .= (( Euclid_add n) . (w1,v1)) by BINOP_1:def 2

            .= (w + v) by Def4;

          end;

        end;

        hence ( REAL-NS n) is Abelian;

        for u,v,w be VECTOR of ( REAL-NS n) holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be VECTOR of ( REAL-NS n);

          thus ((u + v) + w) = (u + (v + w))

          proof

            reconsider u1 = u, v1 = v, w1 = w as Element of ( REAL n) by Def4;

            

             A8: (v + w) = (v1 + w1) by Th2;

            

            thus ((u + v) + w) = (( Euclid_add n) . ((the addF of ( REAL-NS n) . (u,v)),w)) by Def4

            .= (( Euclid_add n) . ((( Euclid_add n) . (u1,v1)),w1)) by Def4

            .= (( Euclid_add n) . (u1,(( Euclid_add n) . (v1,w1)))) by BINOP_1:def 3

            .= (( Euclid_add n) . (u1,(v1 + w1))) by Def1

            .= (u1 + (v1 + w1)) by Def1

            .= (u + (v + w)) by A8, Th2;

          end;

        end;

        hence ( REAL-NS n) is add-associative;

        for v be VECTOR of ( REAL-NS n) holds (v + ( 0. ( REAL-NS n))) = v

        proof

          let v be VECTOR of ( REAL-NS n);

          reconsider v1 = v as Element of ( REAL n) by Def4;

          reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          reconsider zz = (n |-> ( In ( 0 , REAL ))) as Element of (n -tuples_on REAL );

          ( 0. ( REAL-NS n)) = ( 0* n) by Def4;

          

          hence (v + ( 0. ( REAL-NS n))) = (v1 + ( 0* n)) by Th2

          .= (v2 + zz) by EUCLID:def 4

          .= v by RVSUM_1: 16;

        end;

        hence ( REAL-NS n) is right_zeroed;

        ( REAL-NS n) is right_complementable

        proof

          let v be VECTOR of ( REAL-NS n);

          thus ex w be VECTOR of ( REAL-NS n) st (v + w) = ( 0. ( REAL-NS n))

          proof

            reconsider v1 = v as Element of ( REAL n) by Def4;

            reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

            

             A9: ( 0. ( REAL-NS n)) = ( 0* n) by Def4

            .= (n |-> 0 ) by EUCLID:def 4;

            reconsider w = ( - v1) as VECTOR of ( REAL-NS n) by Def4;

            take w;

            

            thus (v + w) = (v2 + ( - v2)) by Th2

            .= ( 0. ( REAL-NS n)) by A9, RVSUM_1: 22;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: REAL_NS1:4

    

     Th4: for x be VECTOR of ( REAL-NS n), a be Element of ( REAL n) st x = a holds ( - x) = ( - a)

    proof

      let x be VECTOR of ( REAL-NS n);

      let a be Element of ( REAL n);

      assume

       A1: x = a;

      reconsider a1 = a as Element of (n -tuples_on REAL ) by EUCLID:def 1;

      ( - x) = (( - 1) * x) by RLVECT_1: 16

      .= ( - a1) by A1, Th3;

      hence thesis;

    end;

    theorem :: REAL_NS1:5

    

     Th5: for x,y be VECTOR of ( REAL-NS n), a,b be Element of ( REAL n) st x = a & y = b holds (x - y) = (a - b)

    proof

      let x,y be VECTOR of ( REAL-NS n);

      let a,b be Element of ( REAL n);

      assume that

       A1: x = a and

       A2: y = b;

      ( - y) = ( - b) by A2, Th4;

      hence thesis by A1, Th2;

    end;

    theorem :: REAL_NS1:6

    

     Th6: for f be FinSequence of REAL st ( dom f) = ( Seg n) holds f is Element of ( REAL n)

    proof

      

       A1: n in NAT by ORDINAL1:def 12;

      let f be FinSequence of REAL ;

      assume ( dom f) = ( Seg n);

      then ( len f) = n by A1, FINSEQ_1:def 3;

      then f is Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      hence thesis by EUCLID:def 1;

    end;

    theorem :: REAL_NS1:7

    

     Th7: for n be Nat, x be Element of ( REAL n) st (for i be Nat st i in ( Seg n) holds 0 <= (x . i)) holds 0 <= ( Sum x) & for i be Nat st i in ( Seg n) holds (x . i) <= ( Sum x)

    proof

      defpred P[ Nat] means for x be Element of ( REAL $1) st (for i be Nat st i in ( Seg $1) holds 0 <= (x . i)) holds 0 <= ( Sum x) & (for i be Nat st i in ( Seg $1) holds (x . i) <= ( Sum x));

       A1:

      now

        let k be Nat such that

         A2: P[k];

        now

          let x be Element of ( REAL (k + 1));

          assume

           A3: for i be Nat st i in ( Seg (k + 1)) holds 0 <= (x . i);

          thus 0 <= ( Sum x) & for i be Nat st i in ( Seg (k + 1)) holds (x . i) <= ( Sum x)

          proof

            set xk = (x | k);

            

             A4: 0 <= (x . (k + 1)) by A3, FINSEQ_1: 4;

            

             A5: (k + 1) = ( len x) by CARD_1:def 7;

            then ( len (x | k)) = k by FINSEQ_1: 59, NAT_1: 11;

            then

             A6: xk is Element of (k -tuples_on REAL ) by FINSEQ_2: 92;

            1 <= (k + 1) by NAT_1: 11;

            then (k + 1) in ( Seg ( len x)) by A5, FINSEQ_1: 1;

            then

             A7: (k + 1) in ( dom x) by FINSEQ_1:def 3;

            reconsider xk as Element of ( REAL k) by A6, EUCLID:def 1;

            

             A8: xk = (x | ( Seg k)) by FINSEQ_1:def 15;

            x = (x | (k + 1)) by A5, FINSEQ_1: 58

            .= (x | ( Seg (k + 1))) by FINSEQ_1:def 15

            .= (xk ^ <*(x . (k + 1))*>) by A7, A8, FINSEQ_5: 10;

            then

             A9: ( Sum x) = (( Sum xk) + (x . (k + 1))) by RVSUM_1: 74;

             A10:

            now

              let i be Nat;

              assume

               A11: i in ( Seg k);

              k <= (k + 1) by NAT_1: 11;

              then ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

              then 0 <= (x . i) by A3, A11;

              then 0 <= ((x | ( Seg k)) . i) by A11, FUNCT_1: 49;

              hence 0 <= (xk . i) by FINSEQ_1:def 15;

            end;

            

             A12: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

             A13:

            now

              let i be Nat;

              assume

               A14: i in ( Seg (k + 1));

              then

               A15: 1 <= i by FINSEQ_1: 1;

              

               A16: i <= (k + 1) by A14, FINSEQ_1: 1;

              per cases by A16, XXREAL_0: 1;

                suppose i < (k + 1);

                then i <= k by NAT_1: 13;

                then

                 A17: i in ( Seg k) by A15, FINSEQ_1: 1;

                then (xk . i) <= ( Sum xk) by A2, A10;

                then

                 A18: (x . i) <= ( Sum xk) by A8, A17, FUNCT_1: 49;

                ( Sum xk) <= (( Sum xk) + (x . (k + 1))) by A3, A12, XREAL_1: 31;

                hence (x . i) <= ( Sum x) by A9, A18, XXREAL_0: 2;

              end;

                suppose i = (k + 1);

                hence (x . i) <= ( Sum x) by A2, A10, A9, XREAL_1: 31;

              end;

            end;

             0 <= ( Sum xk) by A2, A10;

            hence thesis by A4, A9, A13;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A19: P[ 0 ] by RVSUM_1: 72;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A19, A1);

    end;

    theorem :: REAL_NS1:8

    

     Th8: for x be Element of ( REAL n), i be Nat st i in ( Seg n) holds |.(x . i).| <= |.x.|

    proof

      let x be Element of ( REAL n);

      let i be Nat;

      reconsider sx = ( sqr x) as Element of ( REAL n) by EUCLID:def 1;

       A1:

      now

        let k be Nat;

        assume k in ( Seg n);

        (sx . k) = ((x . k) ^2 ) by VALUED_1: 11;

        hence 0 <= (sx . k) by XREAL_1: 63;

      end;

      

       A2: 0 <= ( |.(x . i).| * |.(x . i).|) by XREAL_1: 63;

      ( |.(x . i).| * |.(x . i).|) = ((x . i) ^2 )

      proof

        per cases by ABSVALUE: 1;

          suppose |.(x . i).| = (x . i);

          hence thesis;

        end;

          suppose |.(x . i).| = ( - (x . i));

          hence thesis;

        end;

      end;

      then

       A3: (( sqr x) . i) = ( |.(x . i).| * |.(x . i).|) by VALUED_1: 11;

      assume i in ( Seg n);

      then ( |.(x . i).| * |.(x . i).|) <= ( Sum ( sqr x)) by A3, A1, Th7;

      then

       A4: ( sqrt ( |.(x . i).| * |.(x . i).|)) <= ( sqrt ( Sum ( sqr x))) by A2, SQUARE_1: 26;

      ( sqrt ( |.(x . i).| ^2 )) = |.(x . i).| by COMPLEX1: 46, SQUARE_1: 22;

      hence thesis by A4, EUCLID:def 5;

    end;

    theorem :: REAL_NS1:9

    

     Th9: for x be Point of ( REAL-NS n), y be Element of ( REAL n) st x = y holds for i be Nat st i in ( Seg n) holds |.(y . i).| <= ||.x.||

    proof

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

      assume x = y;

      then ||.x.|| = |.y.| by Th1;

      hence thesis by Th8;

    end;

    theorem :: REAL_NS1:10

    

     Th10: for x be Element of ( REAL (n + 1)) holds ( |.x.| ^2 ) = (( |.(x | n).| ^2 ) + ((x . (n + 1)) ^2 ))

    proof

      let x be Element of ( REAL (n + 1));

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

      reconsider x as Element of ((n + 1) -tuples_on REAL ) by EUCLID:def 1;

      

       A1: (x | n) = (x | ( Seg n)) by FINSEQ_1:def 15;

      

       A2: (n + 1) = ( len x) by CARD_1:def 7;

      then (n + 1) in ( Seg ( len x)) by FINSEQ_1: 4;

      then

       A3: (n + 1) in ( dom x) by FINSEQ_1:def 3;

      ( len (x | n)) = n by A2, FINSEQ_1: 59, NAT_1: 11;

      then

      reconsider xn = (x | n) as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      ( sqr x) is Element of ( REAL (n + 1)) & for k be Nat st k in ( Seg (n + 1)) holds 0 <= (( sqr x) . k)

      proof

        thus ( sqr x) is Element of ( REAL (n + 1)) by EUCLID:def 1;

        let k be Nat;

        assume k in ( Seg (n + 1));

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

        .= ((x . k) * (x . k));

        hence thesis by XREAL_1: 63;

      end;

      then |.x.| = ( sqrt ( Sum ( sqr x))) & 0 <= ( Sum ( sqr x)) by Th7, EUCLID:def 5;

      then

       A4: ( |.x.| ^2 ) = ( Sum ( sqr x)) by SQUARE_1:def 2;

      ( sqr (x | n)) is Element of ( REAL n) & for k be Nat st k in ( Seg n) holds 0 <= (( sqr (x | n)) . k)

      proof

        ( sqr xn) is Element of ( REAL n) by EUCLID:def 1;

        hence ( sqr (x | n)) is Element of ( REAL n);

        let k be Nat;

        assume k in ( Seg n);

        (( sqr xn) . k) = ((xn . k) ^2 ) by VALUED_1: 11

        .= ((xn . k) * (xn . k));

        hence thesis by XREAL_1: 63;

      end;

      then |.(x | n).| = ( sqrt ( Sum ( sqr (x | n)))) & 0 <= ( Sum ( sqr (x | n))) by Th7, EUCLID:def 5;

      then

       A5: (( |.(x | n).| ^2 ) + ((x . (n + 1)) ^2 )) = (( Sum ( sqr (x | n))) + ((x . (n + 1)) ^2 )) by SQUARE_1:def 2;

      

       A6: x = (x | (n + 1)) by A2, FINSEQ_1: 58

      .= (x | ( Seg (n + 1))) by FINSEQ_1:def 15

      .= ((x | n) ^ <*(x . (n + 1))*>) by A3, A1, FINSEQ_5: 10;

      (( sqr (x | n)) ^ <*((x . (n + 1)) ^2 )*>) = (( mlt (xn,xn)) ^ <*((x . (n + 1)) * (x . (n + 1)))*>)

      .= ( mlt ((xn ^ <*(x . (n + 1))*>),((x | n) ^ <*(x . (n + 1))*>))) by RFUNCT_4: 2

      .= ( sqr x) by A6;

      hence thesis by A4, A5, RVSUM_1: 74;

    end;

    definition

      let n be Nat;

      let f be sequence of ( REAL n), k be Nat;

      :: original: .

      redefine

      func f . k -> Element of ( REAL n) ;

      coherence

      proof

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

        (f . k) in ( REAL n);

        hence thesis;

      end;

    end

    theorem :: REAL_NS1:11

    

     Th11: for n be Nat holds for x be Point of ( REAL-NS n), xs be Element of ( REAL n), seq be sequence of ( REAL-NS n), xseq be sequence of ( REAL n) st xs = x & xseq = seq holds (seq is convergent & ( lim seq) = x iff for i be Nat st i in ( Seg n) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi))

    proof

      defpred P[ Nat] means for x be Point of ( REAL-NS $1), xs be Element of ( REAL $1), seq be sequence of ( REAL-NS $1), xseq be sequence of ( REAL $1) st xs = x & xseq = seq holds ((seq is convergent & ( lim seq) = x) iff (for i be Nat st i in ( Seg $1) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi)));

       A1:

      now

        let n be Nat;

        assume

         A2: P[n];

        now

          let x be Point of ( REAL-NS (n + 1)), xs be Element of ( REAL (n + 1)), seq be sequence of ( REAL-NS (n + 1)), xseq be sequence of ( REAL (n + 1));

          assume

           A3: xs = x & xseq = seq;

           A4:

          now

            assume

             A5: for i be Nat st i in ( Seg (n + 1)) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi);

            thus seq is convergent & ( lim seq) = x

            proof

              ( len xs) = (n + 1) by CARD_1:def 7;

              then ( len (xs | n)) = n by FINSEQ_1: 59, NAT_1: 11;

              then ( dom (xs | n)) = ( Seg n) by FINSEQ_1:def 3;

              then

              reconsider xsn = (xs | n) as Element of ( REAL n) by Th6;

              reconsider xn = xsn as Point of ( REAL-NS n) by Def4;

              defpred P1[ Nat, Element of ( REAL n)] means $2 = ((xseq . $1) | n);

              set seq2 = ( ||.(seq - x).|| (#) ||.(seq - x).||);

              consider rseqn1 be Real_Sequence such that

               A6: for k be Nat holds (rseqn1 . k) = ((xseq . k) . (n + 1)) & rseqn1 is convergent & (xs . (n + 1)) = ( lim rseqn1) by A5, FINSEQ_1: 4;

              

               A7: for i be Element of NAT holds ex y be Element of ( REAL n) st P1[i, y]

              proof

                let i be Element of NAT ;

                take y = ((xseq . i) | n);

                ( len (xseq . i)) = (n + 1) by CARD_1:def 7;

                then ( len ((xseq . i) | n)) = n by FINSEQ_1: 59, NAT_1: 11;

                then ( dom ((xseq . i) | n)) = ( Seg n) by FINSEQ_1:def 3;

                hence thesis by Th6;

              end;

              consider xseqn be sequence of ( REAL n) such that

               A8: for i be Element of NAT holds P1[i, (xseqn . i)] from FUNCT_2:sch 3( A7);

              reconsider seqn = xseqn as sequence of ( REAL-NS n) by Def4;

              set seqn2 = ( ||.(seqn - xn).|| (#) ||.(seqn - xn).||);

              deffunc F( Nat) = |.((rseqn1 . $1) - (xs . (n + 1))).|;

              consider absrseq be Real_Sequence such that

               A9: for i be Nat holds (absrseq . i) = F(i) from SEQ_1:sch 1;

              

               A10: for i be Nat st i in ( Seg n) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseqn . k) . i) & rseqi is convergent & (xsn . i) = ( lim rseqi)

              proof

                let i be Nat such that

                 A11: i in ( Seg n);

                n <= (n + 1) by NAT_1: 11;

                then ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

                then

                consider rseqi be Real_Sequence such that

                 A12: for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi) by A5, A11;

                 A13:

                now

                  let k be Nat;

                  

                   A14: k in NAT by ORDINAL1:def 12;

                  

                  thus (rseqi . k) = ((xseq . k) . i) by A12

                  .= (((xseq . k) | ( Seg n)) . i) by A11, FUNCT_1: 49

                  .= (((xseq . k) | n) . i) by FINSEQ_1:def 15

                  .= ((xseqn . k) . i) by A8, A14;

                end;

                (xsn . i) = ((xs | ( Seg n)) . i) by FINSEQ_1:def 15

                .= (xs . i) by A11, FUNCT_1: 49;

                hence thesis by A12, A13;

              end;

              then

               A15: xn = ( lim seqn) by A2;

              set rseqn2 = (absrseq (#) absrseq);

              xsn = xn;

              then

               A16: seqn is convergent by A2, A10;

              then

               A17: ||.(seqn - xn).|| is convergent by A15, NORMSP_1: 24;

              then

               A18: seqn2 is convergent by SEQ_2: 14;

              now

                reconsider rxs = xs as Element of ((n + 1) -tuples_on REAL ) by EUCLID:def 1;

                let k be Nat;

                

                 A19: k in NAT by ORDINAL1:def 12;

                

                 A20: ( ||.(seq - x).|| . k) = ||.((seq - x) . k).|| by NORMSP_0:def 4

                .= ||.((seq . k) - x).|| by NORMSP_1:def 4;

                reconsider rxseqk = (xseq . k) as Element of ((n + 1) -tuples_on REAL ) by EUCLID:def 1;

                

                 A21: ( ||.(seqn - xn).|| . k) = ||.((seqn - xn) . k).|| by NORMSP_0:def 4

                .= ||.((seqn . k) - xn).|| by NORMSP_1:def 4;

                ( len ((xseqn . k) - xsn)) = n by CARD_1:def 7;

                then

                 A22: ( dom ((xseqn . k) - xsn)) = ( Seg n) by FINSEQ_1:def 3;

                

                 A23: (((xseq . k) - xs) . (n + 1)) = ((rxseqk . (n + 1)) - (rxs . (n + 1))) by RVSUM_1: 27

                .= ((rseqn1 . k) - (xs . (n + 1))) by A6;

                ( len ((xseq . k) - xs)) = (n + 1) by CARD_1:def 7;

                then

                 A24: ( len (((xseq . k) - xs) | n)) = n by FINSEQ_1: 59, NAT_1: 11;

                 A25:

                now

                  reconsider xseq2 = (xseqn . k), xs2 = xsn as Element of (n -tuples_on REAL ) by EUCLID:def 1;

                  reconsider xseq1 = (xseq . k), xs1 = xs as Element of ((n + 1) -tuples_on REAL ) by EUCLID:def 1;

                  let i be Nat;

                  assume i in ( dom (((xseq . k) - xs) | n));

                  then

                   A26: i in ( Seg n) by A24, FINSEQ_1:def 3;

                  

                   A27: (((xseqn . k) - xsn) . i) = ((xseq2 . i) - (xs2 . i)) by RVSUM_1: 27;

                  

                   A28: (((xseq . k) - xs) . i) = ((xseq1 . i) - (xs1 . i)) by RVSUM_1: 27;

                  

                  thus ((((xseq . k) - xs) | n) . i) = ((((xseq . k) - xs) | ( Seg n)) . i) by FINSEQ_1:def 15

                  .= (((xseq . k) - xs) . i) by A26, FUNCT_1: 49

                  .= ((((xseq . k) | ( Seg n)) . i) - (xs . i)) by A26, A28, FUNCT_1: 49

                  .= ((((xseq . k) | ( Seg n)) . i) - ((xs | ( Seg n)) . i)) by A26, FUNCT_1: 49

                  .= ((((xseq . k) | n) . i) - ((xs | ( Seg n)) . i)) by FINSEQ_1:def 15

                  .= ((((xseq . k) | n) . i) - ((xs | n) . i)) by FINSEQ_1:def 15

                  .= (((xseqn . k) - xsn) . i) by A8, A27, A19;

                end;

                ( dom (((xseq . k) - xs) | n)) = ( Seg n) by A24, FINSEQ_1:def 3;

                then

                 A29: (((xseq . k) - xs) | n) = ((xseqn . k) - xsn) by A22, A25, FINSEQ_1: 13;

                

                 A30: 0 <= (((rseqn1 . k) - (xs . (n + 1))) ^2 ) by XREAL_1: 63;

                

                 A31: (absrseq . k) = |.((rseqn1 . k) - (xs . (n + 1))).| by A9;

                 ||.((seq . k) - x).|| = |.((xseq . k) - xs).| by A3, Th1, Th5;

                

                hence (seq2 . k) = ( |.((xseq . k) - xs).| ^2 ) by A20, SEQ_1: 8

                .= (( |.((xseqn . k) - xsn).| ^2 ) + (((rseqn1 . k) - (xs . (n + 1))) ^2 )) by A23, A29, Th10

                .= (( ||.((seqn . k) - xn).|| ^2 ) + (((rseqn1 . k) - (xs . (n + 1))) ^2 )) by Th1, Th5

                .= ((( ||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (((rseqn1 . k) - (xs . (n + 1))) ^2 )) by A21, SEQ_1: 8

                .= ((seqn2 . k) + |.(((rseqn1 . k) - (xs . (n + 1))) * ((rseqn1 . k) - (xs . (n + 1)))).|) by A30, ABSVALUE:def 1

                .= ((seqn2 . k) + ( |.((rseqn1 . k) - (xs . (n + 1))).| * |.((rseqn1 . k) - (xs . (n + 1))).|)) by COMPLEX1: 65

                .= ((seqn2 . k) + (rseqn2 . k)) by A31, SEQ_1: 8;

              end;

              then

               A32: seq2 = (seqn2 + rseqn2) by SEQ_1: 7;

               A33:

              now

                let e be Real;

                assume e > 0 ;

                then

                consider m be Nat such that

                 A34: for k be Nat st m <= k holds |.((rseqn1 . k) - (xs . (n + 1))).| < e by A6, SEQ_2:def 7;

                now

                  let k be Nat;

                  assume m <= k;

                  then |.( |.((rseqn1 . k) - (xs . (n + 1))).| - 0 ).| < e by A34;

                  hence |.((absrseq . k) - 0 ).| < e by A9;

                end;

                hence ex m be Nat st for k be Nat st m <= k holds |.((absrseq . k) - 0 ).| < e;

              end;

              then

               A35: absrseq is convergent by SEQ_2:def 6;

              then ( lim absrseq) = 0 by A33, SEQ_2:def 7;

              

              then

               A36: ( lim rseqn2) = ( 0 * 0 ) by A35, SEQ_2: 15

              .= 0 ;

              

               A37: rseqn2 is convergent by A35, SEQ_2: 14;

              then

               A38: seq2 is convergent by A18, A32, SEQ_2: 5;

              ( lim ||.(seqn - xn).||) = 0 by A16, A15, NORMSP_1: 24;

              

              then ( lim seqn2) = ( 0 * 0 ) by A17, SEQ_2: 15

              .= 0 ;

              

              then

               A39: ( lim seq2) = ( 0 + 0 ) by A18, A37, A36, A32, SEQ_2: 6

              .= 0 ;

              

               A40: for e be Real st e > 0 holds ex m be Nat st for k be Nat st k >= m holds ||.((seq . k) - x).|| < e

              proof

                let e be Real such that

                 A41: e > 0 ;

                (e * 0 ) < (e * e) by A41, XREAL_1: 97;

                then

                consider m be Nat such that

                 A42: for k be Nat st m <= k holds |.((seq2 . k) - 0 ).| < (e * e) by A38, A39, SEQ_2:def 7;

                now

                  let k be Nat such that

                   A43: m <= k;

                  ( ||.(seq - x).|| . k) = ||.((seq - x) . k).|| by NORMSP_0:def 4

                  .= ||.((seq . k) - x).|| by NORMSP_1:def 4;

                  then (seq2 . k) = ( ||.((seq . k) - x).|| * ||.((seq . k) - x).||) by SEQ_1: 8;

                  then |.((seq2 . k) - 0 ).| = ( ||.((seq . k) - x).|| * ||.((seq . k) - x).||) by ABSVALUE:def 1;

                  then

                   A44: ( ||.((seq . k) - x).|| * ||.((seq . k) - x).||) < (e * e) by A42, A43;

                  

                   A45: ( sqrt ( ||.((seq . k) - x).|| * ||.((seq . k) - x).||)) = ( sqrt ( ||.((seq . k) - x).|| ^2 ))

                  .= ||.((seq . k) - x).|| by SQUARE_1: 22;

                  ( sqrt (e * e)) = ( sqrt (e ^2 ))

                  .= e by A41, SQUARE_1: 22;

                  hence ||.((seq . k) - x).|| < e by A44, A45, SQUARE_1: 27;

                end;

                hence thesis;

              end;

              then seq is convergent by NORMSP_1:def 6;

              hence thesis by A40, NORMSP_1:def 7;

            end;

          end;

          now

            assume

             A46: seq is convergent & ( lim seq) = x;

            now

              let i be Nat such that

               A47: i in ( Seg (n + 1));

              deffunc F( Nat) = ((xseq . $1) . i);

              consider rseqi be Real_Sequence such that

               A48: for l be Nat holds (rseqi . l) = F(l) from SEQ_1:sch 1;

               A49:

              now

                let e be Real such that

                 A50: e > 0 ;

                thus ex k be Nat st for m be Nat st k <= m holds |.((rseqi . m) - (xs . i)).| < e

                proof

                  consider k be Nat such that

                   A51: for m be Nat st m >= k holds ||.((seq . m) - x).|| < e by A46, A50, NORMSP_1:def 7;

                  take k;

                  let m be Nat;

                  assume k <= m;

                  then

                   A52: ||.((seq . m) - x).|| < e by A51;

                  ( len ((xseq . m) - xs)) = (n + 1) by CARD_1:def 7;

                  then i in ( dom ((xseq . m) - xs)) by A47, FINSEQ_1:def 3;

                  then (((xseq . m) . i) - (xs . i)) = (((xseq . m) - xs) . i) by VALUED_1: 13;

                  then

                   A53: |.(((xseq . m) . i) - (xs . i)).| <= ||.((seq . m) - x).|| by A3, A47, Th5, Th9;

                  ((rseqi . m) - (xs . i)) = (((xseq . m) . i) - (xs . i)) by A48;

                  hence thesis by A52, A53, XXREAL_0: 2;

                end;

              end;

              then

               A54: rseqi is convergent by SEQ_2:def 6;

              then (xs . i) = ( lim rseqi) by A49, SEQ_2:def 7;

              hence ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi) by A48, A54;

            end;

            hence for i be Nat st i in ( Seg (n + 1)) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi);

          end;

          hence seq is convergent & ( lim seq) = x iff for i be Nat st i in ( Seg (n + 1)) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi) by A4;

        end;

        hence P[(n + 1)];

      end;

      

       A55: P[ 0 ]

      proof

        let x be Point of ( REAL-NS 0 ), xs be Element of ( REAL 0 ), seq be sequence of ( REAL-NS 0 ), xseq be sequence of ( REAL 0 );

        assume that

         A56: xs = x and

         A57: xseq = seq;

        now

          assume for i be Nat st i in ( Seg 0 ) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi);

          

           A58: for i be Nat holds (seq . i) = ( 0. ( REAL-NS 0 ))

          proof

            let i be Nat;

            (xseq . i) = ( 0.REAL 0 );

            hence thesis by A57, Def4;

          end;

          xs = ( 0* 0 );

          then

           A59: x = ( 0. ( REAL-NS 0 )) by A56, Def4;

          

           A60: for r be Real st 0 < r holds ex m be Nat st for k be Nat st m <= k holds ||.((seq . k) - x).|| < r

          proof

            let r be Real;

            assume

             A61: 0 < r;

            take m = 1;

            let k be Nat;

            assume m <= k;

             ||.((seq . k) - x).|| = ||.(( 0. ( REAL-NS 0 )) - ( 0. ( REAL-NS 0 ))).|| by A59, A58

            .= ||.( 0. ( REAL-NS 0 )).|| by RLVECT_1: 15

            .= 0 ;

            hence thesis by A61;

          end;

          then seq is convergent by NORMSP_1:def 6;

          hence seq is convergent & ( lim seq) = x by A60, NORMSP_1:def 7;

        end;

        hence thesis;

      end;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A55, A1);

    end;

    theorem :: REAL_NS1:12

    

     Th12: for f be sequence of ( REAL-NS n) st f is Cauchy_sequence_by_Norm holds f is convergent

    proof

      let vseq be sequence of ( REAL-NS n) such that

       A1: vseq is Cauchy_sequence_by_Norm;

      reconsider xvseq = vseq as sequence of ( REAL n) by Def4;

      defpred P[ set, set] means ex rseqi be Real_Sequence st for l be Nat holds (rseqi . l) = ((xvseq . l) . $1) & rseqi is convergent & $2 = ( lim rseqi);

      

       A2: for i be Nat st i in ( Seg n) holds ex y be Element of REAL st P[i, y]

      proof

        let i be Nat such that

         A3: i in ( Seg n);

        deffunc F( Nat) = ((xvseq . $1) . i);

        consider rseqi be Real_Sequence such that

         A4: for l be Nat holds (rseqi . l) = F(l) from SEQ_1:sch 1;

        reconsider lr = ( lim rseqi) as Element of REAL by XREAL_0:def 1;

        take lr;

        now

          let e be Real such that

           A5: e > 0 ;

          thus ex k be Nat st for m be Nat st k <= m holds |.((rseqi . m) - (rseqi . k)).| < e

          proof

            consider k be Nat such that

             A6: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A5, RSSPACE3: 8;

            take k;

            let m be Nat;

            assume k <= m;

            then

             A7: ||.((vseq . m) - (vseq . k)).|| < e by A6;

            ( len ((xvseq . m) - (xvseq . k))) = n by CARD_1:def 7;

            then i in ( dom ((xvseq . m) - (xvseq . k))) by A3, FINSEQ_1:def 3;

            then (((xvseq . m) . i) - ((xvseq . k) . i)) = (((xvseq . m) - (xvseq . k)) . i) by VALUED_1: 13;

            then

             A8: |.(((xvseq . m) . i) - ((xvseq . k) . i)).| <= ||.((vseq . m) - (vseq . k)).|| by A3, Th5, Th9;

            (rseqi . m) = ((xvseq . m) . i) & (rseqi . k) = ((xvseq . k) . i) by A4;

            hence thesis by A7, A8, XXREAL_0: 2;

          end;

        end;

        then rseqi is convergent by SEQ_4: 41;

        hence thesis by A4;

      end;

      consider f be FinSequence of REAL such that

       A9: ( dom f) = ( Seg n) & for k be Nat st k in ( Seg n) holds P[k, (f . k)] from FINSEQ_1:sch 5( A2);

      reconsider tseq = f as Element of ( REAL n) by A9, Th6;

      reconsider xseq = tseq as Point of ( REAL-NS n) by Def4;

      

       A10: xseq = tseq;

      for k be Nat st k in ( Seg n) holds P[k, (f . k)] by A9;

      hence thesis by A10, Th11;

    end;

    

     Lm2: ( REAL-NS n) is RealBanachSpace

    proof

      for seq be sequence of ( REAL-NS n) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th12;

      hence thesis by LOPBAN_1:def 15;

    end;

    registration

      let n;

      cluster ( REAL-NS n) -> complete;

      coherence by Lm2;

    end

    begin

    definition

      let n be Nat;

      :: REAL_NS1:def5

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

      : Def5: for x,y be Element of ( REAL n) holds (it . (x,y)) = ( Sum ( mlt (x,y)));

      existence

      proof

        deffunc F( Element of ( REAL n), Element of ( REAL n)) = ( In (( Sum ( mlt ($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 scalar1,scalar2 be Function of [:( REAL n), ( REAL n):], REAL such that

         A2: for x,y be Element of ( REAL n) holds (scalar1 . (x,y)) = ( Sum ( mlt (x,y))) and

         A3: for x,y be Element of ( REAL n) holds (scalar2 . (x,y)) = ( Sum ( mlt (x,y)));

        for x,y be Element of ( REAL n) holds (scalar1 . (x,y)) = (scalar2 . (x,y))

        proof

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

          (scalar1 . (x,y)) = ( Sum ( mlt (x,y))) by A2;

          hence thesis by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let n be Nat;

      :: REAL_NS1:def6

      func REAL-US n -> strict non empty UNITSTR means

      : Def6: the carrier of it = ( REAL n) & ( 0. it ) = ( 0* n) & the addF of it = ( Euclid_add n) & the Mult of it = ( Euclid_mult n) & the scalar of it = ( Euclid_scalar n);

      existence

      proof

        take UNITSTR (# ( REAL n), ( 0* n), ( Euclid_add n), ( Euclid_mult n), ( Euclid_scalar n) #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let n be non zero Nat;

      cluster ( REAL-US n) -> non trivial;

      coherence

      proof

        the carrier of ( REAL-US n) = ( REAL n) by Def6

        .= the carrier of ( TOP-REAL n) by EUCLID: 22;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

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

      coherence

      proof

        now

          let x,y,z be Point of ( REAL-US n), a be Real;

          reconsider x1 = x, y1 = y, z1 = z as Element of ( REAL n) by Def6;

          reconsider x2 = x1, y2 = y1, z2 = z1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          

           A1: ( len x2) = n & ( len y2) = n by CARD_1:def 7;

          

           A2: for k be Nat st k in ( dom ( mlt (x1,x1))) holds 0 <= (( mlt (x1,x1)) . k)

          proof

            let k be Nat;

            assume k in ( dom ( mlt (x1,x1)));

            (( mlt (x1,x1)) . k) = ((x1 . k) * (x1 . k)) by RVSUM_1: 59;

            hence thesis by XREAL_1: 63;

          end;

          

           A3: (x .|. x) = (( Euclid_scalar n) . (x,x)) by Def6

          .= ( Sum ( mlt (x1,x1))) by Def5;

          hence 0 <= (x .|. x) by A2, RVSUM_1: 84;

          thus (x .|. x) = 0 iff x = ( 0. ( REAL-US n))

          proof

            now

              assume that

               A4: (x .|. x) = 0 and

               A5: x <> ( 0. ( REAL-US n));

              for k be Element of NAT st k in ( dom x2) holds (x2 . k) = 0

              proof

                let k be Element of NAT ;

                ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

                then [:( rng x1), ( rng x1):] c= ( dom multreal ) by ZFMISC_1: 96;

                then

                 A6: ( dom ( multreal .: (x1,x1))) = (( dom x1) /\ ( dom x1)) by FUNCOP_1: 69;

                assume k in ( dom x2);

                then

                 A7: k in ( dom ( mlt (x1,x1))) by A6, RVSUM_1:def 9;

                then 0 <= (( mlt (x1,x1)) . k) by A2;

                then (( mlt (x1,x1)) . k) = 0 by A3, A2, A4, A7, RVSUM_1: 85;

                then ((x1 . k) ^2 ) = 0 by RVSUM_1: 59;

                hence thesis by SQUARE_1: 12;

              end;

              then x1 = (n |-> 0 qua Real) by RFUNCT_4: 4;

              then x = ( 0* n) by EUCLID:def 4;

              hence contradiction by A5, Def6;

            end;

            hence (x .|. x) = 0 implies x = ( 0. ( REAL-US n));

            assume x = ( 0. ( REAL-US n));

            

            then x = ( 0* n) by Def6

            .= (n |-> 0 qua Real) by EUCLID:def 4;

            

            then ( mlt (x2,x2)) = ( 0 * x2) by RVSUM_1: 63

            .= (n |-> 0 ) by RVSUM_1: 53;

            hence thesis by A3, RVSUM_1: 81;

          end;

          

           A8: ( len z2) = n by CARD_1:def 7;

          

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

          .= ( Sum ( mlt (y1,x1))) by Def5

          .= (( Euclid_scalar n) . (y,x)) by Def5

          .= (y .|. x) by Def6;

          

           A9: (x .|. z) = (( Euclid_scalar n) . (x,z)) by Def6

          .= ( Sum ( mlt (x1,z1))) by Def5;

          (a * x) is Element of ( REAL n) by Def6;

          then

          reconsider ax = (a * x) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          

           A10: for k be Nat st k in ( Seg n) holds (ax . k) = ((a * x1) . k)

          proof

            reconsider a as Real;

            let k be Nat;

            assume k in ( Seg n);

            (a * x) = (( Euclid_mult n) . (a,x1)) by Def6

            .= (a * x1) by Def2;

            hence thesis;

          end;

          

           A11: (y .|. z) = (( Euclid_scalar n) . (y,z)) by Def6

          .= ( Sum ( mlt (y1,z1))) by Def5;

          

          thus ((x + y) .|. z) = (( Euclid_scalar n) . ((x + y),z)) by Def6

          .= (( Euclid_scalar n) . ((( Euclid_add n) . (x1,y1)),z1)) by Def6

          .= (( Euclid_scalar n) . ((x1 + y1),z1)) by Def1

          .= ( Sum ( mlt ((x1 + y1),z1))) by Def5

          .= ( Sum (( mlt (x1,z1)) + ( mlt (y1,z1)))) by A1, A8, RVSUM_1: 118

          .= (( Sum ( mlt (x2,z2))) + ( Sum ( mlt (y2,z2)))) by RVSUM_1: 89

          .= ((x .|. z) + (y .|. z)) by A9, A11;

          

          thus ((a * x) .|. y) = (( Euclid_scalar n) . ((a * x),y)) by Def6

          .= (( Euclid_scalar n) . ((a * x1),y1)) by A10, FINSEQ_2: 119

          .= ( Sum ( mlt ((a * x1),y1))) by Def5

          .= ( Sum (a * ( mlt (x2,y2)))) by RVSUM_1: 65

          .= (a * ( Sum ( mlt (x2,y2)))) by RVSUM_1: 87

          .= (a * (( Euclid_scalar n) . (x1,y1))) by Def5

          .= (a * (x .|. y)) by Def6;

        end;

        hence ( REAL-US n) is RealUnitarySpace-like;

        

         A12: for a,b be Real holds for v be VECTOR of ( REAL-US n) holds ((a * b) * v) = (a * (b * v))

        proof

          let a,b be Real;

          let v be VECTOR of ( REAL-US n);

          reconsider v1 = v as Element of ( REAL n) by Def6;

          reconsider a, b as Real;

          reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          (b * v) is Element of ( REAL n) by Def6;

          then

          reconsider bv = (b * v) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          for k be Nat st k in ( Seg n) holds (bv . k) = ((b * v1) . k)

          proof

            reconsider b as Element of REAL by XREAL_0:def 1;

            let k be Nat;

            assume k in ( Seg n);

            (b * v) = (( Euclid_mult n) . (b,v1)) by Def6

            .= (b * v1) by Def2;

            hence thesis;

          end;

          then (b * v1) = (b * v) by FINSEQ_2: 119;

          

          then

           A13: (a * (b * v)) = (( Euclid_mult n) . (a,(b * v1))) by Def6

          .= (a * (b * v2)) by Def2;

          ((a * b) * v) = (( Euclid_mult n) . ((a * b),v1)) by Def6

          .= ((a * b) * v2) by Def2

          .= (a * (b * v2)) by RVSUM_1: 49;

          hence thesis by A13;

        end;

        

         A14: for a be Real holds for v,w be VECTOR of ( REAL-US n) holds (a * (v + w)) = ((a * v) + (a * w))

        proof

          let a be Real;

          let v,w be VECTOR of ( REAL-US n);

          reconsider v1 = v, w1 = w as Element of ( REAL n) by Def6;

          reconsider a as Real;

          reconsider v2 = v1, w2 = w1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          (a * v) is Element of ( REAL n) by Def6;

          then

          reconsider av = (a * v) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          

           A15: for k be Nat st k in ( Seg n) holds (av . k) = ((a * v1) . k)

          proof

            let k be Nat;

            assume k in ( Seg n);

            (a * v) = (( Euclid_mult n) . (a,v1)) by Def6

            .= (a * v1) by Def2;

            hence thesis;

          end;

          (a * w) is Element of ( REAL n) by Def6;

          then

          reconsider aw = (a * w) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          for k be Nat st k in ( Seg n) holds (aw . k) = ((a * w1) . k)

          proof

            reconsider a as Element of REAL by XREAL_0:def 1;

            let k be Nat;

            assume k in ( Seg n);

            (a * w) = (( Euclid_mult n) . (a,w1)) by Def6

            .= (a * w1) by Def2;

            hence thesis;

          end;

          then

           A16: (a * v1) is Element of (n -tuples_on REAL ) & (a * w1) = (a * w) by EUCLID:def 1, FINSEQ_2: 119;

          

           A17: ((a * v) + (a * w)) = (( Euclid_add n) . ((a * v),(a * w))) by Def6

          .= (( Euclid_add n) . ((a * v1),(a * w1))) by A15, A16, FINSEQ_2: 119

          .= ((a * v2) + (a * w2)) by Def1;

          (a * (v + w)) = (( Euclid_mult n) . (a,(v + w))) by Def6

          .= (( Euclid_mult n) . (a,(( Euclid_add n) . (v1,w1)))) by Def6

          .= (( Euclid_mult n) . (a,(v1 + w1))) by Def1

          .= (a * (v1 + w1)) by Def2

          .= ((a * v2) + (a * w2)) by RVSUM_1: 51;

          hence thesis by A17;

        end;

        

         A18: for a,b be Real holds for v be VECTOR of ( REAL-US n) holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Real;

          let v be VECTOR of ( REAL-US n);

          reconsider v1 = v as Element of ( REAL n) by Def6;

          reconsider a, b as Real;

          reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          

           A19: ((a + b) * v) = (( Euclid_mult n) . ((a + b),v1)) by Def6

          .= ((a + b) * v2) by Def2

          .= ((a * v1) + (b * v1)) by RVSUM_1: 50;

          (a * v) is Element of ( REAL n) by Def6;

          then

          reconsider av = (a * v) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          

           A20: for k be Nat st k in ( Seg n) holds (av . k) = ((a * v1) . k)

          proof

            reconsider a as Element of REAL by XREAL_0:def 1;

            let k be Nat;

            assume k in ( Seg n);

            (a * v) = (( Euclid_mult n) . (a,v1)) by Def6

            .= (a * v1) by Def2;

            hence thesis;

          end;

          (b * v) is Element of ( REAL n) by Def6;

          then

          reconsider bv = (b * v) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          for k be Nat st k in ( Seg n) holds (bv . k) = ((b * v1) . k)

          proof

            reconsider b as Element of REAL by XREAL_0:def 1;

            let k be Nat;

            assume k in ( Seg n);

            (b * v) = (( Euclid_mult n) . (b,v1)) by Def6

            .= (b * v1) by Def2;

            hence thesis;

          end;

          then

           A21: (a * v1) is Element of (n -tuples_on REAL ) & (b * v1) = (b * v) by EUCLID:def 1, FINSEQ_2: 119;

          ((a * v) + (b * v)) = (( Euclid_add n) . ((a * v),(b * v))) by Def6

          .= (( Euclid_add n) . ((a * v1),(b * v1))) by A20, A21, FINSEQ_2: 119

          .= ((a * v2) + (b * v2)) by Def1;

          hence thesis by A19;

        end;

        for v be VECTOR of ( REAL-US n) holds (1 * v) = v

        proof

          let v be VECTOR of ( REAL-US n);

          reconsider v1 = v as Element of ( REAL n) by Def6;

          reconsider v2 = v1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          (1 * v) = (( Euclid_mult n) . (1,v1)) by Def6

          .= (1 * v2) by Def2

          .= v2 by RVSUM_1: 52;

          hence thesis;

        end;

        hence ( REAL-US n) is vector-distributive scalar-distributive scalar-associative scalar-unital by A14, A18, A12;

        thus ( REAL-US n) is Abelian

        proof

          let v,w be VECTOR of ( REAL-US n);

          reconsider v1 = v, w1 = w as Element of ( REAL n) by Def6;

          

          thus (v + w) = (( Euclid_add n) . (v,w)) by Def6

          .= (( Euclid_add n) . (w1,v1)) by BINOP_1:def 2

          .= (w + v) by Def6;

        end;

        for u,v,w be Element of ( REAL-US n) holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be Element of ( REAL-US n);

          reconsider u1 = u, v1 = v, w1 = w as Element of ( REAL n) by Def6;

          reconsider u2 = u1, v2 = v1, w2 = w1 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

          

           A22: (u + (v + w)) = (( Euclid_add n) . (u1,(v + w))) by Def6

          .= (( Euclid_add n) . (u2,(( Euclid_add n) . (v2,w2)))) by Def6

          .= (( Euclid_add n) . (u2,(v1 + w1))) by Def1;

          ((u + v) + w) = (( Euclid_add n) . ((u + v),w1)) by Def6

          .= (( Euclid_add n) . ((( Euclid_add n) . (u1,v1)),w1)) by Def6

          .= (( Euclid_add n) . ((u1 + v1),w1)) by Def1

          .= ((u1 + v1) + w2) by Def1

          .= (u2 + (v2 + w2)) by RVSUM_1: 15;

          hence thesis by A22, Def1;

        end;

        hence ( REAL-US n) is add-associative;

        for v be Element of ( REAL-US n) holds (v + ( 0. ( REAL-US n))) = v

        proof

          let v be Element of ( REAL-US n);

          reconsider v1 = v as Element of ( REAL n) by Def6;

          (v + ( 0. ( REAL-US n))) = (( Euclid_add n) . (v,( 0. ( REAL-US n)))) by Def6

          .= (( Euclid_add n) . (v1,( 0* n))) by Def6

          .= (v1 + ( 0* n)) by Def1;

          hence thesis by EUCLID_4: 1;

        end;

        hence ( REAL-US n) is right_zeroed;

        let v be Element of ( REAL-US n);

        reconsider v1 = v as Element of ( REAL n) by Def6;

        reconsider w = ( - v1) as Element of ( REAL-US n) by Def6;

        take w;

        

        thus (v + w) = (( Euclid_add n) . (v1,( - v1))) by Def6

        .= (v1 + ( - v1)) by Def1

        .= ( 0* n) by EUCLIDLP: 2

        .= ( 0. ( REAL-US n)) by Def6;

      end;

    end

    theorem :: REAL_NS1:13

    

     Th13: for n be Nat, a be Real, x1,y1 be Point of ( REAL-NS n), x2,y2 be Point of ( REAL-US n) st x1 = x2 & y1 = y2 holds (x1 + y1) = (x2 + y2) & ( - x1) = ( - x2) & (a * x1) = (a * x2)

    proof

      let n be Nat, a be Real;

      let x1,y1 be Point of ( REAL-NS n);

      reconsider x = x1, y = y1 as Element of ( REAL n) by Def4;

      let x2,y2 be Point of ( REAL-US n);

      assume that

       A1: x1 = x2 and

       A2: y1 = y2;

      

      thus (x1 + y1) = (( Euclid_add n) . (x,y)) by Def4

      .= (x2 + y2) by A1, A2, Def6;

      

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

      .= (( Euclid_mult n) . (( - 1),x)) by Def4

      .= (( - 1) * x2) by A1, Def6

      .= ( - x2) by RLVECT_1: 16;

      

      thus (a * x1) = (( Euclid_mult n) . (a,x)) by Def4

      .= (a * x2) by A1, Def6;

    end;

    theorem :: REAL_NS1:14

    for n be Nat, x1 be Point of ( REAL-NS n), x2 be Point of ( REAL-US n) st x1 = x2 holds ( ||.x1.|| ^2 ) = (x2 .|. x2)

    proof

      let n be Nat, x1 be Point of ( REAL-NS n), x2 be Point of ( REAL-US n);

      reconsider x = x1 as Element of ( REAL n) by Def4;

      assume

       A1: x1 = x2;

      

      thus ( ||.x1.|| ^2 ) = ( |.x.| ^2 ) by Th1

      .= |(x, x)| by EUCLID_2: 4

      .= ( Sum ( mlt (x,x))) by RVSUM_1:def 16

      .= (( Euclid_scalar n) . (x,x)) by Def5

      .= (x2 .|. x2) by A1, Def6;

    end;

    theorem :: REAL_NS1:15

    

     Th15: for n be Nat, f be set holds f is sequence of ( REAL-NS n) iff f is sequence of ( REAL-US n)

    proof

      let n be Nat, f be set;

      the carrier of ( REAL-NS n) = ( REAL n) by Def4

      .= the carrier of ( REAL-US n) by Def6;

      hence thesis;

    end;

    theorem :: REAL_NS1:16

    

     Th16: for n be Nat, seq1 be sequence of ( REAL-NS n), seq2 be sequence of ( REAL-US n) st seq1 = seq2 holds (seq1 is convergent implies seq2 is convergent & ( lim seq1) = ( lim seq2)) & (seq2 is convergent implies seq1 is convergent & ( lim seq1) = ( lim seq2))

    proof

      let n be Nat;

      let seq1 be sequence of ( REAL-NS n);

      let seq2 be sequence of ( REAL-US n);

      assume

       A1: seq1 = seq2;

      

       A2: the carrier of ( REAL-NS n) = ( REAL n) by Def4

      .= the carrier of ( REAL-US n) by Def6;

      now

        reconsider LIMIT = ( lim seq1) as Point of ( REAL-US n) by A2;

        assume

         A3: seq1 is convergent;

        then

        consider RNg be Point of ( REAL-NS n) such that

         A4: for r be Real st 0 < r holds ex m be Nat st for k be Nat st m <= k holds ||.((seq1 . k) - RNg).|| < r by NORMSP_1:def 6;

        reconsider RUg = RNg as Point of ( REAL-US n) by A2;

        for r be Real st 0 < r holds ex m be Nat st for k be Nat st m <= k holds ( dist ((seq2 . k),RUg)) < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           A5: for k be Nat st m <= k holds ||.((seq1 . k) - RNg).|| < r by A4;

          take m;

          let k be Nat;

          reconsider p = ((seq1 . k) - RNg) as Element of ( REAL n) by Def4;

          assume

           A6: m <= k;

          ( - RNg) = ( - RUg) by Th13;

          then

           A7: p = ((seq2 . k) - RUg) by A1, Th13;

           ||.((seq1 . k) - RNg).|| = |.p.| by Th1

          .= ( sqrt |(p, p)|) by EUCLID_2: 5

          .= ( sqrt ( Sum ( mlt (p,p)))) by RVSUM_1:def 16

          .= ( sqrt (( Euclid_scalar n) . (p,p))) by Def5

          .= ||.((seq2 . k) - RUg).|| by A7, Def6;

          hence thesis by A5, A6;

        end;

        hence

         A8: seq2 is convergent by BHSP_2:def 1;

        for r be Real st r > 0 holds ex m be Nat st for k be Nat st k >= m holds ( dist ((seq2 . k),LIMIT)) < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider m be Nat such that

           A9: for k be Nat st m <= k holds ||.((seq1 . k) - ( lim seq1)).|| < r by A3, NORMSP_1:def 7;

          take m;

          let k be Nat;

          reconsider p = ((seq1 . k) - ( lim seq1)) as Element of ( REAL n) by Def4;

          assume

           A10: m <= k;

          ( - ( lim seq1)) = ( - LIMIT) by Th13;

          then

           A11: p = ((seq2 . k) - LIMIT) by A1, Th13;

           ||.((seq1 . k) - ( lim seq1)).|| = |.p.| by Th1

          .= ( sqrt |(p, p)|) by EUCLID_2: 5

          .= ( sqrt ( Sum ( mlt (p,p)))) by RVSUM_1:def 16

          .= ( sqrt (( Euclid_scalar n) . (p,p))) by Def5

          .= ||.((seq2 . k) - LIMIT).|| by A11, Def6;

          hence thesis by A9, A10;

        end;

        hence ( lim seq2) = ( lim seq1) by A8, BHSP_2:def 2;

      end;

      hence seq1 is convergent implies seq2 is convergent & ( lim seq1) = ( lim seq2);

      now

        reconsider LIMIT = ( lim seq2) as Point of ( REAL-NS n) by A2;

        assume

         A12: seq2 is convergent;

        then

        consider RUg be Point of ( REAL-US n) such that

         A13: for r be Real st 0 < r holds ex m be Nat st for k be Nat st m <= k holds ( dist ((seq2 . k),RUg)) < r by BHSP_2:def 1;

        reconsider RNg = RUg as Point of ( REAL-NS n) by A2;

        for r be Real st 0 < r holds ex m be Nat st for k be Nat st m <= k holds ||.((seq1 . k) - RNg).|| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           A14: for k be Nat st m <= k holds ( dist ((seq2 . k),RUg)) < r by A13;

          take m;

          for k be Nat st m <= k holds ||.((seq1 . k) - RNg).|| < r

          proof

            let k be Nat;

            reconsider p = ((seq2 . k) - RUg) as Element of ( REAL n) by Def6;

            assume m <= k;

            then

             A15: ( dist ((seq2 . k),RUg)) < r by A14;

            ( - RNg) = ( - RUg) by Th13;

            then

             A16: p = ((seq1 . k) - RNg) by A1, Th13;

            ( dist ((seq2 . k),RUg)) = ( sqrt (( Euclid_scalar n) . (p,p))) by Def6

            .= ( sqrt ( Sum ( mlt (p,p)))) by Def5

            .= ( sqrt |(p, p)|) by RVSUM_1:def 16

            .= |.p.| by EUCLID_2: 5;

            hence thesis by A15, A16, Th1;

          end;

          hence thesis;

        end;

        hence

         A17: seq1 is convergent by NORMSP_1:def 6;

        for r be Real st r > 0 holds ex m be Nat st for k be Nat st k >= m holds ||.((seq1 . k) - LIMIT).|| < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider m be Nat such that

           A18: for k be Nat st k >= m holds ( dist ((seq2 . k),( lim seq2))) < r by A12, BHSP_2:def 2;

          take m;

          let k be Nat;

          assume k >= m;

          then

           A19: ( dist ((seq2 . k),( lim seq2))) < r by A18;

          reconsider p = ((seq2 . k) - ( lim seq2)) as Element of ( REAL n) by Def6;

          ( - ( lim seq2)) = ( - LIMIT) by Th13;

          then

           A20: p = ((seq1 . k) - LIMIT) by A1, Th13;

          ( dist ((seq2 . k),( lim seq2))) = ( sqrt (( Euclid_scalar n) . (p,p))) by Def6

          .= ( sqrt ( Sum ( mlt (p,p)))) by Def5

          .= ( sqrt |(p, p)|) by RVSUM_1:def 16

          .= |.p.| by EUCLID_2: 5;

          hence thesis by A19, A20, Th1;

        end;

        hence ( lim seq1) = ( lim seq2) by A17, NORMSP_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: REAL_NS1:17

    for n be Nat, seq1 be sequence of ( REAL-NS n), seq2 be sequence of ( REAL-US n) st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds seq2 is Cauchy

    proof

      let n be Nat, seq1 be sequence of ( REAL-NS n), seq2 be sequence of ( REAL-US n);

      assume that

       A1: seq1 = seq2 and

       A2: seq1 is Cauchy_sequence_by_Norm;

      let r be Real;

      assume

       A3: r > 0 ;

      reconsider r as Real;

      r > 0 by A3;

      then

      consider k be Nat such that

       A4: for n,m be Nat st n >= k & m >= k holds ( dist ((seq1 . n),(seq1 . m))) < r by A2;

      take k;

      let m1,m2 be Nat;

      reconsider p = ((seq2 . m1) - (seq2 . m2)) as Element of ( REAL n) by Def6;

      ( - (seq1 . m2)) = ( - (seq2 . m2)) by A1, Th13;

      then ((seq1 . m1) + ( - (seq1 . m2))) = ((seq2 . m1) + ( - (seq2 . m2))) by A1, Th13;

      

      then

       A5: ||.((seq1 . m1) - (seq1 . m2)).|| = |.p.| by Th1

      .= ( sqrt |(p, p)|) by EUCLID_2: 5

      .= ( sqrt ( Sum ( mlt (p,p)))) by RVSUM_1:def 16

      .= ( sqrt (( Euclid_scalar n) . (p,p))) by Def5

      .= ||.((seq2 . m1) - (seq2 . m2)).|| by Def6;

      assume m1 >= k & m2 >= k;

      then ( dist ((seq1 . m1),(seq1 . m2))) < r by A4;

      hence thesis by A5;

    end;

    theorem :: REAL_NS1:18

    

     Th18: for n be Nat, seq1 be sequence of ( REAL-NS n), seq2 be sequence of ( REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds seq1 is Cauchy_sequence_by_Norm

    proof

      let n be Nat, seq1 be sequence of ( REAL-NS n), seq2 be sequence of ( REAL-US n);

      assume that

       A1: seq1 = seq2 and

       A2: seq2 is Cauchy;

      let r be Real;

      assume r > 0 ;

      then

      consider k be Nat such that

       A3: for m1,m2 be Nat st m1 >= k & m2 >= k holds ( dist ((seq2 . m1),(seq2 . m2))) < r by A2;

      take k;

      let m1,m2 be Nat;

      reconsider p = ((seq2 . m1) - (seq2 . m2)) as Element of ( REAL n) by Def6;

      ( - (seq1 . m2)) = ( - (seq2 . m2)) by A1, Th13;

      then

       A4: p = ((seq1 . m1) - (seq1 . m2)) by A1, Th13;

      assume m1 >= k & m2 >= k;

      then

       A5: ( dist ((seq2 . m1),(seq2 . m2))) < r by A3;

       ||.((seq2 . m1) - (seq2 . m2)).|| = ( sqrt (( Euclid_scalar n) . (p,p))) by Def6

      .= ( sqrt ( Sum ( mlt (p,p)))) by Def5

      .= ( sqrt |(p, p)|) by RVSUM_1:def 16

      .= |.p.| by EUCLID_2: 5

      .= ||.((seq1 . m1) - (seq1 . m2)).|| by A4, Th1;

      hence thesis by A5;

    end;

    registration

      let n;

      cluster ( REAL-US n) -> complete;

      coherence

      proof

        let seq be sequence of ( REAL-US n);

        reconsider seq9 = seq as sequence of ( REAL-NS n) by Th15;

        assume seq is Cauchy;

        then seq9 is convergent by Th12, Th18;

        hence thesis by Th16;

      end;

    end