normsp_0.miz

    begin

    definition

      let RNS be non empty 1-sorted;

      let s be sequence of RNS, n be Nat;

      :: original: .

      redefine

      func s . n -> Element of RNS ;

      coherence

      proof

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

        (s . n) is Element of RNS;

        hence thesis;

      end;

    end

    definition

      struct ( 1-sorted) N-Str (# the carrier -> set,

the normF -> Function of the carrier, REAL #)

       attr strict strict;

    end

     0 in REAL by XREAL_0:def 1;

    then

    reconsider f = op1 as Function of { 0 }, REAL by FUNCOP_1: 46;

    reconsider z = 0 as Element of { 0 } by TARSKI:def 1;

    registration

      cluster non empty strict for N-Str;

      existence

      proof

        take N-Str (# { 0 }, f #);

        thus thesis;

      end;

    end

    definition

      let X be non empty N-Str, x be Element of X;

      :: NORMSP_0:def1

      func ||.x.|| -> Real equals (the normF of X . x);

      coherence ;

    end

    reserve X for non empty N-Str;

    definition

      let X;

      let f be the carrier of X -valued Function;

      :: NORMSP_0:def2

      func ||.f.|| -> Function means

      : Def2: ( dom it ) = ( dom f) & for e be set st e in ( dom it ) holds (it . e) = ||.(f /. e).||;

      existence

      proof

        deffunc F( object) = ||.(f /. $1).||;

        consider g be Function such that

         A1: ( dom g) = ( dom f) and

         A2: for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        take g;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A3: ( dom f1) = ( dom f) and

         A4: for e be set st e in ( dom f1) holds (f1 . e) = ||.(f /. e).|| and

         A5: ( dom f2) = ( dom f) and

         A6: for e be set st e in ( dom f2) holds (f2 . e) = ||.(f /. e).||;

        thus ( dom f1) = ( dom f2) by A3, A5;

        let e be object;

        assume

         A7: e in ( dom f1);



        hence (f1 . e) = ||.(f /. e).|| by A4

        .= (f2 . e) by A3, A5, A6, A7;

      end;

    end

    registration

      let X;

      let f be the carrier of X -valued Function;

      cluster ||.f.|| -> REAL -valued;

      coherence

      proof

        let u be object;

        assume u in ( rng ||.f.||);

        then

        consider e be object such that

         A1: e in ( dom ||.f.||) and

         A2: u = ( ||.f.|| . e) by FUNCT_1:def 3;

        ( ||.f.|| . e) = ||.(f /. e).|| by A1, Def2;

        hence u in REAL by A2;

      end;

    end

    definition

      let C be non empty set, X;

      let f be PartFunc of C, the carrier of X;

      :: original: ||.

      redefine

      :: NORMSP_0:def3

      func ||.f.|| -> PartFunc of C, REAL means ( dom it ) = ( dom f) & for c be Element of C st c in ( dom it ) holds (it . c) = ||.(f /. c).||;

      coherence

      proof

        ( dom ||.f.||) = ( dom f) by Def2;

        then

         A1: ( dom ||.f.||) c= C by RELAT_1:def 18;

        ( rng ||.f.||) c= REAL

        proof

          let e be object;

          assume e in ( rng ||.f.||);

          then

          consider u be object such that

           A2: u in ( dom ||.f.||) and

           A3: e = ( ||.f.|| . u) by FUNCT_1:def 3;

          e = ||.(f /. u).|| by A2, A3, Def2;

          hence e in REAL ;

        end;

        hence ||.f.|| is PartFunc of C, REAL by A1, RELSET_1: 4;

      end;

      compatibility

      proof

        let F be PartFunc of C, REAL ;

        thus F = ||.f.|| implies ( dom F) = ( dom f) & for c be Element of C st c in ( dom F) holds (F . c) = ||.(f /. c).|| by Def2;

        assume that

         A4: ( dom F) = ( dom f) and

         A5: for c be Element of C st c in ( dom F) holds (F . c) = ||.(f /. c).||;

        for e be set st e in ( dom F) holds (F . e) = ||.(f /. e).||

        proof

          let e be set;

          assume

           A6: e in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider c = e as Element of C by A6;



          thus (F . e) = ||.(f /. c).|| by A6, A5

          .= ||.(f /. e).||;

        end;

        hence F = ||.f.|| by A4, Def2;

      end;

    end

    definition

      let X;

      let s be sequence of X;

      :: original: ||.

      redefine

      :: NORMSP_0:def4

      func ||.s.|| -> Real_Sequence means for n be Nat holds (it . n) = ||.(s . n).||;

      coherence

      proof



         A1: ( dom ||.s.||) = ( dom s) by Def2

        .= NAT by PARTFUN1:def 2;

        ( rng ||.s.||) c= REAL by RELAT_1:def 19;

        hence ||.s.|| is Real_Sequence by A1, FUNCT_2: 2;

      end;

      compatibility

      proof

        let S be Real_Sequence;



         A2: ( dom S) = NAT by PARTFUN1:def 2;



         A3: ( dom s) = NAT by PARTFUN1:def 2;

        thus S = ||.s.|| implies for n be Nat holds (S . n) = ||.(s . n).||

        proof

          assume

           A4: S = ||.s.||;

          let n be Nat;



           A5: n in NAT by ORDINAL1:def 12;



          thus (S . n) = ( ||.s.|| . n) by A4

          .= ||.(s /. n).|| by Def2, A2, A4, A5

          .= ||.(s . n).|| by A3, A5, PARTFUN1:def 6;

        end;

        assume

         A6: for n be Nat holds (S . n) = ||.(s . n).||;

        for e be set st e in ( dom s) holds (S . e) = ||.(s /. e).||

        proof

          let e be set;

          assume

           A7: e in ( dom s);

          then

          reconsider n = e as Element of NAT by PARTFUN1:def 2;



          thus (S . e) = ||.(s . n).|| by A6

          .= ||.(s /. e).|| by A7, PARTFUN1:def 6;

        end;

        hence S = ||.s.|| by A2, A3, Def2;

      end;

    end

    definition

      struct ( N-Str, ZeroStr) N-ZeroStr (# the carrier -> set,

the ZeroF -> Element of the carrier,

the normF -> Function of the carrier, REAL #)

       attr strict strict;

    end

    registration

      cluster non empty strict for N-ZeroStr;

      existence

      proof

        take N-ZeroStr (# { 0 }, z, f #);

        thus thesis;

      end;

    end

    reserve X for non empty N-ZeroStr,

x for Element of X;

    definition

      let X;

      :: NORMSP_0:def5

      attr X is discerning means ||.x.|| = 0 implies x = ( 0. X);

      :: NORMSP_0:def6

      attr X is reflexive means

      : Def6: ||.( 0. X).|| = 0 ;

    end

    registration

      cluster reflexive discerning for non empty strict N-ZeroStr;

      existence

      proof

        reconsider S = N-ZeroStr (# { 0 }, z, f #) as non empty strict N-ZeroStr;

        take S;

         ||.( 0. S).|| = 0 by FUNCOP_1: 7;

        hence S is reflexive;

        let x be Element of S;

        thus thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be reflexive non empty N-ZeroStr;

      let x be zero Element of X;

      cluster ||.x.|| -> zero;

      coherence

      proof

        x = ( 0. X) by STRUCT_0:def 12;

        hence thesis by Def6;

      end;

    end