mazurulm.miz



    begin

    reserve E,F,G for RealNormSpace;

    reserve f for Function of E, F;

    reserve g for Function of F, G;

    reserve a,b,c for Point of E;

    reserve t for Real;

    registration

      cluster I[01] -> closed;

      coherence by TOPMETR: 20, TREAL_1: 2;

    end

    reconsider D = DYADIC as Subset of I[01] by BORSUK_1: 40, URYSOHN2: 28;

    

     Lm1: ( Cl D) = ( [#] I[01] )

    proof

      reconsider P = [. 0 , 1.] as Subset of R^1 by MEMBERED: 3, TOPMETR: 17;

      

       A1: I[01] = ( R^1 | P) by TOPMETR: 19, TOPMETR: 20;

      reconsider D1 = D as Subset of ( R^1 | P) by TOPMETR: 19, TOPMETR: 20;

      

       A2: ( Cl D) = (( Cl ( Up D1)) /\ P) by A1, CONNSP_3: 30;

      thus ( Cl D) c= ( [#] I[01] );

      let x be object;

      assume

       A3: x in ( [#] I[01] );

      reconsider p = x as Point of RealSpace by A3, BORSUK_1: 40;

      now

        let r be Real such that

         A4: r > 0 ;

        

         A5: (p - r) < (p - 0 ) by A4, XREAL_1: 10;

        

         A6: p <= 1 by A3, BORSUK_1: 43;

        

         A7: ( Ball (p,r)) = ].(p - r), (p + r).[ by FRECHET: 7;

        per cases ;

          suppose r <= p;

          then (r - r) <= (p - r) by XREAL_1: 9;

          then

          consider c be Real such that

           A8: c in D and

           A9: (p - r) < c and

           A10: c < p by A5, A6, URYSOHN2: 24;

          (p + 0 ) < (p + r) by A4, XREAL_1: 8;

          then c < (p + r) by A10, XXREAL_0: 2;

          then c in ( Ball (p,r)) by A9, A7, XXREAL_1: 4;

          hence ( Ball (p,r)) meets D by A8, XBOOLE_0: 3;

        end;

          suppose r > p;

          then

           A11: (p - r) < (p - p) by XREAL_1: 10;

           0 <= p by A3, BORSUK_1: 43;

          then 0 in ( Ball (p,r)) by A4, A11, A7, XXREAL_1: 4;

          hence ( Ball (p,r)) meets D by URYSOHN2: 27, XBOOLE_0: 3;

        end;

      end;

      then x in ( Cl ( Up D1)) by GOBOARD6: 92, TOPMETR:def 6;

      hence x in ( Cl D) by A3, A2, BORSUK_1: 40, XBOOLE_0:def 4;

    end;

    theorem :: MAZURULM:1

     DYADIC is dense Subset of I[01]

    proof

      D is dense by Lm1;

      hence thesis;

    end;

    theorem :: MAZURULM:2

    

     Th2: ( Cl DYADIC ) = [. 0 , 1.]

    proof

      reconsider W = D as Subset of R^1 by TOPMETR: 17;

      

      thus ( Cl DYADIC ) = ( Cl W) by JORDAN5A: 24

      .= [. 0 , 1.] by Lm1, BORSUK_1: 40, TOPS_3: 55;

    end;

    theorem :: MAZURULM:3

    

     Th3: (a + a) = (2 * a)

    proof

      (1 * a) = a by RLVECT_1:def 8;

      

      hence (a + a) = ((1 + 1) * a) by RLVECT_1:def 6

      .= (2 * a);

    end;

    theorem :: MAZURULM:4

    

     Th4: ((a + b) - b) = a

    proof

      

      thus ((a + b) - b) = (a + (b - b)) by RLVECT_1: 28

      .= (a + ( 0. E)) by RLVECT_1: 15

      .= a;

    end;

    registration

      let A be bounded_above real-membered set;

      let r be non negative Real;

      cluster (r ** A) -> bounded_above;

      coherence

      proof

        per cases ;

          suppose

           A1: A <> {} ;

          A c= REAL by MEMBERED: 3;

          hence thesis by A1, INTEGRA2: 9;

        end;

          suppose A = {} ;

          hence thesis;

        end;

      end;

    end

    registration

      let A be bounded_above real-membered set;

      let r be non positive Real;

      cluster (r ** A) -> bounded_below;

      coherence

      proof

        per cases ;

          suppose

           A1: A <> {} ;

          A c= REAL by MEMBERED: 3;

          hence thesis by A1, INTEGRA2: 10;

        end;

          suppose A = {} ;

          hence thesis;

        end;

      end;

    end

    registration

      let A be bounded_below real-membered set;

      let r be non negative Real;

      cluster (r ** A) -> bounded_below;

      coherence

      proof

        per cases ;

          suppose

           A1: A <> {} ;

          A c= REAL by MEMBERED: 3;

          hence thesis by A1, INTEGRA2: 11;

        end;

          suppose A = {} ;

          hence thesis;

        end;

      end;

    end

    registration

      let A be bounded_below non empty real-membered set;

      let r be non positive Real;

      cluster (r ** A) -> bounded_above;

      coherence

      proof

        A c= REAL by MEMBERED: 3;

        hence thesis by INTEGRA2: 12;

      end;

    end

    theorem :: MAZURULM:5

    

     Th5: for f be Real_Sequence holds (f + ( NAT --> t)) = (t + f)

    proof

      let f be Real_Sequence;

      let n be Element of NAT ;

      

      thus ((f + ( NAT --> t)) . n) = ((f . n) + (( NAT --> t) . n)) by VALUED_1: 1

      .= ((f + t) . n) by VALUED_1: 2;

    end;

    theorem :: MAZURULM:6

    

     Th6: for r be Element of REAL holds ( lim ( NAT --> r)) = r

    proof

      let r be Element of REAL ;

      

      thus ( lim ( NAT --> r)) = (( NAT --> r) . 0 ) by SEQ_4: 26

      .= r;

    end;

    theorem :: MAZURULM:7

    

     Th7: for f be convergent Real_Sequence holds ( lim (t + f)) = (t + ( lim f))

    proof

      let f be convergent Real_Sequence;

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

      (f + ( NAT --> t)) = (t + f) by Th5;

      

      hence ( lim (t + f)) = (( lim ( NAT --> r)) + ( lim f)) by SEQ_2: 6

      .= (t + ( lim f)) by Th6;

    end;

    registration

      let f be convergent Real_Sequence;

      let t;

      cluster (t + f) -> convergent;

      coherence

      proof

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

        (f + ( NAT --> r)) = (t + f) by Th5;

        hence thesis;

      end;

    end

    theorem :: MAZURULM:8

    

     Th8: for f be Real_Sequence holds (f (#) ( NAT --> a)) = (f * a)

    proof

      let f be Real_Sequence;

      let n be Element of NAT ;

      

      thus ((f (#) ( NAT --> a)) . n) = ((f . n) * (( NAT --> a) . n)) by NDIFF_1:def 2

      .= ((f * a) . n) by NDIFF_1:def 3;

    end;

    theorem :: MAZURULM:9

    

     Th9: ( lim ( NAT --> a)) = a

    proof

      

      thus ( lim ( NAT --> a)) = (( NAT --> a) . 0 ) by NDIFF_1: 18

      .= a;

    end;

    theorem :: MAZURULM:10

    

     Th10: for f be convergent Real_Sequence holds ( lim (f * a)) = (( lim f) * a)

    proof

      let f be convergent Real_Sequence;

      (f (#) ( NAT --> a)) = (f * a) by Th8;

      

      hence ( lim (f * a)) = (( lim f) * ( lim ( NAT --> a))) by NDIFF_1: 14, NDIFF_1: 18

      .= (( lim f) * a) by Th9;

    end;

    registration

      let f be convergent Real_Sequence;

      let E, a;

      cluster (f * a) -> convergent;

      coherence

      proof

        (f (#) ( NAT --> a)) = (f * a) by Th8;

        hence thesis by NDIFF_1: 13, NDIFF_1: 18;

      end;

    end

    definition

      let E,F be non empty NORMSTR, f be Function of E, F;

      :: MAZURULM:def1

      attr f is isometric means

      : Def1: for a,b be Point of E holds ||.((f . a) - (f . b)).|| = ||.(a - b).||;

    end

    definition

      let E,F be non empty RLSStruct, f be Function of E, F;

      :: MAZURULM:def2

      attr f is Affine means for a,b be Point of E, t be Real st 0 <= t & t <= 1 holds (f . (((1 - t) * a) + (t * b))) = (((1 - t) * (f . a)) + (t * (f . b)));

      :: MAZURULM:def3

      attr f is midpoints-preserving means for a,b be Point of E holds (f . ((1 / 2) * (a + b))) = ((1 / 2) * ((f . a) + (f . b)));

    end

    registration

      let E be non empty NORMSTR;

      cluster ( id E) -> isometric;

      coherence ;

    end

    registration

      let E be non empty RLSStruct;

      cluster ( id E) -> midpoints-preserving Affine;

      coherence ;

    end

    registration

      let E be non empty NORMSTR;

      cluster bijective isometric midpoints-preserving Affine for UnOp of E;

      existence

      proof

        take ( id E);

        thus thesis;

      end;

    end

    theorem :: MAZURULM:11

    

     Th11: f is isometric & g is isometric implies (g * f) is isometric

    proof

      assume that

       A1: f is isometric and

       A2: g is isometric;

      set h = (g * f);

      let a, b;

      (h . a) = (g . (f . a)) & (h . b) = (g . (f . b)) by FUNCT_2: 15;

      

      hence ||.((h . a) - (h . b)).|| = ||.((f . a) - (f . b)).|| by A2

      .= ||.(a - b).|| by A1;

    end;

    registration

      let E;

      let f,g be isometric UnOp of E;

      cluster (g * f) -> isometric;

      coherence by Th11;

    end

     Lm2:

    now

      let E, F, f;

      assume

       A1: f is bijective;

      set g = (f /" );

      let a be Point of F;

      ( rng f) = ( [#] F) by A1, FUNCT_2:def 3;

      then

       A2: (g /" ) = f by A1, TOPS_2: 51;

      

       A3: g = (f qua Function " ) by A1, TOPS_2:def 4;

      

       A4: g is bijective by A1, PENCIL_2: 12;

      f = (g qua Function " ) by A2, A4, TOPS_2:def 4;

      hence (f . (g . a)) = a by A1, A3, FUNCT_2: 26;

    end;

    theorem :: MAZURULM:12

    

     Th12: f is bijective isometric implies (f /" ) is isometric

    proof

      assume that

       A1: f is bijective and

       A2: f is isometric;

      set g = (f /" );

      let a,b be Point of F;

      (f . (g . a)) = a & (f . (g . b)) = b by A1, Lm2;

      hence thesis by A2;

    end;

    registration

      let E;

      let f be bijective isometric UnOp of E;

      cluster (f /" ) -> isometric;

      coherence by Th12;

    end

    theorem :: MAZURULM:13

    

     Th13: f is midpoints-preserving & g is midpoints-preserving implies (g * f) is midpoints-preserving

    proof

      assume that

       A1: f is midpoints-preserving and

       A2: g is midpoints-preserving;

      set h = (g * f);

      let a, b;

      

       A3: (h . a) = (g . (f . a)) & (h . b) = (g . (f . b)) by FUNCT_2: 15;

      

      thus (h . ((1 / 2) * (a + b))) = (g . (f . ((1 / 2) * (a + b)))) by FUNCT_2: 15

      .= (g . ((1 / 2) * ((f . a) + (f . b)))) by A1

      .= ((1 / 2) * ((h . a) + (h . b))) by A3, A2;

    end;

    registration

      let E;

      let f,g be midpoints-preserving UnOp of E;

      cluster (g * f) -> midpoints-preserving;

      coherence by Th13;

    end

     Lm3:

    now

      let E, F, f;

      assume

       A1: f is bijective;

      then

       A2: ( rng f) = ( [#] F) by FUNCT_2:def 3;

      ( dom f) = ( [#] E) by FUNCT_2:def 1;

      hence ((f /" ) * f) = ( id E) by A1, A2, TOPS_2: 52;

    end;

    theorem :: MAZURULM:14

    

     Th14: f is bijective midpoints-preserving implies (f /" ) is midpoints-preserving

    proof

      assume that

       A1: f is bijective and

       A2: f is midpoints-preserving;

      set g = (f /" );

      let a,b be Point of F;

      

       A3: (g * f) = ( id E) by A1, Lm3;

      (f . (g . a)) = a & (f . (g . b)) = b by A1, Lm2;

      

      hence (g . ((1 / 2) * (a + b))) = (g . (f . ((1 / 2) * (((f /" ) . a) + ((f /" ) . b))))) by A2

      .= ((g * f) . ((1 / 2) * (((f /" ) . a) + ((f /" ) . b)))) by FUNCT_2: 15

      .= ((1 / 2) * ((g . a) + (g . b))) by A3;

    end;

    registration

      let E;

      let f be bijective midpoints-preserving UnOp of E;

      cluster (f /" ) -> midpoints-preserving;

      coherence by Th14;

    end

    theorem :: MAZURULM:15

    

     Th15: f is Affine & g is Affine implies (g * f) is Affine

    proof

      assume that

       A1: f is Affine and

       A2: g is Affine;

      set h = (g * f);

      let a, b, t such that

       A3: 0 <= t & t <= 1;

      

       A4: (h . a) = (g . (f . a)) & (h . b) = (g . (f . b)) by FUNCT_2: 15;

      

      thus (h . (((1 - t) * a) + (t * b))) = (g . (f . (((1 - t) * a) + (t * b)))) by FUNCT_2: 15

      .= (g . (((1 - t) * (f . a)) + (t * (f . b)))) by A1, A3

      .= (((1 - t) * (h . a)) + (t * (h . b))) by A2, A3, A4;

    end;

    registration

      let E;

      let f,g be Affine UnOp of E;

      cluster (g * f) -> Affine;

      coherence by Th15;

    end

    theorem :: MAZURULM:16

    

     Th16: f is bijective Affine implies (f /" ) is Affine

    proof

      assume that

       A1: f is bijective and

       A2: f is Affine;

      set g = (f /" );

      let a,b be Point of F;

      let t such that

       A3: 0 <= t & t <= 1;

      

       A4: (g * f) = ( id E) by A1, Lm3;

      (f . (g . a)) = a & (f . (g . b)) = b by A1, Lm2;

      

      hence (g . (((1 - t) * a) + (t * b))) = (g . (f . (((1 - t) * (g . a)) + (t * (g . b))))) by A3, A2

      .= ((g * f) . (((1 - t) * (g . a)) + (t * (g . b)))) by FUNCT_2: 15

      .= (((1 - t) * (g . a)) + (t * (g . b))) by A4;

    end;

    registration

      let E;

      let f be bijective Affine UnOp of E;

      cluster (f /" ) -> Affine;

      coherence by Th16;

    end

    definition

      let E be non empty RLSStruct, a be Point of E;

      :: MAZURULM:def4

      func a -reflection -> UnOp of E means

      : Def4: for b be Point of E holds (it . b) = ((2 * a) - b);

      existence

      proof

        deffunc F( Point of E) = ((2 * a) - $1);

        ex f be UnOp of E st for x be Point of E holds (f . x) = F(x) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be UnOp of E such that

         A1: for b be Point of E holds (f1 . b) = ((2 * a) - b) and

         A2: for b be Point of E holds (f2 . b) = ((2 * a) - b);

        let b be Point of E;

        

        thus (f1 . b) = ((2 * a) - b) by A1

        .= (f2 . b) by A2;

      end;

    end

    theorem :: MAZURULM:17

    

     Th17: ((a -reflection ) * (a -reflection )) = ( id E)

    proof

      set R = (a -reflection );

      let b;

      

      thus ((R * R) . b) = (R . (R . b)) by FUNCT_2: 15

      .= ((2 * a) - (R . b)) by Def4

      .= ((2 * a) - ((2 * a) - b)) by Def4

      .= (((2 * a) - (2 * a)) + b) by RLVECT_1: 29

      .= (( 0. E) + b) by RLVECT_1: 5

      .= b

      .= (( id E) . b);

    end;

    registration

      let E, a;

      cluster (a -reflection ) -> bijective;

      coherence

      proof

        set R = (a -reflection );

        (R * R) = ( id E) by Th17;

        hence R is one-to-one onto by FUNCT_2: 23;

      end;

    end

    theorem :: MAZURULM:18

    

     Th18: ((a -reflection ) . a) = a & for b st ((a -reflection ) . b) = b holds a = b

    proof

      set R = (a -reflection );

      

      thus (R . a) = ((2 * a) - a) by Def4

      .= ((a + a) - a) by Th3

      .= (a + (a - a)) by RLVECT_1: 28

      .= (a + ( 0. E)) by RLVECT_1: 15

      .= a;

      let b;

      assume (R . b) = b;

      then

       A1: ((R . b) + b) = (2 * b) by Th3;

      (R . b) = ((2 * a) - b) by Def4;

      

      then ((R . b) + b) = ((2 * a) - (b - b)) by RLVECT_1: 29

      .= ((2 * a) - ( 0. E)) by RLVECT_1: 15

      .= (2 * a);

      hence thesis by A1, RLVECT_1: 36;

    end;

    theorem :: MAZURULM:19

    

     Th19: (((a -reflection ) . b) - a) = (a - b)

    proof

      set R = (a -reflection );

      

       A1: (1 * a) = a by RLVECT_1:def 8;

      (R . b) = ((2 * a) - b) by Def4;

      

      hence ((R . b) - a) = (((2 * a) - a) - b) by VECTSP_1: 34

      .= (((2 - 1) * a) - b) by A1, RLVECT_1: 35

      .= (a - b) by RLVECT_1:def 8;

    end;

    theorem :: MAZURULM:20

    

     Th20: ||.(((a -reflection ) . b) - a).|| = ||.(b - a).||

    proof

      (((a -reflection ) . b) - a) = (a - b) by Th19;

      hence thesis by NORMSP_1: 7;

    end;

    theorem :: MAZURULM:21

    

     Th21: (((a -reflection ) . b) - b) = (2 * (a - b))

    proof

      (((2 * a) - b) - b) = ((2 * a) - (b + b)) by RLVECT_1: 27

      .= ((2 * a) - (2 * b)) by Th3

      .= (2 * (a - b)) by RLVECT_1: 34;

      hence thesis by Def4;

    end;

    theorem :: MAZURULM:22

    

     Th22: ||.(((a -reflection ) . b) - b).|| = (2 * ||.(b - a).||)

    proof

      

       A1: (((a -reflection ) . b) - b) = (2 * (a - b)) by Th21;

      

       A2: |.2.| = 2 by COMPLEX1: 43;

       ||.(a - b).|| = ||.(b - a).|| by NORMSP_1: 7;

      hence thesis by A1, A2, NORMSP_1:def 1;

    end;

    theorem :: MAZURULM:23

    

     Th23: ((a -reflection ) /" ) = (a -reflection )

    proof

      set R = (a -reflection );

      

       A1: ( rng R) = ( [#] E) by FUNCT_2:def 3;

      

       A2: (R /" ) = (R qua Function " ) by TOPS_2:def 4;

      (R * R) = ( id E) by Th17;

      hence thesis by A1, A2, FUNCT_2: 30;

    end;

    registration

      let E, a;

      cluster (a -reflection ) -> isometric;

      coherence

      proof

        set R = (a -reflection );

        let b, c;

        (R . b) = ((2 * a) - b) & (R . c) = ((2 * a) - c) by Def4;

        

        then ((R . b) - (R . c)) = ((((2 * a) - b) - (2 * a)) + c) by RLVECT_1: 29

        .= ((((2 * a) - (2 * a)) - b) + c) by VECTSP_1: 34

        .= ((( 0. E) - b) + c) by RLVECT_1: 15

        .= (c - b);

        hence ||.((R . b) - (R . c)).|| = ||.(b - c).|| by NORMSP_1: 7;

      end;

    end

    deffunc W( RealNormSpace, Point of $1, Point of $1) = { g where g be UnOp of $1 : g is bijective isometric & (g . $2) = $2 & (g . $3) = $3 };

    deffunc l( RealNormSpace, Point of $1, Point of $1) = { ||.((g . ((1 / 2) * ($2 + $3))) - ((1 / 2) * ($2 + $3))).|| where g be UnOp of $1 : g in W($1,$2,$3) };

     Lm4:

    now

      let E, a, b;

      let l be real-membered set such that

       A1: l = l(E,a,b);

      set z = ((1 / 2) * (a + b));

      thus (2 * ||.(a - z).||) is UpperBound of l

      proof

        let x be ExtReal;

        assume x in l;

        then

        consider g1 be UnOp of E such that

         A2: x = ||.((g1 . z) - z).|| and

         A3: g1 in W(E,a,b) by A1;

        consider g be UnOp of E such that

         A4: g1 = g and g is bijective and

         A5: g is isometric and

         A6: (g . a) = a and (g . b) = b by A3;

        

         A7: ||.((g . z) - a).|| = ||.(z - a).|| by A5, A6

        .= ||.(a - z).|| by NORMSP_1: 7;

         ||.((g . z) - z).|| <= ( ||.((g . z) - a).|| + ||.(a - z).||) by NORMSP_1: 10;

        hence thesis by A2, A4, A7;

      end;

    end;

     Lm5:

    now

      let E, a, b;

      let h be UnOp of E such that

       A1: h in W(E,a,b);

      set z = ((1 / 2) * (a + b));

      set R = (z -reflection );

      set gs = (((R * (h /" )) * R) * h);

      consider g be UnOp of E such that

       A2: g = h and

       A3: g is bijective and

       A4: g is isometric and

       A5: (g . a) = a and

       A6: (g . b) = b by A1;

      

       A7: (g /" ) = (g qua Function " ) by A3, TOPS_2:def 4;

      then

       A8: (g /" ) is bijective by A3, GROUP_6: 63;

      

       A9: (2 * z) = ((2 * (1 / 2)) * (a + b)) by RLVECT_1:def 7

      .= (a + b) by RLVECT_1:def 8;

      then

       A10: ((2 * z) - a) = b by Th4;

      

       A11: ((2 * z) - b) = a by A9, Th4;

      

       A12: ( dom g) = ( [#] E) by FUNCT_2:def 1;

      

       A13: ((g /" ) . b) = b by A7, A6, A3, A12, FUNCT_1: 32;

      

       A14: ((g /" ) . a) = a by A7, A5, A3, A12, FUNCT_1: 32;

      

       A15: (gs . a) = (((R * (g /" )) * R) . a) by A5, A2, FUNCT_2: 15

      .= ((R * (g /" )) . (R . a)) by FUNCT_2: 15

      .= ((R * (g /" )) . b) by A10, Def4

      .= (R . ((g /" ) . b)) by FUNCT_2: 15

      .= ((2 * z) - b) by A13, Def4

      .= a by A9, Th4;

      (gs . b) = (((R * (g /" )) * R) . b) by A6, A2, FUNCT_2: 15

      .= ((R * (g /" )) . (R . b)) by FUNCT_2: 15

      .= ((R * (g /" )) . a) by A11, Def4

      .= (R . ((g /" ) . a)) by FUNCT_2: 15

      .= ((2 * z) - a) by A14, Def4

      .= b by A9, Th4;

      hence gs in W(E,a,b) by A2, A3, A4, A8, A15;

    end;

     Lm6:

    now

      let E, a, b;

      let l be non empty bounded_above Subset of REAL such that

       A1: l = l(E,a,b);

      thus ( sup l) is UpperBound of (2 ** l)

      proof

        set z = ((1 / 2) * (a + b));

        set R = (z -reflection );

        let x be ExtReal;

        assume x in (2 ** l);

        then

        consider w be Element of ExtREAL such that

         A2: x = (2 * w) and

         A3: w in l by MEMBER_1: 188;

        consider h be UnOp of E such that

         A4: w = ||.((h . z) - z).|| and

         A5: h in W(E,a,b) by A3, A1;

        consider g be UnOp of E such that

         A6: g = h and

         A7: g is bijective and

         A8: g is isometric and (g . a) = a & (g . b) = b by A5;

        

         A9: (R * ((g /" ) * (R * g))) = ((R * (g /" )) * (R * g)) by RELAT_1: 36

        .= (((R * (g /" )) * R) * g) by RELAT_1: 36;

        

         A10: (R . ((g /" ) . (R . (g . z)))) = (R . ((g /" ) . ((R * g) . z))) by FUNCT_2: 15

        .= (R . (((g /" ) * (R * g)) . z)) by FUNCT_2: 15

        .= ((R * ((g /" ) * (R * g))) . z) by FUNCT_2: 15;

        

         A11: (g /" ) = (g qua Function " ) by A7, TOPS_2:def 4;

        (((R * (g /" )) * R) * g) in W(E,a,b) by A5, A6, Lm5;

        then

         A12: ||.(((((R * (g /" )) * R) * g) . z) - z).|| in l by A1;

        reconsider d = 2 as R_eal by XXREAL_0:def 1;

        

         A13: ((g /" ) . (g . z)) = z by A7, A11, FUNCT_2: 26;

        (2 * ||.((g . z) - z).||) = ||.((R . (g . z)) - (g . z)).|| by Th22

        .= ||.(((g /" ) . (R . (g . z))) - ((g /" ) . (g . z))).|| by A7, A8, Def1

        .= ||.((R . ((g /" ) . (R . (g . z)))) - z).|| by A13, Th20;

        hence x <= ( sup l) by A2, A4, A9, A10, A12, A6, XXREAL_2: 4;

      end;

    end;

     Lm7:

    now

      let E, a, b;

      let l be real-membered set such that

       A1: l = l(E,a,b);

      let g be UnOp of E such that

       A2: g in W(E,a,b);

      set z = ((1 / 2) * (a + b));

      set R = (z -reflection );

      

       A3: l c= REAL by XREAL_0:def 1;

      (( id E) . a) = a & (( id E) . b) = b;

      then ( id E) in W(E,a,b);

      then

       A4: ||.((( id E) . z) - z).|| in l by A1;

      (2 * ||.(a - z).||) is UpperBound of l by A1, Lm4;

      then

      reconsider A = l as non empty bounded_above Subset of REAL by A3, A4, XXREAL_2:def 10;

      set lambda = ( sup A);

      reconsider d = 2 as R_eal by XXREAL_0:def 1;

      

       A5: (d * ( sup A)) = ( sup (2 ** A)) by URYSOHN2: 18;

      

       A6: ||.((g . z) - z).|| in A by A1, A2;

      lambda is UpperBound of (2 ** A) by A1, Lm6;

      then ( sup (2 ** A)) <= lambda by XXREAL_2:def 3;

      then ((2 * lambda) - lambda) <= (lambda - lambda) by A5, XREAL_1: 9;

      then ||.((g . z) - z).|| = 0 by A6, XXREAL_2: 4;

      hence (g . z) = z by NORMSP_1: 6;

    end;

    theorem :: MAZURULM:24

    

     Th24: f is isometric implies f is_continuous_on ( dom f)

    proof

      assume

       A1: f is isometric;

      set X = ( dom f);

      for s1 be sequence of E st ( rng s1) c= X & s1 is convergent & ( lim s1) in X holds (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1))

      proof

        let s1 be sequence of E;

        assume that

         A2: ( rng s1) c= X and

         A3: s1 is convergent and ( lim s1) in X;

        consider a such that

         A4: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((s1 . n) - a).|| < r by A3;

        

         A5: a = ( lim s1) by A3, A4, NORMSP_1:def 7;

        

         A6: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.(((f /* s1) . n) - (f . a)).|| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           A7: for n be Nat st m <= n holds ||.((s1 . n) - a).|| < r by A4;

          take m;

          let n be Nat;

          

           A8: n in NAT by ORDINAL1:def 12;

          assume m <= n;

          then

           A9: ||.((s1 . n) - a).|| < r by A7;

          

           A10: ||.((f . (s1 . n)) - (f . a)).|| = ||.((s1 . n) - a).|| by A1;

          (f /* s1) = (f * s1) by A2, FUNCT_2:def 11;

          hence ||.(((f /* s1) . n) - (f . a)).|| < r by A9, A10, FUNCT_2: 15, A8;

        end;

        thus (f /* s1) is convergent by A6;

        hence (f /. ( lim s1)) = ( lim (f /* s1)) by A5, A6, NORMSP_1:def 7;

      end;

      hence thesis by NFCONT_1: 18;

    end;

    

     Lm8: (((1 - t) * a) + (t * b)) = (a + (t * (b - a)))

    proof

      

      thus (((1 - t) * a) + (t * b)) = (((1 * a) - (t * a)) + (t * b)) by RLVECT_1: 35

      .= ((a - (t * a)) + (t * b)) by RLVECT_1:def 8

      .= ((a + (t * b)) - (t * a)) by RLVECT_1:def 3

      .= (a + ((t * b) - (t * a))) by RLVECT_1: 28

      .= (a + (t * (b - a))) by RLVECT_1: 34;

    end;

     Lm9:

    now

      let E, F, f, a, b;

      let n,j be Nat;

      set m = (2 |^ (n + 1 qua Complex) qua Nat);

      set k = (2 |^ n);

      set x = (k - j);

      assume

       A1: f is midpoints-preserving;

      assume j <= k;

      then x in NAT by INT_1: 5;

      then

      reconsider x as Nat;

      take x;

      thus x = (k - j);

      set z = ((1 - (j / m)) - (1 / 2));

      

       A2: k <> 0 by NEWTON: 83;

      

       A3: (2 * k) = m by NEWTON: 6;

      

       A4: ((1 / 2) * (1 / k)) = (1 / (2 * k)) by XCMPLX_1: 102;

      (x / m) = (((1 * k) / m) - (j / m))

      .= ((1 / 2) - (j / m)) by A2, A3, XCMPLX_1: 91

      .= z;

      

      then

       A5: ((z * a) + ((j / m) * b)) = (((1 / m) * (x * a)) + (((1 / m) * j) * b)) by RLVECT_1:def 7

      .= (((1 / m) * (x * a)) + ((1 / m) * (j * b))) by RLVECT_1:def 7

      .= ((1 / m) * ((x * a) + (j * b))) by RLVECT_1:def 5

      .= ((1 / 2) * ((1 / k) * ((x * a) + (j * b)))) by A4, A3, RLVECT_1:def 7;

      (a + ((j / m) * (b - a))) = (a + (((j / m) * b) - ((j / m) * a))) by RLVECT_1: 34

      .= ((a + ((j / m) * b)) - ((j / m) * a)) by RLVECT_1:def 3

      .= ((a - ((j / m) * a)) + ((j / m) * b)) by RLVECT_1:def 3

      .= (((1 * a) - ((j / m) * a)) + ((j / m) * b)) by RLVECT_1:def 8

      .= (((1 - (j / m)) * a) + ((j / m) * b)) by RLVECT_1: 35

      .= (((((1 - (j / m)) * a) + (z * a)) - (z * a)) + ((j / m) * b)) by Th4

      .= (((((1 - (j / m)) * a) - (z * a)) + (z * a)) + ((j / m) * b)) by RLVECT_1:def 3

      .= (((((1 - (j / m)) - z) * a) + (z * a)) + ((j / m) * b)) by RLVECT_1: 35

      .= (((1 / 2) * a) + ((z * a) + ((j / m) * b))) by RLVECT_1:def 3

      .= ((1 / 2) * (a + ((1 / k) * ((x * a) + (j * b))))) by A5, RLVECT_1:def 5;

      hence (f . (a + ((j / m) * (b - a)))) = ((1 / 2) * ((f . a) + (f . ((1 / k) * ((x * a) + (j * b)))))) by A1;

    end;

     Lm10:

    now

      let E, F, f, a, b;

      let n,j be Nat;

      set m = (2 |^ (n + 1 qua Complex) qua Nat);

      set k = (2 |^ n);

      set x = ((k + j) - m);

      assume

       A1: f is midpoints-preserving;

      

       A2: (2 * k) = m by NEWTON: 6;

      assume j >= k;

      then (k + k) <= (k + j) by XREAL_1: 6;

      then x in NAT by A2, INT_1: 5;

      then

      reconsider x as Nat;

      take x;

      thus x = ((k + j) - m);

      set z = ((j / m) - (1 / 2) qua Complex);

      

       A3: k <> 0 by NEWTON: 83;

      

       A4: m <> 0 by NEWTON: 83;

      

       A5: (m / m) = 1 by A4, XCMPLX_1: 60;

      

      then

       A6: (1 - (j / m)) = ((m / m) - (j / m))

      .= ((1 / m) * (m - j));

      

       A7: (k / m) = ((1 * k) / (2 * k)) by NEWTON: 6

      .= (1 / 2) by A3, XCMPLX_1: 91;

      

       A8: ((1 / 2) * (1 / k)) = (1 / (2 * k)) by XCMPLX_1: 102;

      (x / m) = (((k + j) / m) - (m / m))

      .= (((k / m) + (j / m)) - (m / m))

      .= z by A5, A7;

      

      then

       A9: ((z * b) + ((1 - (j / m)) * a)) = (((1 / m) * ((m - j) * a)) + (((1 / m) * x) * b)) by A6, RLVECT_1:def 7

      .= (((1 / m) * ((m - j) * a)) + ((1 / m) * (x * b))) by RLVECT_1:def 7

      .= ((1 / m) * (((m - j) * a) + (x * b))) by RLVECT_1:def 5

      .= ((1 / 2) * ((1 / k) * (((m - j) * a) + (x * b)))) by A8, A2, RLVECT_1:def 7;

      (a + ((j / m) * (b - a))) = (a + (((j / m) * b) - ((j / m) * a))) by RLVECT_1: 34

      .= ((a + ((j / m) * b)) - ((j / m) * a)) by RLVECT_1:def 3

      .= ((a - ((j / m) * a)) + ((j / m) * b)) by RLVECT_1:def 3

      .= (((1 * a) - ((j / m) * a)) + ((j / m) * b)) by RLVECT_1:def 8

      .= (((1 - (j / m)) * a) + ((j / m) * b)) by RLVECT_1: 35

      .= (((((j / m) * b) + (z * b)) - (z * b)) + ((1 - (j / m)) * a)) by Th4

      .= (((((j / m) * b) - (z * b)) + (z * b)) + ((1 - (j / m)) * a)) by RLVECT_1:def 3

      .= (((((j / m) - z) * b) + (z * b)) + ((1 - (j / m)) * a)) by RLVECT_1: 35

      .= (((1 / 2) * b) + ((z * b) + ((1 - (j / m)) * a))) by RLVECT_1:def 3

      .= ((1 / 2) * (b + ((1 / k) * (((m - j) * a) + (x * b))))) by A9, RLVECT_1:def 5;

      hence (f . (a + ((j / m) * (b - a)))) = ((1 / 2) * ((f . b) + (f . ((1 / k) * (((m - j) * a) + (x * b)))))) by A1;

    end;

     Lm11:

    now

      let E, F, f, a, b;

      let t be Nat;

      assume

       A1: f is midpoints-preserving;

      thus for n be Nat st t <= (2 |^ n) holds (f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b))) = (((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)))

      proof

        defpred P[ Nat] means for w be Nat st w <= (2 |^ $1) holds (f . (((1 - (w / (2 |^ $1))) * a) + ((w / (2 |^ $1)) * b))) = (((1 - (w / (2 |^ $1))) * (f . a)) + ((w / (2 |^ $1)) * (f . b)));

        

         A2: P[ 0 ]

        proof

          let t be Nat such that

           A3: t <= (2 |^ 0 );

          

           A4: (2 |^ 0 ) = 1 by NEWTON: 4;

          per cases by A3, A4, NAT_1: 25;

            suppose

             A5: t = 1;

            

            then (f . (((1 - t) * a) + (t * b))) = (f . (( 0. E) + (t * b))) by RLVECT_1: 10

            .= (f . (t * b))

            .= (f . b) by A5, RLVECT_1:def 8

            .= (t * (f . b)) by A5, RLVECT_1:def 8

            .= (( 0. F) + (t * (f . b)))

            .= (((1 - t) * (f . a)) + (t * (f . b))) by A5, RLVECT_1: 10;

            hence thesis by A4;

          end;

            suppose

             A6: t = 0 ;

            

            then (f . (((1 - t) * a) + (t * b))) = (f . ((1 * a) + ( 0. E))) by RLVECT_1: 10

            .= (f . (1 * a))

            .= (f . a) by RLVECT_1:def 8

            .= ((1 - t) * (f . a)) by A6, RLVECT_1:def 8

            .= (((1 - t) * (f . a)) + ( 0. F))

            .= (((1 - t) * (f . a)) + (t * (f . b))) by A6, RLVECT_1: 10;

            hence thesis by A4;

          end;

        end;

        

         A7: for n be Nat st P[n] holds P[(n + 1 qua Complex)]

        proof

          let n be Nat;

          set m = (2 |^ n), k = (2 |^ (n + 1 qua Complex));

          assume

           A8: P[n];

          let t be Nat such that

           A9: t <= k;

          

           A10: k = (m * 2) by NEWTON: 6;

          

           A11: m <> 0 by NEWTON: 83;

          

           A12: ((1 / 2) * (t / m)) = ((1 * t) / (2 * m)) by XCMPLX_1: 76

          .= (t / k) by NEWTON: 6;

          per cases ;

            suppose

             A13: t <= m;

            then

            consider x be Nat such that

             A14: x = (m - t) and

             A15: (f . (a + ((t / k) * (b - a)))) = ((1 / 2) * ((f . a) + (f . ((1 / m) * ((x * a) + (t * b)))))) by A1, Lm9;

            

             A16: (x / m) = ((m / m) - (t / m)) by A14

            .= (1 - (t / m)) by A11, XCMPLX_1: 60;

            

             A17: ((1 / m) * ((x * a) + (t * b))) = (((1 / m) * (x * a)) + ((1 / m) * (t * b))) by RLVECT_1:def 5

            .= (((1 / m) * (x * a)) + ((t / m) * b)) by RLVECT_1:def 7

            .= (((x / m) * a) + ((t / m) * b)) by RLVECT_1:def 7;

            

            thus (f . (((1 - (t / k)) * a) + ((t / k) * b))) = (f . (a + ((t / k) * (b - a)))) by Lm8

            .= (((1 / 2) * (f . a)) + ((1 / 2) * (f . ((1 / m) * ((x * a) + (t * b)))))) by A15, RLVECT_1:def 5

            .= (((1 / 2) * (f . a)) + ((1 / 2) * (((1 - (t / m)) * (f . a)) + ((t / m) * (f . b))))) by A16, A13, A17, A8

            .= (((1 / 2) * (f . a)) + (((1 / 2) * ((1 - (t / m)) * (f . a))) + ((1 / 2) * ((t / m) * (f . b))))) by RLVECT_1:def 5

            .= ((((1 / 2) * (f . a)) + ((1 / 2) * ((1 - (t / m)) * (f . a)))) + ((1 / 2) * ((t / m) * (f . b)))) by RLVECT_1:def 3

            .= ((((1 / 2) * (f . a)) + (((1 / 2) * (1 - (t / m))) * (f . a))) + ((1 / 2) * ((t / m) * (f . b)))) by RLVECT_1:def 7

            .= ((((1 / 2) + ((1 / 2) * (1 - (t / m)))) * (f . a)) + ((1 / 2) * ((t / m) * (f . b)))) by RLVECT_1:def 6

            .= (((1 - (t / k)) * (f . a)) + ((t / k) * (f . b))) by A12, RLVECT_1:def 7;

          end;

            suppose t >= m;

            then

            consider x be Nat such that

             A18: x = ((m + t) - k) and

             A19: (f . (a + ((t / k) * (b - a)))) = ((1 / 2) * ((f . b) + (f . ((1 / m) * (((k - t) * a) + (x * b)))))) by A1, Lm10;

            set w = (t - m);

            

             A20: w <= ((2 * m) - m) by A9, A10, XREAL_1: 9;

            

             A21: (m / m) = 1 by A11, XCMPLX_1: 60;

            

             A22: (k / m) = ((2 * m) / (1 * m)) by NEWTON: 6

            .= (2 / 1) by A11, XCMPLX_1: 91;

            

             A23: (1 - (t / m)) = ((m / m) - (t / m)) by A21

            .= ( - ((t / m) - (m / m)))

            .= ( - ((t - m) / m));

            

             A24: ((1 / m) * (k - t)) = ((k / m) - (t / m))

            .= ((1 + 1) - (t / m)) by A22

            .= (1 - ((t - m) / m)) by A23

            .= (1 - (w / m));

            ((1 / m) * x) = (w / m) by A18, A10;

            then ((((1 / m) * (k - t)) * a) + (((1 / m) * x) * b)) = (((1 - (w / m)) * a) + ((w / m) * b)) by A24;

            then

             A25: ((1 / 2) * (f . ((((1 / m) * (k - t)) * a) + (((1 / m) * x) * b)))) = ((1 / 2) * (((1 - (w / m)) * (f . a)) + ((w / m) * (f . b)))) by A20, A18, A10, A8;

            

             A26: ((1 / 2) * (1 - (w / m))) = ((1 / 2) * (1 - ((t / m) - (m / m))))

            .= (1 - ((1 / 2) * (t / m))) by A21

            .= (1 - ((1 * t) / (2 * m))) by XCMPLX_1: 76

            .= (1 - (t / k)) by NEWTON: 6;

            

            thus (f . (((1 - (t / k)) * a) + ((t / k) * b))) = (f . (a + ((t / k) * (b - a)))) by Lm8

            .= (((1 / 2) * (f . b)) + ((1 / 2) * (f . ((1 / m) * (((k - t) * a) + (x * b)))))) by A19, RLVECT_1:def 5

            .= (((1 / 2) * (f . b)) + ((1 / 2) * (f . (((1 / m) * ((k - t) * a)) + ((1 / m) * (x * b)))))) by RLVECT_1:def 5

            .= (((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / m) * (k - t)) * a) + ((1 / m) * (x * b)))))) by RLVECT_1:def 7

            .= (((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / m) * (k - t)) * a) + (((1 / m) * x) * b))))) by RLVECT_1:def 7

            .= (((1 / 2) * (f . b)) + ((1 / 2) * (((1 - (w / m)) * (f . a)) + ((w / m) * (f . b))))) by A25

            .= (((1 / 2) * (f . b)) + (((1 / 2) * ((1 - (w / m)) * (f . a))) + ((1 / 2) * ((w / m) * (f . b))))) by RLVECT_1:def 5

            .= (((1 / 2) * ((1 - (w / m)) * (f . a))) + (((1 / 2) * (f . b)) + ((1 / 2) * ((w / m) * (f . b))))) by RLVECT_1:def 3

            .= (((1 / 2) * ((1 - (w / m)) * (f . a))) + ((1 / 2) * ((f . b) + ((w / m) * (f . b))))) by RLVECT_1:def 5

            .= (((1 / 2) * ((1 - (w / m)) * (f . a))) + ((1 / 2) * ((1 * (f . b)) + ((w / m) * (f . b))))) by RLVECT_1:def 8

            .= (((1 / 2) * ((1 - (w / m)) * (f . a))) + ((1 / 2) * ((1 + (w / m)) * (f . b)))) by RLVECT_1:def 6

            .= (((1 / 2) * ((1 - (w / m)) * (f . a))) + (((1 / 2) * (1 + (w / m))) * (f . b))) by RLVECT_1:def 7

            .= (((1 - (t / k)) * (f . a)) + ((t / k) * (f . b))) by A26, RLVECT_1:def 7;

          end;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A2, A7);

        hence thesis;

      end;

    end;

    registration

      let E, F;

      cluster bijective isometric -> midpoints-preserving for Function of E, F;

      coherence

      proof

        let f be Function of E, F such that

         A1: f is bijective and

         A2: f is isometric;

        let a,b be Point of E;

        set W = W(E,a,b);

        set l = l(E,a,b);

        set z = ((1 / 2) * (a + b));

        set z1 = ((1 / 2) * ((f . a) + (f . b)));

        set R = (z -reflection );

        set R1 = (z1 -reflection );

        set h = (((R * (f /" )) * R1) * f);

        now

          let x be object;

          assume x in l;

          then ex g be UnOp of E st x = ||.((g . z) - z).|| & g in W(E,a,b);

          hence x is real;

        end;

        then

        reconsider l as real-membered set by MEMBERED:def 3;

        

         A3: ( rng f) = ( [#] F) by A1, FUNCT_2:def 3;

        

         A4: (f /" ) = (f qua Function " ) by A1, TOPS_2:def 4;

        then

         A5: (f /" ) is bijective by A1, GROUP_6: 63;

        (R * (f /" )) is onto by A5, FUNCT_2: 27;

        then ((R * (f /" )) * R1) is onto by FUNCT_2: 27;

        then

         A6: h is onto by A1, FUNCT_2: 27;

        (f /" ) is isometric by A1, A2, Th12;

        then (R * (f /" )) is isometric by Th11;

        then ((R * (f /" )) * R1) is isometric by Th11;

        then

         A7: h is isometric by A2, Th11;

        

         A8: (2 * z) = ((2 * (1 / 2)) * (a + b)) by RLVECT_1:def 7

        .= (a + b) by RLVECT_1:def 8;

        then

         A9: ((2 * z) - a) = b by Th4;

        

         A10: ((2 * z) - b) = a by A8, Th4;

        

         A11: (2 * z1) = ((2 * (1 / 2)) * ((f . a) + (f . b))) by RLVECT_1:def 7

        .= ((f . a) + (f . b)) by RLVECT_1:def 8;

        then

         A12: ((2 * z1) - (f . a)) = (f . b) by Th4;

        

         A13: ((2 * z1) - (f . b)) = (f . a) by A11, Th4;

        

         A14: (h . a) = (((R * (f /" )) * R1) . (f . a)) by FUNCT_2: 15

        .= ((R * (f /" )) . (R1 . (f . a))) by FUNCT_2: 15

        .= ((R * (f /" )) . (f . b)) by A12, Def4

        .= (R . ((f /" ) . (f . b))) by FUNCT_2: 15

        .= (R . b) by A4, A1, FUNCT_2: 26

        .= a by A10, Def4;

        (h . b) = (((R * (f /" )) * R1) . (f . b)) by FUNCT_2: 15

        .= ((R * (f /" )) . (R1 . (f . b))) by FUNCT_2: 15

        .= ((R * (f /" )) . (f . a)) by A13, Def4

        .= (R . ((f /" ) . (f . a))) by FUNCT_2: 15

        .= (R . a) by A4, A1, FUNCT_2: 26

        .= b by A9, Def4;

        then

         A15: h in W by A4, A1, A6, A7, A14;

        ( rng R) = ( [#] E) by FUNCT_2:def 3;

        

        then

         A16: ((R /" ) * R) = ( id ( dom R)) by TOPS_2: 52

        .= ( id E) by FUNCT_2:def 1;

        

         A17: (f * (f /" )) = ( id F) by A1, A3, TOPS_2: 52;

        

         A18: ((R /" ) * h) = ((R /" ) * ((R * (f /" )) * (R1 * f))) by RELAT_1: 36

        .= ((R /" ) * (R * ((f /" ) * (R1 * f)))) by RELAT_1: 36

        .= (((R /" ) * R) * ((f /" ) * (R1 * f))) by RELAT_1: 36

        .= ((((R /" ) * R) * (f /" )) * (R1 * f)) by RELAT_1: 36

        .= (((((R /" ) * R) * (f /" )) * R1) * f) by RELAT_1: 36

        .= (((f /" ) * R1) * f) by A16, FUNCT_2: 17;

        

         A19: (f * (((f /" ) * R1) * f)) = (f * ((f /" ) * (R1 * f))) by RELAT_1: 36

        .= ((f * (f /" )) * (R1 * f)) by RELAT_1: 36

        .= (R1 * f) by A17, FUNCT_2: 17;

        l = l(E,a,b);

        then (h . z) = z by A15, Lm7;

        then (((R /" ) * h) . z) = ((R /" ) . z) by FUNCT_2: 15;

        

        then

         A20: ((f * (((f /" ) * R1) * f)) . z) = (f . ((R /" ) . z)) by A18, FUNCT_2: 15

        .= ((f * (R /" )) . z) by FUNCT_2: 15;

        (R1 . (f . z)) = ((R1 * f) . z) by FUNCT_2: 15

        .= ((f * R) . z) by A20, A19, Th23

        .= (f . (R . z)) by FUNCT_2: 15

        .= (f . z) by Th18;

        hence thesis by Th18;

      end;

    end

    registration

      let E, F;

      cluster isometric midpoints-preserving -> Affine for Function of E, F;

      coherence

      proof

        let f such that

         A1: f is isometric and

         A2: f is midpoints-preserving;

        let a, b, t;

        assume 0 <= t & t <= 1;

        then t in [. 0 , 1.] by XXREAL_1: 1;

        then

        consider s be Real_Sequence such that

         A3: ( rng s) c= DYADIC and

         A4: s is convergent and

         A5: ( lim s) = t by Th2, MEASURE6: 64;

        

         A6: ( dom f) = the carrier of E by FUNCT_2:def 1;

        set stb = (s * b);

        set 1t = (1 + ( - s));

        set s1ta = (1t * a);

        set s1 = (s1ta + stb);

        set za = (1t * (f . a));

        set zb = (s * (f . b));

        

         A7: f is_continuous_on ( dom f) by A1, Th24;

        

         A8: ( - s) is convergent by A4;

        

         A9: s1 is convergent by A4, NORMSP_1: 19;

        

         A10: ( lim s1ta) = (( lim 1t) * a) by A8, Th10;

        

         A11: ( lim ( - s)) = ( - ( lim s)) by A4, SEQ_2: 10;

        

         A12: ( lim 1t) = (1 + ( lim ( - s))) by A8, Th7

        .= (1 - ( lim s)) by A11

        .= (1 - t) by A5;

        ( lim stb) = (( lim s) * b) by A4, Th10;

        then

         A13: ( lim s1) = (((1 - t) * a) + (t * b)) by A5, A10, A12, A4, NORMSP_1: 25;

        

         A14: ( lim za) = ((1 - t) * (f . a)) by A8, A12, Th10;

        

         A15: ( lim zb) = (t * (f . b)) by A4, A5, Th10;

        

         A16: (f /* s1) = (za + zb)

        proof

          let n be Element of NAT ;

          

           A17: (1t . n) = (1 + (( - s) . n)) by VALUED_1: 2

          .= (1 + ( - (s . n))) by VALUED_1: 8;

          ( dom s) = NAT by FUNCT_2:def 1;

          then (s . n) in ( rng s) by FUNCT_1: 3;

          then

          consider m be Nat such that

           A18: (s . n) in ( dyadic m) by A3, URYSOHN1:def 2;

          consider i be Nat such that

           A19: i <= (2 |^ m) & (s . n) = (i / (2 |^ m) qua Complex) by A18, URYSOHN1:def 1;

          reconsider t = i as Nat;

          

           A20: (f . (((1 - (t / (2 |^ m))) * a) + ((t / (2 |^ m)) * b))) = (((1 - (t / (2 |^ m))) * (f . a)) + ((t / (2 |^ m)) * (f . b))) by A19, Lm11, A2;

          ( rng s1) c= ( dom f) by A6;

          

          hence ((f /* s1) . n) = (f . (s1 . n)) by FUNCT_2: 108

          .= (f . ((s1ta . n) + (stb . n))) by NORMSP_1:def 2

          .= (f . (((1 - (s . n)) * a) + (stb . n))) by A17, NDIFF_1:def 3

          .= (f . (((1 - (s . n)) * a) + ((s . n) * b))) by NDIFF_1:def 3

          .= (((1 - (s . n)) * (f . a)) + ((s . n) * (f . b))) by A19, A20

          .= (((1t . n) * (f . a)) + (zb . n)) by A17, NDIFF_1:def 3

          .= ((za . n) + (zb . n)) by NDIFF_1:def 3

          .= ((za + zb) . n) by NORMSP_1:def 2;

        end;

        

         A21: ( rng s1) c= the carrier of E;

        

        thus (f . (((1 - t) * a) + (t * b))) = (f /. (((1 - t) * a) + (t * b)))

        .= ( lim (f /* s1)) by A6, A7, A21, A9, A13, NFCONT_1: 18

        .= (((1 - t) * (f . a)) + (t * (f . b))) by A14, A15, A4, A16, NORMSP_1: 25;

      end;

    end