ndiff_8.miz



    begin

    reserve S,T,W,Y for RealNormSpace;

    reserve f,f1,f2 for PartFunc of S, T;

    reserve Z for Subset of S;

    reserve i,n for Nat;

    theorem :: NDIFF_8:1

    

     LMNR0: for X,Y be RealNormSpace, x be Point of X, y be Point of Y, z be Point of [:X, Y:] st z = [x, y] holds ||.z.|| = ( sqrt (( ||.x.|| ^2 ) + ( ||.y.|| ^2 )))

    proof

      let X,Y be RealNormSpace, x be Point of X, y be Point of Y, z be Point of [:X, Y:];

      assume z = [x, y];

      then

      consider w be Element of ( REAL 2) such that

       A1: w = <* ||.x.||, ||.y.||*> & ||.z.|| = |.w.| by PRVECT_3: 18;

      w in (2 -tuples_on REAL );

      then

       A2: ex s be Element of ( REAL * ) st s = w & ( len s) = 2;

      (w . 1) = ||.x.|| & (w . 2) = ||.y.|| by A1, FINSEQ_1: 44;

      hence thesis by A1, A2, EUCLID_3: 22;

    end;

    theorem :: NDIFF_8:2

    

     LMNR1: for X,Y be RealNormSpace, x be Point of X, z be Point of [:X, Y:] st z = [x, ( 0. Y)] holds ||.z.|| = ||.x.||

    proof

      let X,Y be RealNormSpace, x be Point of X, z be Point of [:X, Y:];

      assume z = [x, ( 0. Y)];

      

      then ||.z.|| = ( sqrt (( ||.x.|| ^2 ) + ( ||.( 0. Y).|| ^2 ))) by LMNR0

      .= ( sqrt ( ||.x.|| ^2 ));

      hence ||.x.|| = ||.z.|| by SQUARE_1: 22;

    end;

    theorem :: NDIFF_8:3

    for X,Y be RealNormSpace, y be Point of Y, z be Point of [:X, Y:] st z = [( 0. X), y] holds ||.z.|| = ||.y.||

    proof

      let X,Y be RealNormSpace, y be Point of Y, z be Point of [:X, Y:];

      assume z = [( 0. X), y];

      

      then ||.z.|| = ( sqrt (( ||.( 0. X).|| ^2 ) + ( ||.y.|| ^2 ))) by LMNR0

      .= ( sqrt ( ||.y.|| ^2 ));

      hence ||.y.|| = ||.z.|| by SQUARE_1: 22;

    end;

    theorem :: NDIFF_8:4

    for X,Y,Z,W be RealNormSpace holds for f be Lipschitzian LinearOperator of Z, W, g be Lipschitzian LinearOperator of Y, Z, h be Lipschitzian LinearOperator of X, Y holds (f * (g * h)) = ((f * g) * h) by RELAT_1: 36;

    theorem :: NDIFF_8:5

    

     LPB2Th4: for X,Y,Z be RealNormSpace holds for g be Lipschitzian LinearOperator of X, Y, f be Lipschitzian LinearOperator of Y, Z, h be Lipschitzian LinearOperator of X, Z holds h = (f * g) iff for x be VECTOR of X holds (h . x) = (f . (g . x))

    proof

      let X,Y,Z be RealNormSpace;

      let g be Lipschitzian LinearOperator of X, Y, f be Lipschitzian LinearOperator of Y, Z, h be Lipschitzian LinearOperator of X, Z;

      now

        assume

         A1: for x be VECTOR of X holds (h . x) = (f . (g . x));

        now

          let x be VECTOR of X;

          

          thus ((f * g) . x) = (f . (g . x)) by FUNCT_2: 15

          .= (h . x) by A1;

        end;

        hence h = (f * g) by FUNCT_2: 63;

      end;

      hence thesis by FUNCT_2: 15;

    end;

    theorem :: NDIFF_8:6

    

     LPB2Th6: for X,Y be RealNormSpace holds for f be Lipschitzian LinearOperator of X, Y holds (f * ( id the carrier of X)) = f & (( id the carrier of Y) * f) = f

    proof

      let X,Y be RealNormSpace;

      reconsider ii = ( id the carrier of X) as Lipschitzian LinearOperator of X, X by LOPBAN_2: 3;

      reconsider jj = ( id the carrier of Y) as Lipschitzian LinearOperator of Y, Y by LOPBAN_2: 3;

      let f be Lipschitzian LinearOperator of X, Y;

       A1:

      now

        let x be VECTOR of X;

        

        thus ((( id the carrier of Y) * f) . x) = (jj . (f . x)) by FUNCT_2: 15

        .= (f . x);

      end;

      now

        let x be VECTOR of X;

        

        thus ((f * ( id the carrier of X)) . x) = (f . (ii . x)) by FUNCT_2: 15

        .= (f . x);

      end;

      hence thesis by A1, FUNCT_2: 63;

    end;

    theorem :: NDIFF_8:7

    for X,Y,Z,W be RealNormSpace holds for f be Element of ( BoundedLinearOperators (Z,W)), g be Element of ( BoundedLinearOperators (Y,Z)), h be Element of ( BoundedLinearOperators (X,Y)) holds (f * (g * h)) = ((f * g) * h)

    proof

      let X,Y,Z,W be RealNormSpace;

      let f be Element of ( BoundedLinearOperators (Z,W)), g be Element of ( BoundedLinearOperators (Y,Z)), h be Element of ( BoundedLinearOperators (X,Y));

      ( modetrans ((g * h),X,Z)) = (( modetrans (g,Y,Z)) * ( modetrans (h,X,Y))) by LOPBAN_1:def 11;

      then (( modetrans (f,Z,W)) * ( modetrans ((g * h),X,Z))) = ((( modetrans (f,Z,W)) * ( modetrans (g,Y,Z))) * ( modetrans (h,X,Y))) by RELAT_1: 36;

      hence thesis by LOPBAN_1:def 11;

    end;

    theorem :: NDIFF_8:8

    for X,Y be RealNormSpace holds for f be Element of ( BoundedLinearOperators (X,Y)) holds (f * ( FuncUnit X)) = f & (( FuncUnit Y) * f) = f

    proof

      let X,Y be RealNormSpace;

      let f be Element of ( BoundedLinearOperators (X,Y));

      ( id the carrier of X) is Lipschitzian LinearOperator of X, X by LOPBAN_2: 3;

      then ( id the carrier of X) is Element of ( BoundedLinearOperators (X,X)) by LOPBAN_1:def 9;

      then ( modetrans (( id the carrier of X),X,X)) = ( id the carrier of X) by LOPBAN_1:def 11;

      

      hence (f * ( FuncUnit X)) = ( modetrans (f,X,Y)) by LPB2Th6

      .= f by LOPBAN_1:def 11;

      ( id the carrier of Y) is Lipschitzian LinearOperator of Y, Y by LOPBAN_2: 3;

      then ( id the carrier of Y) is Element of ( BoundedLinearOperators (Y,Y)) by LOPBAN_1:def 9;

      then ( modetrans (( id the carrier of Y),Y,Y)) = ( id the carrier of Y) by LOPBAN_1:def 11;

      

      hence (( FuncUnit Y) * f) = ( modetrans (f,X,Y)) by LPB2Th6

      .= f by LOPBAN_1:def 11;

    end;

    theorem :: NDIFF_8:9

    

     LPB2Th9: for X,Y,Z be RealNormSpace holds for f be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), g,h be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (f * (g + h)) = ((f * g) + (f * h))

    proof

      let X,Y,Z be RealNormSpace;

      let f be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), g,h be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      set BLOPXY = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      set BLOPXZ = ( R_NormSpace_of_BoundedLinearOperators (X,Z));

      set mf = ( modetrans (f,Y,Z));

      set mg = ( modetrans (g,X,Y));

      set mh = ( modetrans (h,X,Y));

      set mgh = ( modetrans ((g + h),X,Y));

      

       A1: (mf * mh) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider fh = (mf * mh) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      

       A2: (mf * mg) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider fg = (mf * mg) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      

       A3: (mf * mgh) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider k = (mf * mgh) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      reconsider hh = h as VECTOR of BLOPXY;

      reconsider gg = g as VECTOR of BLOPXY;

      

       A4: gg = mg & hh = mh by LOPBAN_1:def 11;

      for x be VECTOR of X holds ((mf * mgh) . x) = (((mf * mg) . x) + ((mf * mh) . x))

      proof

        let x be VECTOR of X;

        (g + h) = (gg + hh) & ( modetrans ((g + h),X,Y)) = (g + h) by LOPBAN_1:def 11;

        then

         A5: (mgh . x) = ((mg . x) + (mh . x)) by A4, LOPBAN_1: 35;

        

        thus ((mf * mgh) . x) = (mf . (mgh . x)) by A3, LPB2Th4

        .= ((mf . (mg . x)) + (mf . (mh . x))) by A5, VECTSP_1:def 20

        .= (((mf * mg) . x) + (mf . (mh . x))) by A2, LPB2Th4

        .= (((mf * mg) . x) + ((mf * mh) . x)) by A1, LPB2Th4;

      end;

      hence thesis by LOPBAN_1: 35;

    end;

    theorem :: NDIFF_8:10

    for X,Y,Z be RealNormSpace holds for f be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), g,h be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds ((g + h) * f) = ((g * f) + (h * f))

    proof

      let X,Y,Z be RealNormSpace;

      let f be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), g,h be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      set BLOPXY = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      set BLOPXZ = ( R_NormSpace_of_BoundedLinearOperators (X,Z));

      set BLOPYZ = ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      set mf = ( modetrans (f,X,Y));

      set mg = ( modetrans (g,Y,Z));

      set mh = ( modetrans (h,Y,Z));

      set mgh = ( modetrans ((g + h),Y,Z));

      

       A1: (mh * mf) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider hf = (mh * mf) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      

       A2: (mg * mf) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider gf = (mg * mf) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      

       A3: (mgh * mf) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider k = (mgh * mf) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      reconsider hh = h as VECTOR of BLOPYZ;

      reconsider gg = g as VECTOR of BLOPYZ;

      

       A4: gg = mg & hh = mh by LOPBAN_1:def 11;

      for x be VECTOR of X holds ((mgh * mf) . x) = (((mg * mf) . x) + ((mh * mf) . x))

      proof

        let x be VECTOR of X;

        (g + h) = (gg + hh) & ( modetrans ((g + h),Y,Z)) = (g + h) by LOPBAN_1:def 11;

        then

         A5: (mgh . (mf . x)) = ((mg . (mf . x)) + (mh . (mf . x))) by A4, LOPBAN_1: 35;

        

        thus ((mgh * mf) . x) = (mgh . (mf . x)) by A3, LPB2Th4

        .= (((mg * mf) . x) + (mh . (mf . x))) by A2, A5, LPB2Th4

        .= (((mg * mf) . x) + ((mh * mf) . x)) by A1, LPB2Th4;

      end;

      hence thesis by LOPBAN_1: 35;

    end;

    theorem :: NDIFF_8:11

    

     LPB2Th11: for X,Y,Z be RealNormSpace holds for f be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), g be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds for a,b be Real holds ((a * b) * (f * g)) = ((a * f) * (b * g))

    proof

      let X,Y,Z be RealNormSpace;

      let f be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), g be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      let a,b be Real;

      set BLOPXY = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      set BLOPXZ = ( R_NormSpace_of_BoundedLinearOperators (X,Z));

      set BLOPYZ = ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      set mf = ( modetrans (f,Y,Z));

      set mg = ( modetrans (g,X,Y));

      set maf = ( modetrans ((a * f),Y,Z));

      set mbg = ( modetrans ((b * g),X,Y));

      

       A1: (maf * mbg) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider k = (maf * mbg) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      

       A2: (mf * mg) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      then

      reconsider fg = (mf * mg) as VECTOR of BLOPXZ by LOPBAN_1:def 9;

      reconsider ff = f as VECTOR of BLOPYZ;

      reconsider gg = g as VECTOR of BLOPXY;

      

       A3: gg = mg by LOPBAN_1:def 11;

      

       A4: ff = mf by LOPBAN_1:def 11;

      for x be VECTOR of X holds ((maf * mbg) . x) = ((a * b) * ((mf * mg) . x))

      proof

        let x be VECTOR of X;

        set y = (b * (mg . x));

        (a * f) = (a * ff) & ( modetrans ((a * f),Y,Z)) = (a * f) by LOPBAN_1:def 11;

        then

         A5: (maf . y) = (a * (mf . y)) by A4, LOPBAN_1: 36;

        (b * g) = (b * gg) & ( modetrans ((b * g),X,Y)) = (b * g) by LOPBAN_1:def 11;

        then

         A6: (mbg . x) = (b * (mg . x)) by A3, LOPBAN_1: 36;

        

        thus ((maf * mbg) . x) = (maf . (mbg . x)) by A1, LPB2Th4

        .= (a * (b * (mf . (mg . x)))) by A5, A6, LOPBAN_1:def 5

        .= ((a * b) * (mf . (mg . x))) by RLVECT_1:def 7

        .= ((a * b) * ((mf * mg) . x)) by A2, LPB2Th4;

      end;

      hence thesis by LOPBAN_1: 36;

    end;

    theorem :: NDIFF_8:12

    for X,Y,Z be RealNormSpace holds for f be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), g be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds for a be Real holds (a * (f * g)) = ((a * f) * g)

    proof

      let X,Y,Z be RealNormSpace;

      let f be Element of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), g be Element of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      let a be Real;

      reconsider jj = 1 as Real;

      (a * (f * g)) = ((a * jj) * (f * g))

      .= ((a * f) * (jj * g)) by LPB2Th11;

      hence thesis by RLVECT_1:def 8;

    end;

    begin

    definition

      let M be RealNormSpace, p be Element of M, r be Real;

      :: NDIFF_8:def1

      func cl_Ball (p,r) -> Subset of M equals { q where q be Element of M : ||.(p - q).|| <= r };

      correctness

      proof

        defpred P[ Element of M] means ||.(p - $1).|| <= r;

        set X = { q where q be Element of M : P[q] };

        X c= the carrier of M from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: NDIFF_8:13

    

     LMBALL2: for p be Element of S, r be Real st 0 < r holds p in ( Ball (p,r)) & p in ( cl_Ball (p,r))

    proof

      let p be Element of S, r be Real;

      assume

       A1: 0 < r;

      

       A2: ||.(p - p).|| = ||.( 0. S).|| by RLVECT_1: 15

      .= 0 ;

      hence p in ( Ball (p,r)) by A1;

      thus p in ( cl_Ball (p,r)) by A1, A2;

    end;

    theorem :: NDIFF_8:14

    for p be Element of S, r be Real st 0 < r holds ( Ball (p,r)) <> {} & ( cl_Ball (p,r)) <> {} by LMBALL2;

    theorem :: NDIFF_8:15

    

     LMBALL1: for M be RealNormSpace, p be Element of M, r1,r2 be Real st r1 <= r2 holds ( cl_Ball (p,r1)) c= ( cl_Ball (p,r2)) & ( Ball (p,r1)) c= ( cl_Ball (p,r2)) & ( Ball (p,r1)) c= ( Ball (p,r2))

    proof

      let M be RealNormSpace, p be Element of M, r1,r2 be Real;

      assume

       A1: r1 <= r2;

      thus ( cl_Ball (p,r1)) c= ( cl_Ball (p,r2))

      proof

        let x be object;

        assume

         A2: x in ( cl_Ball (p,r1));

        then

        reconsider y = x as Point of M;

        ex q be Element of M st y = q & ||.(p - q).|| <= r1 by A2;

        then ||.(p - y).|| <= r2 by A1, XXREAL_0: 2;

        hence x in ( cl_Ball (p,r2));

      end;

      thus ( Ball (p,r1)) c= ( cl_Ball (p,r2))

      proof

        let x be object;

        assume

         A3: x in ( Ball (p,r1));

        then

        reconsider y = x as Point of M;

        ex q be Element of M st y = q & ||.(p - q).|| < r1 by A3;

        then ||.(p - y).|| <= r2 by A1, XXREAL_0: 2;

        hence x in ( cl_Ball (p,r2));

      end;

      let x be object;

      assume

       A4: x in ( Ball (p,r1));

      then

      reconsider y = x as Point of M;

      ex q be Element of M st y = q & ||.(p - q).|| < r1 by A4;

      then ||.(p - y).|| < r2 by A1, XXREAL_0: 2;

      hence x in ( Ball (p,r2));

    end;

    theorem :: NDIFF_8:16

    

     LMBALL1X: for M be RealNormSpace, p be Element of M, r1,r2 be Real st r1 < r2 holds ( cl_Ball (p,r1)) c= ( Ball (p,r2))

    proof

      let M be RealNormSpace, p be Element of M, r1,r2 be Real;

      assume

       A1: r1 < r2;

      assume not ( cl_Ball (p,r1)) c= ( Ball (p,r2));

      then

      consider x be object such that

       A2: x in ( cl_Ball (p,r1)) & not x in ( Ball (p,r2)) by TARSKI:def 3;

      reconsider x as Point of M by A2;

      

       A3: ex q be Element of M st x = q & ||.(p - q).|| <= r1 by A2;

      r2 <= ||.(p - x).|| by A2;

      hence contradiction by A1, A3, XXREAL_0: 2;

    end;

    theorem :: NDIFF_8:17

    

     LMBALL: for p be Element of S, r be Real holds ( Ball (p,r)) = { y where y be Point of S : ||.(y - p).|| < r }

    proof

      let p be Element of S, r be Real;

      deffunc F( object) = $1;

      defpred P1[ Element of S] means ||.(p - $1).|| < r;

      defpred P2[ Element of S] means ||.($1 - p).|| < r;

      

       A1: for v be Element of the carrier of S holds ( P1[v] iff P2[v]) by NORMSP_1: 7;

      { F(y) where y be Element of the carrier of S : P1[y] } = { F(y) where y be Element of the carrier of S : P2[y] } from FRAENKEL:sch 3( A1);

      hence thesis;

    end;

    theorem :: NDIFF_8:18

    for p be Element of S, r be Real holds ( cl_Ball (p,r)) = { y where y be Point of S : ||.(y - p).|| <= r }

    proof

      let p be Element of S, r be Real;

      deffunc F( object) = $1;

      defpred P1[ Element of S] means ||.(p - $1).|| <= r;

      defpred P2[ Element of S] means ||.($1 - p).|| <= r;

      

       A1: for v be Element of the carrier of S holds ( P1[v] iff P2[v]) by NORMSP_1: 7;

      { F(y) where y be Element of the carrier of S : P1[y] } = { F(y) where y be Element of the carrier of S : P2[y] } from FRAENKEL:sch 3( A1);

      hence thesis;

    end;

    theorem :: NDIFF_8:19

    for p be Element of S, r be Real st 0 < r holds ( Ball (p,r)) is Neighbourhood of p

    proof

      let p be Element of S, r be Real;

      assume 0 < r;

      then { y where y be Point of S : ||.(y - p).|| < r } is Neighbourhood of p by NFCONT_1: 3;

      hence thesis by LMBALL;

    end;

    registration

      let X be RealNormSpace, x be Point of X, r be Real;

      cluster ( Ball (x,r)) -> open;

      coherence

      proof

        defpred P[ Element of X] means ||.(x - $1).|| < r;

        set K = { q where q be Point of X : P[q] };

        K c= the carrier of X from FRAENKEL:sch 10;

        then

        reconsider K as Subset of X;

        reconsider T = K as Subset of ( TopSpaceNorm X);

        T is open by NORMSP_2: 8;

        hence thesis by NORMSP_2: 16;

      end;

      cluster ( cl_Ball (x,r)) -> closed;

      coherence

      proof

        defpred P[ Element of X] means ||.(x - $1).|| <= r;

        set K = { q where q be Point of X : P[q] };

        K c= the carrier of X from FRAENKEL:sch 10;

        then

        reconsider K as Subset of X;

        reconsider T = K as Subset of ( TopSpaceNorm X);

        T is closed by NORMSP_2: 9;

        hence thesis by NORMSP_2: 15;

      end;

    end

    theorem :: NDIFF_8:20

    

     NORMSP27: for X be RealNormSpace, V be Subset of X holds V is open iff for x be Point of X st x in V holds ex r be Real st r > 0 & ( Ball (x,r)) c= V

    proof

      let X be RealNormSpace, V be Subset of X;

      reconsider V0 = V as Subset of ( TopSpaceNorm X);

      hereby

        assume V is open;

        then

         A1: V0 is open by NORMSP_2: 16;

        thus for x be Point of X st x in V holds ex r be Real st r > 0 & ( Ball (x,r)) c= V

        proof

          let x be Point of X;

          assume x in V;

          then

          consider r be Real such that

           A2: r > 0 & { y where y be Point of X : ||.(x - y).|| < r } c= V0 by A1, NORMSP_2: 7;

          take r;

          thus thesis by A2;

        end;

      end;

      assume

       A3: for x be Point of X st x in V holds ex r be Real st r > 0 & ( Ball (x,r)) c= V;

      for x be Point of X st x in V0 holds ex r be Real st r > 0 & { y where y be Point of X : ||.(x - y).|| < r } c= V0

      proof

        let x be Point of X;

        assume x in V0;

        then

        consider r be Real such that

         A4: r > 0 & ( Ball (x,r)) c= V by A3;

        take r;

        thus thesis by A4;

      end;

      then V0 is open by NORMSP_2: 7;

      hence thesis by NORMSP_2: 16;

    end;

    theorem :: NDIFF_8:21

    

     NORMSP35: for X,Y be RealNormSpace, x be Point of X, y be Point of Y, z be Point of [:X, Y:] st z = [x, y] holds ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.||

    proof

      let X,Y be RealNormSpace, x be Point of X, y be Point of Y, z be Point of [:X, Y:];

      assume z = [x, y];

      then

       A2: ||.z.|| = ( sqrt (( ||.x.|| ^2 ) + ( ||.y.|| ^2 ))) by LMNR0;

      ( 0 + ( ||.x.|| ^2 )) <= (( ||.x.|| ^2 ) + ( ||.y.|| ^2 )) by XREAL_1: 6;

      then ( sqrt ( ||.x.|| ^2 )) <= ( sqrt (( ||.x.|| ^2 ) + ( ||.y.|| ^2 ))) by SQUARE_1: 26;

      hence ||.x.|| <= ||.z.|| by A2, SQUARE_1: 22;

      ( 0 + ( ||.y.|| ^2 )) <= (( ||.x.|| ^2 ) + ( ||.y.|| ^2 )) by XREAL_1: 6;

      then ( sqrt ( ||.y.|| ^2 )) <= ( sqrt (( ||.x.|| ^2 ) + ( ||.y.|| ^2 ))) by SQUARE_1: 26;

      hence ||.y.|| <= ||.z.|| by A2, SQUARE_1: 22;

    end;

    theorem :: NDIFF_8:22

    

     NORMSP31: for X,Y be RealNormSpace, x be Point of X, y be Point of Y, z be Point of [:X, Y:], r1 be Real st 0 < r1 & z = [x, y] holds ex r2 be Real st 0 < r2 & r2 < r1 & [:( Ball (x,r2)), ( Ball (y,r2)):] c= ( Ball (z,r1))

    proof

      let X,Y be RealNormSpace, x be Point of X, y be Point of Y, z be Point of [:X, Y:], r1 be Real;

      assume

       A1: 0 < r1 & z = [x, y];

      take r2 = (r1 / 2);

      thus 0 < r2 & r2 < r1 by A1, XREAL_1: 215, XREAL_1: 216;

      

       A2: ((r1 ^2 ) / 2) < (r1 ^2 ) by A1, SQUARE_1: 12, XREAL_1: 216;

      thus [:( Ball (x,r2)), ( Ball (y,r2)):] c= ( Ball (z,r1))

      proof

        let w be object;

        assume w in [:( Ball (x,r2)), ( Ball (y,r2)):];

        then

        consider x1,y1 be object such that

         A3: x1 in ( Ball (x,r2)) & y1 in ( Ball (y,r2)) & w = [x1, y1] by ZFMISC_1:def 2;

        reconsider x1 as Point of X by A3;

        reconsider y1 as Point of Y by A3;

         [x1, y1] is set by TARSKI: 1;

        then

        reconsider xy = w as Point of [:X, Y:] by A3, PRVECT_3: 18;

        ex p be Point of X st x1 = p & ||.(x - p).|| < r2 by A3;

        then

         A4: ( ||.(x - x1).|| ^2 ) < (r2 ^2 ) by SQUARE_1: 16;

        ex p be Point of Y st y1 = p & ||.(y - p).|| < r2 by A3;

        then

         A5: ( ||.(y - y1).|| ^2 ) < (r2 ^2 ) by SQUARE_1: 16;

        ( - xy) = [( - x1), ( - y1)] by A3, PRVECT_3: 18;

        then (z - xy) = [(x - x1), (y - y1)] by A1, PRVECT_3: 18;

        then

         A7: ||.(z - xy).|| = ( sqrt (( ||.(x - x1).|| ^2 ) + ( ||.(y - y1).|| ^2 ))) by LMNR0;

        (( ||.(x - x1).|| ^2 ) + ( ||.(y - y1).|| ^2 )) < ((r2 ^2 ) + (r2 ^2 )) by A4, A5, XREAL_1: 8;

        then (( ||.(x - x1).|| ^2 ) + ( ||.(y - y1).|| ^2 )) < (r1 ^2 ) by A2, XXREAL_0: 2;

        then ( sqrt (( ||.(x - x1).|| ^2 ) + ( ||.(y - y1).|| ^2 ))) < ( sqrt (r1 ^2 )) by SQUARE_1: 27;

        then ||.(z - xy).|| < r1 by A1, A7, SQUARE_1: 22;

        hence w in ( Ball (z,r1));

      end;

    end;

    theorem :: NDIFF_8:23

    for X,Y be RealNormSpace, x be Point of X, y be Point of Y, V be Subset of [:X, Y:] st V is open & [x, y] in V holds ex r be Real st 0 < r & [:( Ball (x,r)), ( Ball (y,r)):] c= V

    proof

      let X,Y be RealNormSpace, x be Point of X, y be Point of Y, V be Subset of [:X, Y:];

      assume

       A1: V is open & [x, y] in V;

       [x, y] is set by TARSKI: 1;

      then

      reconsider z = [x, y] as Point of [:X, Y:] by PRVECT_3: 18;

      consider r be Real such that

       A2: r > 0 & ( Ball (z,r)) c= V by A1, NORMSP27;

      consider r2 be Real such that

       A3: 0 < r2 & r2 < r & [:( Ball (x,r2)), ( Ball (y,r2)):] c= ( Ball (z,r)) by A2, NORMSP31;

      take r2;

      thus 0 < r2 by A3;

      thus [:( Ball (x,r2)), ( Ball (y,r2)):] c= V by A2, A3, XBOOLE_1: 1;

    end;

    theorem :: NDIFF_8:24

    for X,Y be RealNormSpace, x be Point of X, y be Point of Y, V be Subset of [:X, Y:], r be Real st V = [:( Ball (x,r)), ( Ball (y,r)):] holds V is open

    proof

      let X,Y be RealNormSpace, x be Point of X, y be Point of Y, V be Subset of [:X, Y:], r be Real;

      assume

       A1: V = [:( Ball (x,r)), ( Ball (y,r)):];

      for z be Point of [:X, Y:] st z in V holds ex s be Real st s > 0 & ( Ball (z,s)) c= V

      proof

        let z be Point of [:X, Y:];

        assume

         A2: z in V;

        consider x1 be Point of X, y1 be Point of Y such that

         A3: z = [x1, y1] by PRVECT_3: 18;

        

         A4: x1 in ( Ball (x,r)) & y1 in ( Ball (y,r)) by A1, A2, A3, ZFMISC_1: 87;

        

         A5: ex p be Point of X st x1 = p & ||.(x - p).|| < r by A4;

        

         A6: ex p be Point of Y st y1 = p & ||.(y - p).|| < r by A4;

        set r1 = (r - ||.(x - x1).||);

        set r2 = (r - ||.(y - y1).||);

        

         A7: 0 < r1 by A5, XREAL_1: 50;

        

         A8: 0 < r2 by A6, XREAL_1: 50;

        reconsider s = ( min (r1,r2)) as Real;

        

         A9: 0 < s by A7, A8, XXREAL_0: 15;

        

         A10: s <= (r - ||.(x - x1).||) by XXREAL_0: 17;

        

         A11: s <= (r - ||.(y - y1).||) by XXREAL_0: 17;

        ( Ball (z,s)) c= V

        proof

          let w be object;

          assume

           A12: w in ( Ball (z,s));

          then

          reconsider q = w as Point of [:X, Y:];

          

           A13: ex t be Point of [:X, Y:] st q = t & ||.(z - t).|| < s by A12;

          consider qx be Point of X, qy be Point of Y such that

           A14: q = [qx, qy] by PRVECT_3: 18;

          ( - q) = [( - qx), ( - qy)] by A14, PRVECT_3: 18;

          then (z - q) = [(x1 - qx), (y1 - qy)] by A3, PRVECT_3: 18;

          then ||.(x1 - qx).|| <= ||.(z - q).|| & ||.(y1 - qy).|| <= ||.(z - q).|| by NORMSP35;

          then

           A16: ||.(x1 - qx).|| < s & ||.(y1 - qy).|| < s by A13, XXREAL_0: 2;

          ((x - x1) + (x1 - qx)) = (((x - x1) + x1) - qx) by RLVECT_1: 28

          .= (x - qx) by RLVECT_4: 1;

          then

           A17: ||.(x - qx).|| <= ( ||.(x - x1).|| + ||.(x1 - qx).||) by NORMSP_1:def 1;

          

           A18: ( ||.(x - x1).|| + ||.(x1 - qx).||) < ( ||.(x - x1).|| + s) by A16, XREAL_1: 8;

          ( ||.(x - x1).|| + s) <= ( ||.(x - x1).|| + (r - ||.(x - x1).||)) by A10, XREAL_1: 7;

          then ( ||.(x - x1).|| + ||.(x1 - qx).||) < r by A18, XXREAL_0: 2;

          then ||.(x - qx).|| < r by A17, XXREAL_0: 2;

          then

           A19: qx in ( Ball (x,r));

          ((y - y1) + (y1 - qy)) = (((y - y1) + y1) - qy) by RLVECT_1: 28

          .= (y - qy) by RLVECT_4: 1;

          then

           A20: ||.(y - qy).|| <= ( ||.(y - y1).|| + ||.(y1 - qy).||) by NORMSP_1:def 1;

          

           A21: ( ||.(y - y1).|| + ||.(y1 - qy).||) < ( ||.(y - y1).|| + s) by A16, XREAL_1: 8;

          ( ||.(y - y1).|| + s) <= ( ||.(y - y1).|| + (r - ||.(y - y1).||)) by A11, XREAL_1: 7;

          then ( ||.(y - y1).|| + ||.(y1 - qy).||) < r by A21, XXREAL_0: 2;

          then ||.(y - qy).|| < r by A20, XXREAL_0: 2;

          then qy in ( Ball (y,r));

          hence w in V by A1, A14, A19, ZFMISC_1: 87;

        end;

        hence thesis by A9;

      end;

      hence V is open by NORMSP27;

    end;

    theorem :: NDIFF_8:25

    

     LQ2: for E,F be RealNormSpace, Q be LinearOperator of E, F, v be Point of E st Q is one-to-one holds (Q . v) = ( 0. F) iff v = ( 0. E)

    proof

      let E,F be RealNormSpace, Q be LinearOperator of E, F, v be Point of E;

      assume

       A1: Q is one-to-one;

      hereby

        assume

         A2: (Q . v) = ( 0. F);

        

         A3: ( dom Q) = the carrier of E by FUNCT_2:def 1;

        (Q . ( 0. E)) = ( 0. F) by LOPBAN_7: 3;

        hence v = ( 0. E) by A1, A2, A3, FUNCT_1:def 4;

      end;

      assume v = ( 0. E);

      hence (Q . v) = ( 0. F) by LOPBAN_7: 3;

    end;

    theorem :: NDIFF_8:26

    

     OP1: for E be RealNormSpace, X,Y be Subset of E, v be Point of E st X is open & Y = { (x + v) where x be Point of E : x in X } holds Y is open

    proof

      let E be RealNormSpace, X,Y be Subset of E, v be Point of E;

      assume that

       A1: X is open and

       A2: Y = { (x + v) where x be Point of E : x in X };

      deffunc FHP( Point of E) = ((1 * $1) + ( - v));

      consider H be Function of E, E such that

       A3: for p be Point of E holds (H . p) = FHP(p) from FUNCT_2:sch 4;

      

       A4: ( dom H) = the carrier of E by FUNCT_2:def 1;

      for p be Point of E st p in the carrier of E holds (H /. p) = ((1 * p) + ( - v)) by A3;

      then

       A5: H is_continuous_on the carrier of E by A4, NFCONT_1: 52;

      reconsider H1 = H as Function of ( TopSpaceNorm E), ( TopSpaceNorm E);

      

       A6: H1 is continuous by A5, NORMSP_2: 19;

      reconsider X1 = X, Y1 = Y as Subset of ( TopSpaceNorm E);

      

       A7: X1 is open by A1, NORMSP_2: 16;

      ( [#] ( TopSpaceNorm E)) <> {} ;

      then (H1 " X1) is open by A6, A7, TOPS_2: 43;

      then

       A9: (H " X) is open by NORMSP_2: 16;

      for s be object holds s in (H " X) iff s in Y

      proof

        let s be object;

        hereby

          assume

           A10: s in (H " X);

          then

           A11: s in ( dom H) & (H . s) in X by FUNCT_1:def 7;

          reconsider s1 = s as Point of E by A10;

          

           A12: (H . s) = ((1 * s1) + ( - v)) by A3

          .= (s1 - v) by RLVECT_1:def 8;

          

           A13: (H . s) = (H /. s) by A11, PARTFUN1:def 6;

          

          then ((H /. s) + v) = (s1 - (v - v)) by A12, RLVECT_1: 29

          .= (s1 - ( 0. E)) by RLVECT_1: 15

          .= s1 by RLVECT_1: 13;

          hence s in Y by A2, A11, A13;

        end;

        assume s in Y;

        then

        consider x be Point of E such that

         A14: s = (x + v) & x in X by A2;

        reconsider s1 = s as Point of E by A14;

        (H . s1) = ((1 * s1) + ( - v)) by A3

        .= ((x + v) - v) by A14, RLVECT_1:def 8

        .= (x + (v - v)) by RLVECT_1: 28

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

        .= x by RLVECT_1:def 4;

        hence s in (H " X) by A4, A14, FUNCT_1:def 7;

      end;

      hence thesis by A9, TARSKI: 2;

    end;

    theorem :: NDIFF_8:27

    

     OP2: for E be RealNormSpace, X,Y be Subset of E, v be Point of E st X is open & Y = { (x - v) where x be Point of E : x in X } holds Y is open

    proof

      let E be RealNormSpace, X,Y be Subset of E, v be Point of E;

      assume that

       A1: X is open and

       A2: Y = { (x - v) where x be Point of E : x in X };

      set w = ( - v);

      { (x + w) where x be Point of E : x in X } c= the carrier of E

      proof

        let s be object;

        assume s in { (x + w) where x be Point of E : x in X };

        then ex x be Point of E st s = (x + w) & x in X;

        hence s in the carrier of E;

      end;

      then

      reconsider Z = { (x + w) where x be Point of E : x in X } as Subset of E;

      deffunc F( Point of E) = ($1 + w);

      deffunc G( Point of E) = ($1 - v);

      defpred P[ Point of E] means $1 in X;

      

       A3: for v be Element of the carrier of E holds F(v) = G(v);

      { F(v1) where v1 be Element of the carrier of E : P[v1] } = { G(v2) where v2 be Element of the carrier of E : P[v2] } from FRAENKEL:sch 5( A3);

      hence thesis by A1, A2, OP1;

    end;

    begin

    theorem :: NDIFF_8:28

    

     FIXPOINT: for X be RealBanachSpace, S be non empty Subset of X, f be PartFunc of X, X st S is closed & ( dom f) = S & ( rng f) c= S & ex k be Real st 0 < k < 1 & for x,y be Point of X st x in S & y in S holds ||.((f /. x) - (f /. y)).|| <= (k * ||.(x - y).||) holds (ex x0 be Point of X st x0 in S & (f . x0) = x0) & (for x0,y0 be Point of X st x0 in S & y0 in S & (f . x0) = x0 & (f . y0) = y0 holds x0 = y0)

    proof

      let X be RealBanachSpace, S be non empty Subset of X, f be PartFunc of X, X;

      assume that

       A1: S is closed and

       A2: ( dom f) = S & ( rng f) c= S and

       A3: ex k be Real st 0 < k < 1 & for x,y be Point of X st x in S & y in S holds ||.((f /. x) - (f /. y)).|| <= (k * ||.(x - y).||);

      consider x0 be object such that

       A4: x0 in S by XBOOLE_0:def 1;

      reconsider x0 as Element of X by A4;

      consider K be Real such that

       A5: 0 < K and

       A6: K < 1 and

       A7: for x,y be Point of X st x in S & y in S holds ||.((f /. x) - (f /. y)).|| <= (K * ||.(x - y).||) by A3;

      deffunc G( set, set) = (f . $2);

      consider g be Function such that

       A8: ( dom g) = NAT & (g . 0 ) = x0 & for n be Nat holds (g . (n + 1)) = G(n,.) from NAT_1:sch 11;

      defpred P[ Nat] means (g . $1) in S & (g . $1) is Element of X;

      

       A9: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A10: P[k];

        

         A11: (g . (k + 1)) = (f . (g . k)) by A8;

        (f . (g . k)) in ( rng f) by A2, A10, FUNCT_1: 3;

        hence thesis by A2, A11;

      end;

      

       A12: P[ 0 ] by A4, A8;

      

       A13: for n be Nat holds P[n] from NAT_1:sch 2( A12, A9);

      for n be object st n in NAT holds (g . n) in the carrier of X

      proof

        let n be object such that

         A14: n in NAT ;

        reconsider k = n as Nat by A14;

        (g . k) is Element of X by A13;

        hence thesis;

      end;

      then

      reconsider g as sequence of X by A8, FUNCT_2: 3;

      for x be Element of NAT holds (g . x) in S by A13;

      then

       A15: ( rng g) c= S by FUNCT_2: 114;

      

       A16: for n be Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K to_power n))

      proof

        defpred P[ Nat] means ||.((g . ($1 + 1)) - (g . $1)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K to_power $1));

        

         A17: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          

           A18: (g . (k + 1)) in S & (g . k) in S by A13;

          

           A19: (f /. (g . (k + 1))) = (f . (g . (k + 1))) & (f /. (g . k)) = (f . (g . k)) by A2, A13, PARTFUN1:def 6;

          assume P[k];

          then

           A20: (K * ||.((g . (k + 1)) - (g . k)).||) <= (K * ( ||.((g . 1) - (g . 0 )).|| * (K to_power k))) by A5, XREAL_1: 64;

           ||.((f /. (g . (k + 1))) - (f /. (g . k))).|| <= (K * ||.((g . (k + 1)) - (g . k)).||) by A7, A18;

          then ||.((f /. (g . (k + 1))) - (f /. (g . k))).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K * (K to_power k))) by A20, XXREAL_0: 2;

          then

           A21: ||.((f /. (g . (k + 1))) - (f /. (g . k))).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power 1) * (K to_power k))) by POWER: 25;

          (g . (k + 1)) = (f . (g . k)) by A8;

          then ||.((g . ((k + 1) + 1)) - (g . (k + 1))).|| = ||.((f /. (g . (k + 1))) - (f /. (g . k))).|| by A8, A19;

          hence thesis by A5, A21, POWER: 27;

        end;

         ||.((g . ( 0 + 1)) - (g . 0 )).|| = ( ||.((g . 1) - (g . 0 )).|| * 1)

        .= ( ||.((g . 1) - (g . 0 )).|| * (K to_power 0 )) by POWER: 24;

        then

         A22: P[ 0 ];

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

        hence thesis;

      end;

      

       A23: for k,n be Nat holds ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)))

      proof

        defpred P[ Nat] means for n be Nat holds ||.((g . (n + $1)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + $1))) / (1 - K)));

         A24:

        now

          let k be Nat such that

           A25: P[k];

          now

            let n be Nat;

            (1 - K) <> 0 by A6;

            

            then

             A26: (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k)))) = (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ((( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k))) * (1 - K)) / (1 - K))) by XCMPLX_1: 89

            .= (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (( ||.((g . 1) - (g . 0 )).|| * ((K to_power (n + k)) * (1 - K))) / (1 - K)))

            .= (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ( ||.((g . 1) - (g . 0 )).|| * (((K to_power (n + k)) * (1 - K)) / (1 - K)))) by XCMPLX_1: 74

            .= ( ||.((g . 1) - (g . 0 )).|| * ((((K to_power n) - (K to_power (n + k))) / (1 - K)) + (((K to_power (n + k)) * (1 - K)) / (1 - K))))

            .= ( ||.((g . 1) - (g . 0 )).|| * ((((K to_power n) - (K to_power (n + k))) + ((K to_power (n + k)) * (1 - K))) / (1 - K))) by XCMPLX_1: 62

            .= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K * (K to_power (n + k)))) / (1 - K)))

            .= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - ((K to_power 1) * (K to_power (n + k)))) / (1 - K))) by POWER: 25

            .= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power ((n + k) + 1))) / (1 - K))) by A5, POWER: 27;

             ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) & ||.((g . ((n + k) + 1)) - (g . (n + k))).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k))) by A16, A25;

            then ||.((g . (n + (k + 1))) - (g . n)).|| <= ( ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).||) & ( ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).||) <= (( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k))) + ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)))) by NORMSP_1: 10, XREAL_1: 7;

            hence ||.((g . (n + (k + 1))) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + (k + 1)))) / (1 - K))) by A26, XXREAL_0: 2;

          end;

          hence P[(k + 1)];

        end;

        now

          let n be Nat;

           ||.((g . (n + 0 )) - (g . n)).|| = ||.( 0. X).|| by RLVECT_1: 15

          .= 0 ;

          hence ||.((g . (n + 0 )) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + 0 ))) / (1 - K)));

        end;

        then

         A27: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A27, A24);

        hence thesis;

      end;

      

       A28: for k,n be Nat holds ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K)))

      proof

        let k be Nat;

        now

          let n be Nat;

          (K to_power (n + k)) > 0 by A5, POWER: 34;

          then

           A29: ((K to_power n) - (K to_power (n + k))) <= ((K to_power n) - 0 ) by XREAL_1: 13;

          (1 - K) > (1 - 1) by A6, XREAL_1: 15;

          then (((K to_power n) - (K to_power (n + k))) / (1 - K)) <= ((K to_power n) / (1 - K)) by A29, XREAL_1: 72;

          then

           A30: ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by XREAL_1: 64;

           ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) by A23;

          hence ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by A30, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      now

        let e be Real such that

         A31: e > 0 ;

        (e / 2) > 0 by A31, XREAL_1: 215;

        then

        consider n be Nat such that

         A32: |.(( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)).| < (e / 2) by A5, A6, NFCONT_2: 16;

        reconsider nn = (n + 1) as Nat;

        take nn;

        (( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)) <= |.(( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)).| by ABSVALUE: 4;

        then (( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)) < (e / 2) by A32, XXREAL_0: 2;

        then

         A33: ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) < (e / 2) by XCMPLX_1: 75;

        now

          let m,l be Nat such that

           A34: nn <= m and

           A35: nn <= l;

          n < m by A34, NAT_1: 13;

          then

          consider k1 be Nat such that

           A36: (n + k1) = m by NAT_1: 10;

          n < l by A35, NAT_1: 13;

          then

          consider k2 be Nat such that

           A37: (n + k2) = l by NAT_1: 10;

          reconsider k2 as Nat;

           ||.((g . (n + k2)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by A28;

          then

           A38: ||.((g . l) - (g . n)).|| < (e / 2) by A33, A37, XXREAL_0: 2;

          reconsider k1 as Nat;

           ||.((g . (n + k1)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by A28;

          then ||.((g . m) - (g . n)).|| < (e / 2) by A33, A36, XXREAL_0: 2;

          hence ||.((g . l) - (g . m)).|| < e by A31, A38, NDIFF_2: 4;

        end;

        hence for n,m be Nat st n >= nn & m >= nn holds ||.((g . n) - (g . m)).|| < e;

      end;

      then

       A39: g is convergent by LOPBAN_1:def 15, RSSPACE3: 8;

      then

       A40: (K (#) ||.(g - ( lim g)).||) is convergent by NORMSP_1: 24, SEQ_2: 7;

      

       A41: ( lim g) in S by A1, A15, A39, NFCONT_1:def 3;

       A42:

      now

        let n be Nat;

        

         A43: (g . n) in S by A13;

        

         A44: (f /. (g . n)) = (f . (g . n)) & (f /. ( lim g)) = (f . ( lim g)) by A1, A2, A13, A15, A39, NFCONT_1:def 3, PARTFUN1:def 6;

         ||.(((g ^\ 1) . n) - (f /. ( lim g))).|| = ||.((g . (n + 1)) - (f /. ( lim g))).|| by NAT_1:def 3

        .= ||.((f /. (g . n)) - (f /. ( lim g))).|| by A8, A44;

        hence ||.(((g ^\ 1) . n) - (f /. ( lim g))).|| <= (K * ||.((g . n) - ( lim g)).||) by A7, A41, A43;

      end;

      

       A45: ( lim (K (#) ||.(g - ( lim g)).||)) = (K * ( lim ||.(g - ( lim g)).||)) by A39, NORMSP_1: 24, SEQ_2: 8

      .= (K * 0 ) by A39, NORMSP_1: 24

      .= 0 ;

      

       A46: for e be Real st e > 0 holds ex n be Nat st for m be Nat st n <= m holds ||.(((g ^\ 1) . m) - (f /. ( lim g))).|| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider n be Nat such that

         A47: for m be Nat st n <= m holds |.(((K (#) ||.(g - ( lim g)).||) . m) - 0 ).| < e by A40, A45, SEQ_2:def 7;

        take n;

        now

          let m be Nat;

          assume n <= m;

          then |.(((K (#) ||.(g - ( lim g)).||) . m) - 0 ).| < e by A47;

          then |.(K * ( ||.(g - ( lim g)).|| . m)).| < e by SEQ_1: 9;

          then |.(K * ||.((g - ( lim g)) . m).||).| < e by NORMSP_0:def 4;

          then

           A48: |.(K * ||.((g . m) - ( lim g)).||).| < e by NORMSP_1:def 4;

          (K * ||.((g . m) - ( lim g)).||) <= |.(K * ||.((g . m) - ( lim g)).||).| by ABSVALUE: 4;

          then

           A49: (K * ||.((g . m) - ( lim g)).||) < e by A48, XXREAL_0: 2;

           ||.(((g ^\ 1) . m) - (f /. ( lim g))).|| <= (K * ||.((g . m) - ( lim g)).||) by A42;

          hence ||.(((g ^\ 1) . m) - (f /. ( lim g))).|| < e by A49, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      set xp = ( lim g);

      

       A50: (g ^\ 1) is convergent & ( lim (g ^\ 1)) = ( lim g) by A39, LOPBAN_3: 9;

      then

       A51: ( lim g) = (f /. ( lim g)) by A46, NORMSP_1:def 7;

       A52:

      now

        let x be Point of X such that

         A53: x in S & (f . x) = x;

        

         A54: (f /. x) = x by A2, A53, PARTFUN1:def 6;

        

         A55: for k be Nat holds ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power k))

        proof

          defpred P[ Nat] means ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power $1));

          

           A56: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume P[k];

            then

             A57: (K * ||.(x - xp).||) <= (K * ( ||.(x - xp).|| * (K to_power k))) by A5, XREAL_1: 64;

             ||.((f /. x) - (f /. xp)).|| <= (K * ||.(x - xp).||) by A7, A41, A53;

            then ||.((f /. x) - (f /. xp)).|| <= ( ||.(x - xp).|| * (K * (K to_power k))) by A57, XXREAL_0: 2;

            then ||.((f /. x) - (f /. xp)).|| <= ( ||.(x - xp).|| * ((K to_power 1) * (K to_power k))) by POWER: 25;

            hence thesis by A5, A51, A54, POWER: 27;

          end;

           ||.(x - xp).|| = ( ||.(x - xp).|| * 1)

          .= ( ||.(x - xp).|| * (K to_power 0 )) by POWER: 24;

          then

           A58: P[ 0 ];

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

          hence thesis;

        end;

        for e be Real st 0 < e holds ||.(x - xp).|| < e

        proof

          let e be Real;

          assume 0 < e;

          then

          consider n be Nat such that

           A59: |.( ||.(x - xp).|| * (K to_power n)).| < e by A5, A6, NFCONT_2: 16;

          ( ||.(x - xp).|| * (K to_power n)) <= |.( ||.(x - xp).|| * (K to_power n)).| by ABSVALUE: 4;

          then

           A60: ( ||.(x - xp).|| * (K to_power n)) < e by A59, XXREAL_0: 2;

           ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power n)) by A55;

          hence thesis by A60, XXREAL_0: 2;

        end;

        hence x = xp by NDIFF_2: 4;

      end;

      xp = (f /. xp) by A46, A50, NORMSP_1:def 7;

      then xp = (f . xp) by A1, A2, A15, A39, NFCONT_1:def 3, PARTFUN1:def 6;

      hence ex x0 be Point of X st x0 in S & (f . x0) = x0 by A1, A15, A39, NFCONT_1:def 3;

      for x0,y0 be Point of X st x0 in S & y0 in S & (f . x0) = x0 & (f . y0) = y0 holds x0 = y0

      proof

        let x0,y0 be Point of X such that

         A61: x0 in S and

         A62: y0 in S and

         A63: (f . x0) = x0 and

         A64: (f . y0) = y0;

        x0 = xp by A52, A61, A63;

        hence thesis by A52, A62, A64;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_8:29

    

     FIXPOINT2: for E be RealNormSpace, F be RealBanachSpace, E0 be non empty Subset of E, F0 be non empty Subset of F, Fai be PartFunc of [:E, F:], F st F0 is closed & [:E0, F0:] c= ( dom Fai) & (for x be Point of E, y be Point of F st x in E0 & y in F0 holds (Fai . (x,y)) in F0) & (for y be Point of F st y in F0 holds for x0 be Point of E st x0 in E0 holds for e be Real st 0 < e holds ex d be Real st 0 < d & for x1 be Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds ||.((Fai /. [x1, y]) - (Fai /. [x0, y])).|| < e) & ex k be Real st 0 < k & k < 1 & (for x be Point of E st x in E0 holds for y1,y2 be Point of F st y1 in F0 & y2 in F0 holds ||.((Fai /. [x, y1]) - (Fai /. [x, y2])).|| <= (k * ||.(y1 - y2).||)) holds (for x be Point of E st x in E0 holds (ex y be Point of F st y in F0 & (Fai . (x,y)) = y) & (for y1,y2 be Point of F st y1 in F0 & y2 in F0 & (Fai . (x,y1)) = y1 & (Fai . (x,y2)) = y2 holds y1 = y2)) & (for x0 be Point of E, y0 be Point of F st x0 in E0 & y0 in F0 & (Fai . (x0,y0)) = y0 holds (for e be Real st 0 < e holds ex d be Real st 0 < d & (for x1 be Point of E, y1 be Point of F st x1 in E0 & y1 in F0 & (Fai . (x1,y1)) = y1 & ||.(x1 - x0).|| < d holds ||.(y1 - y0).|| < e)))

    proof

      let E be RealNormSpace, F be RealBanachSpace, E0 be non empty Subset of E, F0 be non empty Subset of F, Fai be PartFunc of [:E, F:], F such that

       A1: F0 is closed and

       A2: [:E0, F0:] c= ( dom Fai) and

       A3: for x be Point of E, y be Point of F st x in E0 & y in F0 holds (Fai . (x,y)) in F0 and

       A4: for y be Point of F st y in F0 holds for x0 be Point of E st x0 in E0 holds for e be Real st 0 < e holds ex d be Real st 0 < d & for x1 be Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds ||.((Fai /. [x1, y]) - (Fai /. [x0, y])).|| < e and

       A5: ex k be Real st 0 < k & k < 1 & for x be Point of E st x in E0 holds for y1,y2 be Point of F st y1 in F0 & y2 in F0 holds ||.((Fai /. [x, y1]) - (Fai /. [x, y2])).|| <= (k * ||.(y1 - y2).||);

      consider k be Real such that

       A6: 0 < k & k < 1 and

       A7: for x be Point of E st x in E0 holds for y1,y2 be Point of F st y1 in F0 & y2 in F0 holds ||.((Fai /. [x, y1]) - (Fai /. [x, y2])).|| <= (k * ||.(y1 - y2).||) by A5;

      thus for x be Point of E st x in E0 holds (ex y be Point of F st y in F0 & (Fai . (x,y)) = y) & (for y1,y2 be Point of F st y1 in F0 & y2 in F0 & (Fai . (x,y1)) = y1 & (Fai . (x,y2)) = y2 holds y1 = y2)

      proof

        let x be Point of E;

        deffunc FX1( object) = (Fai . (x,$1));

        assume

         A8: x in E0;

        then

         A9: for y be object st y in F0 holds FX1(y) in F0 by A3;

        consider Fai0 be Function of F0, F0 such that

         A10: for y be object st y in F0 holds (Fai0 . y) = FX1(y) from FUNCT_2:sch 2( A9);

        

         A11: ( rng Fai0) c= F0;

        

         A12: ( dom Fai0) = F0 by FUNCT_2:def 1;

        ( rng Fai0) c= the carrier of F by XBOOLE_1: 1;

        then

        reconsider Fai0 as PartFunc of F, F by A12, RELSET_1: 4;

        

         A13: for z,y be Point of F st z in F0 & y in F0 holds ||.((Fai0 /. z) - (Fai0 /. y)).|| <= (k * ||.(z - y).||)

        proof

          let z,y be Point of F;

          assume

           A14: z in F0 & y in F0;

          then

           A15: [x, z] in [:E0, F0:] by A8, ZFMISC_1: 87;

          

           A16: [x, y] in [:E0, F0:] by A8, A14, ZFMISC_1: 87;

          

           A18: y in ( dom Fai0) by A14, FUNCT_2:def 1;

          z in ( dom Fai0) by A14, FUNCT_2:def 1;

          

          then

           A19: (Fai0 /. z) = (Fai0 . z) by PARTFUN1:def 6

          .= FX1(z) by A10, A14

          .= (Fai /. [x, z]) by A2, A15, PARTFUN1:def 6;

          (Fai0 /. y) = (Fai0 . y) by A18, PARTFUN1:def 6

          .= FX1(y) by A10, A14

          .= (Fai /. [x, y]) by A2, A16, PARTFUN1:def 6;

          hence thesis by A7, A8, A14, A19;

        end;

        thus ex y be Point of F st y in F0 & (Fai . (x,y)) = y

        proof

          consider y be Point of F such that

           A20: y in F0 & (Fai0 . y) = y by A1, A6, A11, A12, A13, FIXPOINT;

          take y;

          thus y in F0 by A20;

          thus (Fai . (x,y)) = y by A10, A20;

        end;

        thus for y1,y2 be Point of F st y1 in F0 & y2 in F0 & (Fai . (x,y1)) = y1 & (Fai . (x,y2)) = y2 holds y1 = y2

        proof

          let y1,y2 be Point of F such that

           A21: y1 in F0 & y2 in F0 & (Fai . (x,y1)) = y1 & (Fai . (x,y2)) = y2;

          

           A22: (Fai0 . y1) = y1 by A10, A21;

          (Fai0 . y2) = y2 by A10, A21;

          hence y1 = y2 by A1, A6, A11, A12, A13, A21, A22, FIXPOINT;

        end;

      end;

      thus for x0 be Point of E, y0 be Point of F st x0 in E0 & y0 in F0 & (Fai . (x0,y0)) = y0 holds (for e be Real st 0 < e holds ex d be Real st 0 < d & (for x1 be Point of E, y1 be Point of F st x1 in E0 & y1 in F0 & (Fai . (x1,y1)) = y1 & ||.(x1 - x0).|| < d holds ||.(y1 - y0).|| < e))

      proof

        let x0 be Point of E, y0 be Point of F;

        assume

         A24: x0 in E0 & y0 in F0 & (Fai . (x0,y0)) = y0;

        let e be Real;

        assume

         A25: 0 < e;

        reconsider e1 = (e * (1 - k)) as Real;

        

         A26: 0 < (1 - k) by A6, XREAL_1: 50;

        then

        consider d be Real such that

         A27: 0 < d & for x1 be Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds ||.((Fai /. [x1, y0]) - (Fai /. [x0, y0])).|| < e1 by A4, A24, A25, XREAL_1: 129;

        take d;

        thus 0 < d by A27;

        let x1 be Point of E, y1 be Point of F;

        assume

         A28: x1 in E0 & y1 in F0 & (Fai . (x1,y1)) = y1 & ||.(x1 - x0).|| < d;

         [x0, y0] in [:E0, F0:] by A24, ZFMISC_1: 87;

        then

         A29: y0 = (Fai /. [x0, y0]) by A2, A24, PARTFUN1:def 6;

         [x1, y1] in [:E0, F0:] by A28, ZFMISC_1: 87;

        then

         A30: y1 = (Fai /. [x1, y1]) by A2, A28, PARTFUN1:def 6;

        (((Fai /. [x1, y1]) - (Fai /. [x1, y0])) + ((Fai /. [x1, y0]) - (Fai /. [x0, y0]))) = ((((Fai /. [x1, y1]) - (Fai /. [x1, y0])) + (Fai /. [x1, y0])) - (Fai /. [x0, y0])) by RLVECT_1: 28

        .= ((Fai /. [x1, y1]) - (Fai /. [x0, y0])) by RLVECT_4: 1;

        then

         A31: ||.(y1 - y0).|| <= ( ||.((Fai /. [x1, y1]) - (Fai /. [x1, y0])).|| + ||.((Fai /. [x1, y0]) - (Fai /. [x0, y0])).||) by A29, A30, NORMSP_1:def 1;

         ||.((Fai /. [x1, y0]) - (Fai /. [x0, y0])).|| < e1 by A27, A28;

        then ( ||.((Fai /. [x1, y1]) - (Fai /. [x1, y0])).|| + ||.((Fai /. [x1, y0]) - (Fai /. [x0, y0])).||) < (e1 + (k * ||.(y1 - y0).||)) by A7, A24, A28, XREAL_1: 8;

        then ||.(y1 - y0).|| < (e1 + (k * ||.(y1 - y0).||)) by A31, XXREAL_0: 2;

        then ( ||.(y1 - y0).|| - (k * ||.(y1 - y0).||)) < ((e1 + (k * ||.(y1 - y0).||)) - (k * ||.(y1 - y0).||)) by XREAL_1: 14;

        then ((1 - k) * ||.(y1 - y0).||) < e1;

        then ||.(y1 - y0).|| < (e1 / (1 - k)) by A26, XREAL_1: 81;

        hence ||.(y1 - y0).|| < e by A26, XCMPLX_1: 89;

      end;

    end;

    theorem :: NDIFF_8:30

    

     FIXPOINT3: for E be RealNormSpace, F be RealBanachSpace, A be non empty Subset of E, B be non empty Subset of F, Fai be PartFunc of [:E, F:], F st B is closed & [:A, B:] c= ( dom Fai) & (for x be Point of E, y be Point of F st x in A & y in B holds (Fai . (x,y)) in B) & (for y be Point of F st y in B holds for x0 be Point of E st x0 in A holds for e be Real st 0 < e holds ex d be Real st 0 < d & for x1 be Point of E st x1 in A & ||.(x1 - x0).|| < d holds ||.((Fai /. [x1, y]) - (Fai /. [x0, y])).|| < e) & ex k be Real st 0 < k & k < 1 & (for x be Point of E st x in A holds for y1,y2 be Point of F st y1 in B & y2 in B holds ||.((Fai /. [x, y1]) - (Fai /. [x, y2])).|| <= (k * ||.(y1 - y2).||)) holds (ex g be PartFunc of E, F st g is_continuous_on A & ( dom g) = A & ( rng g) c= B & for x be Point of E st x in A holds (Fai . (x,(g . x))) = (g . x)) & (for g1,g2 be PartFunc of E, F st ( dom g1) = A & ( rng g1) c= B & ( dom g2) = A & ( rng g2) c= B & (for x be Point of E st x in A holds (Fai . (x,(g1 . x))) = (g1 . x)) & (for x be Point of E st x in A holds (Fai . (x,(g2 . x))) = (g2 . x)) holds g1 = g2)

    proof

      let E be RealNormSpace, F be RealBanachSpace, A be non empty Subset of E, B be non empty Subset of F, Fai be PartFunc of [:E, F:], F such that

       A1: B is closed and

       A2: [:A, B:] c= ( dom Fai) and

       A3: for x be Point of E, y be Point of F st x in A & y in B holds (Fai . (x,y)) in B and

       A4: for y be Point of F st y in B holds for x0 be Point of E st x0 in A holds for e be Real st 0 < e holds ex d be Real st 0 < d & for x1 be Point of E st x1 in A & ||.(x1 - x0).|| < d holds ||.((Fai /. [x1, y]) - (Fai /. [x0, y])).|| < e and

       A5: ex k be Real st 0 < k & k < 1 & for x be Point of E st x in A holds for y1,y2 be Point of F st y1 in B & y2 in B holds ||.((Fai /. [x, y1]) - (Fai /. [x, y2])).|| <= (k * ||.(y1 - y2).||);

      thus ex g be PartFunc of E, F st g is_continuous_on A & ( dom g) = A & ( rng g) c= B & for x be Point of E st x in A holds (Fai . (x,(g . x))) = (g . x)

      proof

        defpred FP[ object, object] means $2 in B & (Fai . ($1,$2)) = $2;

        

         A6: for x,y1,y2 be object st x in A & FP[x, y1] & FP[x, y2] holds y1 = y2 by A1, A2, A3, A4, A5, FIXPOINT2;

        

         A7: for x be object st x in A holds ex y be object st FP[x, y]

        proof

          let x be object;

          assume

           A8: x in A;

          then

          reconsider x0 = x as Point of E;

          consider y be Point of F such that

           A9: y in B & (Fai . (x0,y)) = y by A1, A2, A3, A4, A5, A8, FIXPOINT2;

          take y;

          thus thesis by A9;

        end;

        consider g be Function such that

         A10: ( dom g) = A & for x be object st x in A holds FP[x, (g . x)] from FUNCT_1:sch 2( A6, A7);

        

         A11: ( rng g) c= B

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A12: x in ( dom g) & y = (g . x) by FUNCT_1:def 3;

          thus y in B by A10, A12;

        end;

        then ( rng g) c= the carrier of F by XBOOLE_1: 1;

        then g in ( PFuncs (the carrier of E,the carrier of F)) by A10, PARTFUN1:def 3;

        then

        reconsider g as PartFunc of E, F by PARTFUN1: 46;

        take g;

        for z0 be Point of E holds for r be Real st z0 in A & 0 < r holds ex s be Real st 0 < s & for z1 be Point of E st z1 in A & ||.(z1 - z0).|| < s holds ||.((g /. z1) - (g /. z0)).|| < r

        proof

          let z0 be Point of E;

          let r be Real;

          assume

           A15: z0 in A & 0 < r;

          then

           A16: (Fai . (z0,(g . z0))) = (g . z0) by A10;

          

           A17: (g . z0) in ( rng g) by A10, A15, FUNCT_1: 3;

          (g . z0) = (g /. z0) by A10, A15, PARTFUN1:def 6;

          then

          consider s be Real such that

           A18: 0 < s & for x1 be Point of E, y1 be Point of F st x1 in A & y1 in B & (Fai . (x1,y1)) = y1 & ||.(x1 - z0).|| < s holds ||.(y1 - (g /. z0)).|| < r by A1, A2, A3, A4, A5, A11, A15, A16, A17, FIXPOINT2;

          take s;

          thus 0 < s by A18;

          let z1 be Point of E;

          assume

           A19: z1 in A & ||.(z1 - z0).|| < s;

          then

           A20: (Fai . (z1,(g . z1))) = (g . z1) by A10;

          

           A21: (g . z1) in B by A10, A19;

          (g . z1) = (g /. z1) by A10, A19, PARTFUN1:def 6;

          hence ||.((g /. z1) - (g /. z0)).|| < r by A18, A19, A20, A21;

        end;

        hence g is_continuous_on A by A10, NFCONT_1: 19;

        thus ( dom g) = A & ( rng g) c= B by A10, A11;

        thus for x be Point of E st x in A holds (Fai . (x,(g . x))) = (g . x) by A10;

      end;

      let g1,g2 be PartFunc of E, F such that

       A22: ( dom g1) = A & ( rng g1) c= B & ( dom g2) = A & ( rng g2) c= B & (for x be Point of E st x in A holds (Fai . (x,(g1 . x))) = (g1 . x)) & (for x be Point of E st x in A holds (Fai . (x,(g2 . x))) = (g2 . x));

      for x be object st x in ( dom g1) holds (g1 . x) = (g2 . x)

      proof

        let x be object;

        assume

         A23: x in ( dom g1);

        then

        reconsider y = x as Point of E;

        

         A24: (g1 . y) in ( rng g1) by A23, FUNCT_1: 3;

        then

        reconsider z1 = (g1 . y) as Point of F;

        

         A25: (g2 . y) in ( rng g2) by A22, A23, FUNCT_1: 3;

        then

        reconsider z2 = (g2 . y) as Point of F;

        (Fai . (y,z1)) = z1 & (Fai . (y,z2)) = z2 & z1 in B & z2 in B & y in A by A22, A23, A24, A25;

        hence (g1 . x) = (g2 . x) by A1, A2, A3, A4, A5, FIXPOINT2;

      end;

      hence g1 = g2 by A22, FUNCT_1: 2;

    end;

    theorem :: NDIFF_8:31

    for E,F be RealNormSpace, s1,s2 be Point of [:E, F:] st (s1 `2 ) = (s2 `2 ) holds ( reproj1 s1) = ( reproj1 s2)

    proof

      let E,F be RealNormSpace, s1,s2 be Point of [:E, F:];

      assume

       A1: (s1 `2 ) = (s2 `2 );

      now

        let r be Element of E;

        

        thus (( reproj1 s1) . r) = [r, (s2 `2 )] by A1, NDIFF_7:def 1

        .= (( reproj1 s2) . r) by NDIFF_7:def 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_8:32

    

     REP2: for E,F be RealNormSpace, s1,s2 be Point of [:E, F:] st (s1 `1 ) = (s2 `1 ) holds ( reproj2 s1) = ( reproj2 s2)

    proof

      let E,F be RealNormSpace, s1,s2 be Point of [:E, F:];

      assume

       A1: (s1 `1 ) = (s2 `1 );

      now

        let r be Element of F;

        

        thus (( reproj2 s1) . r) = [(s2 `1 ), r] by A1, NDIFF_7:def 2

        .= (( reproj2 s2) . r) by NDIFF_7:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_8:33

    

     LMCLOSE2: for E be RealNormSpace, r be Real, z,y1,y2 be Point of E st y1 in ( cl_Ball (z,r)) & y2 in ( cl_Ball (z,r)) holds [.y1, y2.] c= ( cl_Ball (z,r))

    proof

      let E be RealNormSpace, r be Real, z,y1,y2 be Point of E;

      assume

       A1: y1 in ( cl_Ball (z,r)) & y2 in ( cl_Ball (z,r));

      then

       A2: ex y1q be Element of E st y1 = y1q & ||.(z - y1q).|| <= r;

      

       A3: ex y2q be Element of E st y2 = y2q & ||.(z - y2q).|| <= r by A1;

      

       A4: [.y1, y2.] = { (((1 - r) * y1) + (r * y2)) where r be Real : 0 <= r <= 1 } by RLTOPSP1:def 2;

      let s be object;

      assume s in [.y1, y2.];

      then

      consider p be Real such that

       A5: s = (((1 - p) * y1) + (p * y2)) & 0 <= p & p <= 1 by A4;

      reconsider w = s as Point of E by A5;

      (((1 - p) * z) + (p * z)) = (((1 - p) + p) * z) by RLVECT_1:def 6

      .= z by RLVECT_1:def 8;

      

      then (z - w) = (((((1 - p) * z) + (p * z)) - ((1 - p) * y1)) - (p * y2)) by A5, RLVECT_1: 27

      .= (((((1 - p) * z) + ( - ((1 - p) * y1))) + (p * z)) - (p * y2)) by RLVECT_1:def 3

      .= ((((1 - p) * z) - ((1 - p) * y1)) + ((p * z) + ( - (p * y2)))) by RLVECT_1:def 3

      .= (((1 - p) * (z - y1)) + ((p * z) - (p * y2))) by RLVECT_1: 34

      .= (((1 - p) * (z - y1)) + (p * (z - y2))) by RLVECT_1: 34;

      then ||.(z - w).|| <= ( ||.((1 - p) * (z - y1)).|| + ||.(p * (z - y2)).||) by NORMSP_1:def 1;

      then ||.(z - w).|| <= (( |.(1 - p).| * ||.(z - y1).||) + ||.(p * (z - y2)).||) by NORMSP_1:def 1;

      then

       A7: ||.(z - w).|| <= (( |.(1 - p).| * ||.(z - y1).||) + ( |.p.| * ||.(z - y2).||)) by NORMSP_1:def 1;

      

       A8: |.(1 - p).| = (1 - p) & |.p.| = p by A5, COMPLEX1: 43, XREAL_1: 48;

       0 <= (1 - p) by A5, XREAL_1: 48;

      then

       A9: ((1 - p) * ||.(z - y1).||) <= ((1 - p) * r) by A2, XREAL_1: 64;

      (p * ||.(z - y2).||) <= (p * r) by A3, A5, XREAL_1: 64;

      then (((1 - p) * ||.(z - y1).||) + (p * ||.(z - y2).||)) <= (((1 - p) * r) + (p * r)) by A9, XREAL_1: 7;

      then ||.(z - w).|| <= (((1 - p) * r) + (p * r)) by A7, A8, XXREAL_0: 2;

      hence thesis;

    end;

    theorem :: NDIFF_8:34

    

     NEIB1: for E be RealNormSpace, x,b be Point of E, N be Neighbourhood of x holds { (z - b) where z be Point of E : z in N } is Neighbourhood of (x - b) & { (z + b) where z be Point of E : z in N } is Neighbourhood of (x + b)

    proof

      let E be RealNormSpace, x,b be Point of E, N be Neighbourhood of x;

      consider g be Real such that

       A1: 0 < g & { y where y be Point of E : ||.(y - x).|| < g } c= N by NFCONT_1:def 1;

      set V = { y where y be Point of E : ||.(y - x).|| < g };

      

       B2: { (z - b) where z be Point of E : z in N } c= the carrier of E

      proof

        let s be object;

        assume s in { (z - b) where z be Point of E : z in N };

        then ex z be Point of E st s = (z - b) & z in N;

        hence s in the carrier of E;

      end;

      

       B3: { (z + b) where z be Point of E : z in N } c= the carrier of E

      proof

        let s be object;

        assume s in { (z + b) where z be Point of E : z in N };

        then ex z be Point of E st s = (z + b) & z in N;

        hence s in the carrier of E;

      end;

      { y where y be Point of E : ||.(y - (x - b)).|| < g } c= { (z - b) where z be Point of E : z in N }

      proof

        let t be object;

        assume t in { y where y be Point of E : ||.(y - (x - b)).|| < g };

        then

        consider y be Point of E such that

         A4: t = y & ||.(y - (x - b)).|| < g;

        (y - (x - b)) = ((y - x) + b) by RLVECT_1: 29

        .= ((y + b) - x) by RLVECT_1:def 3;

        then

         A5: (y + b) in V by A4;

        y = ((y + b) - b) by RLVECT_4: 1;

        hence t in { (z - b) where z be Point of E : z in N } by A1, A4, A5;

      end;

      hence { (z - b) where z be Point of E : z in N } is Neighbourhood of (x - b) by A1, B2, NFCONT_1:def 1;

      { y where y be Point of E : ||.(y - (x + b)).|| < g } c= { (z + b) where z be Point of E : z in N }

      proof

        let t be object;

        assume t in { y where y be Point of E : ||.(y - (x + b)).|| < g };

        then

        consider y be Point of E such that

         A6: t = y & ||.(y - (x + b)).|| < g;

         ||.((y - b) - x).|| < g by A6, RLVECT_1: 27;

        then

         A7: (y - b) in V;

        y = ((y - b) + b) by RLVECT_4: 1;

        hence t in { (z + b) where z be Point of E : z in N } by A1, A6, A7;

      end;

      hence { (z + b) where z be Point of E : z in N } is Neighbourhood of (x + b) by A1, B3, NFCONT_1:def 1;

    end;

    theorem :: NDIFF_8:35

    

     Th1: for E,G be RealNormSpace, F be RealBanachSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, a be Point of E, b be Point of F, c be Point of G, z be Point of [:E, F:] st Z is open & ( dom f) = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & (f `partial`2| Z) is_continuous_on Z & z = [a, b] & z in Z & (f . (a,b)) = c & ( partdiff`2 (f,z)) is one-to-one & (( partdiff`2 (f,z)) " ) is Lipschitzian LinearOperator of G, F holds ex r1,r2 be Real st 0 < r1 & 0 < r2 & [:( Ball (a,r1)), ( cl_Ball (b,r2)):] c= Z & (for x be Point of E st x in ( Ball (a,r1)) holds ex y be Point of F st y in ( cl_Ball (b,r2)) & (f . (x,y)) = c) & (for x be Point of E st x in ( Ball (a,r1)) holds (for y1,y2 be Point of F st y1 in ( cl_Ball (b,r2)) & y2 in ( cl_Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c holds y1 = y2)) & (ex g be PartFunc of E, F st g is_continuous_on ( Ball (a,r1)) & ( dom g) = ( Ball (a,r1)) & ( rng g) c= ( cl_Ball (b,r2)) & (g . a) = b & for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g . x))) = c) & (for g1,g2 be PartFunc of E, F st ( dom g1) = ( Ball (a,r1)) & ( rng g1) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g1 . x))) = c) & ( dom g2) = ( Ball (a,r1)) & ( rng g2) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g2 . x))) = c) holds g1 = g2)

    proof

      let E,G be RealNormSpace, F be RealBanachSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, a be Point of E, b be Point of F, c be Point of G, z be Point of [:E, F:] such that

       A1: Z is open and

       A2: ( dom f) = Z and

       A3: f is_continuous_on Z and

       A4: f is_partial_differentiable_on`2 Z and

       A5: (f `partial`2| Z) is_continuous_on Z and

       A6: z = [a, b] & z in Z and

       A7: (f . (a,b)) = c and

       A8: ( partdiff`2 (f,z)) is one-to-one and

       A9: (( partdiff`2 (f,z)) " ) is Lipschitzian LinearOperator of G, F;

      consider QQ be Lipschitzian LinearOperator of G, F such that

       A10: QQ = (( partdiff`2 (f,z)) " ) by A9;

      reconsider Q = QQ as Point of ( R_NormSpace_of_BoundedLinearOperators (G,F)) by LOPBAN_1:def 9;

      set BLQ = ||.Q.||;

       [a, ( 0. F)] is set by TARSKI: 1;

      then

      reconsider z1 = [a, ( 0. F)] as Point of [:E, F:] by PRVECT_3: 18;

       [( 0. E), b] is set by TARSKI: 1;

      then

      reconsider e0b = [( 0. E), b] as Point of [:E, F:] by PRVECT_3: 18;

      

       A11: ( - e0b) = [( - ( 0. E)), ( - b)] by PRVECT_3: 18

      .= [( 0. E), ( - b)] by RLVECT_1: 12;

      deffunc FHP( Point of [:E, F:]) = ((1 * $1) + ( - e0b));

      consider H be Function of the carrier of [:E, F:], the carrier of [:E, F:] such that

       A12: for p be Point of [:E, F:] holds (H . p) = FHP(p) from FUNCT_2:sch 4;

      

       A13: for x be Point of E, y be Point of F holds (H . (x,y)) = [x, (y - b)]

      proof

        let x be Point of E, y be Point of F;

         [x, y] is set by TARSKI: 1;

        then

        reconsider p = [x, y] as Point of [:E, F:] by PRVECT_3: 18;

        

         A14: (1 * p) = [(1 * x), (1 * y)] by PRVECT_3: 18

        .= [x, (1 * y)] by RLVECT_1:def 8

        .= [x, y] by RLVECT_1:def 8;

        

        thus (H . (x,y)) = ((1 * p) + ( - e0b)) by A12

        .= [(x + ( 0. E)), (y + ( - b))] by A11, A14, PRVECT_3: 18

        .= [x, (y - b)] by RLVECT_1:def 4;

      end;

      

       A15: ( dom H) = the carrier of [:E, F:] by FUNCT_2:def 1;

      deffunc FKP( Point of [:E, F:]) = ((1 * $1) + e0b);

      consider K be Function of the carrier of [:E, F:], the carrier of [:E, F:] such that

       A16: for p be Point of [:E, F:] holds (K . p) = FKP(p) from FUNCT_2:sch 4;

      

       A17: ( dom K) = the carrier of [:E, F:] by FUNCT_2:def 1;

      for p be Point of [:E, F:] holds ((K * H) . p) = p

      proof

        let p be Point of [:E, F:];

        (H . p) = ((1 * p) + ( - e0b)) by A12

        .= (p - e0b) by RLVECT_1:def 8;

        

        then (K . (H . p)) = ((1 * (p - e0b)) + e0b) by A16

        .= ((p - e0b) + e0b) by RLVECT_1:def 8

        .= (p - (e0b - e0b)) by RLVECT_1: 29

        .= (p - ( 0. [:E, F:])) by RLVECT_1: 15

        .= p by RLVECT_1: 13;

        hence ((K * H) . p) = p by A15, FUNCT_1: 13;

      end;

      then

       A18: (K * H) = ( id the carrier of [:E, F:]) by FUNCT_2: 124;

      then

       A19: H is one-to-one & K is onto by FUNCT_2: 23;

      for p be Point of [:E, F:] holds ((H * K) . p) = p

      proof

        let p be Point of [:E, F:];

        (K . p) = ((1 * p) + e0b) by A16

        .= (p + e0b) by RLVECT_1:def 8;

        

        then (H . (K . p)) = ((1 * (p + e0b)) - e0b) by A12

        .= ((p + e0b) - e0b) by RLVECT_1:def 8

        .= (p + (e0b - e0b)) by RLVECT_1: 28

        .= (p + ( 0. [:E, F:])) by RLVECT_1: 15

        .= p by RLVECT_1:def 4;

        hence ((H * K) . p) = p by A17, FUNCT_1: 13;

      end;

      then (H * K) = ( id the carrier of [:E, F:]) by FUNCT_2: 124;

      then K is one-to-one & H is onto by FUNCT_2: 23;

      then ( rng H) = the carrier of [:E, F:] by FUNCT_2:def 3;

      then

       A20: K = (H " ) by A18, FUNCT_2: 23, FUNCT_2: 30;

      reconsider Z1 = (H .: Z) as Subset of [:E, F:];

      

       A21: for x be Point of E, y be Point of F holds [x, (y + b)] in Z iff [x, y] in Z1

      proof

        let x be Point of E, y be Point of F;

        hereby

          assume

           A22: [x, (y + b)] in Z;

           [x, (y + b)] is set by TARSKI: 1;

          then

          reconsider q = [x, (y + b)] as Point of [:E, F:] by PRVECT_3: 18;

          q in the carrier of [:E, F:];

          then

           A23: [x, (y + b)] in ( dom H) by FUNCT_2:def 1;

          (H . [x, (y + b)]) = (H . (x,(y + b)))

          .= [x, ((y + b) - b)] by A13

          .= [x, (y + (b - b))] by RLVECT_1: 28

          .= [x, (y + ( 0. F))] by RLVECT_1: 15

          .= [x, y] by RLVECT_1:def 4;

          hence [x, y] in Z1 by A22, A23, FUNCT_1:def 6;

        end;

        assume [x, y] in Z1;

        then

        consider s be object such that

         A24: s in ( dom H) & s in Z & [x, y] = (H . s) by FUNCT_1:def 6;

        consider x1 be Point of E, y1 be Point of F such that

         A25: s = [x1, y1] by A24, PRVECT_3: 18;

        

         A26: (H . [x1, y1]) = (H . (x1,y1))

        .= [x1, (y1 - b)] by A13;

        then x = x1 & y = (y1 - b) by A24, A25, XTUPLE_0: 1;

        

        then (y + b) = (y1 - (b - b)) by RLVECT_1: 29

        .= (y1 - ( 0. F)) by RLVECT_1: 5

        .= y1 by RLVECT_1: 13;

        hence [x, (y + b)] in Z by A24, A25, A26, XTUPLE_0: 1;

      end;

       [( 0. E), b] is set by TARSKI: 1;

      then

      reconsider e0b = [( 0. E), b] as Point of [:E, F:] by PRVECT_3: 18;

      

       A27: for p be object holds p in Z1 iff p in { (y - e0b) where y be Point of [:E, F:] : y in Z }

      proof

        let p be object;

        

         A28: ( - e0b) = [( - ( 0. E)), ( - b)] by PRVECT_3: 18

        .= [( 0. E), ( - b)] by RLVECT_1: 12;

        hereby

          assume

           A29: p in Z1;

          then

          consider s be Point of E, t be Point of F such that

           A30: p = [s, t] by PRVECT_3: 18;

          

           A31: [s, (t + b)] in Z by A21, A29, A30;

           [s, (t + b)] is set by TARSKI: 1;

          then

          reconsider y = [s, (t + b)] as Point of [:E, F:] by PRVECT_3: 18;

          (y - e0b) = [(s + ( 0. E)), ((t + b) + ( - b))] by A28, PRVECT_3: 18

          .= [s, ((t + b) - b)] by RLVECT_1:def 4

          .= [s, (t + (b - b))] by RLVECT_1: 28

          .= [s, (t + ( 0. F))] by RLVECT_1: 15

          .= p by A30, RLVECT_1:def 4;

          hence p in { (y - e0b) where y be Point of [:E, F:] : y in Z } by A31;

        end;

        assume p in { (y - e0b) where y be Point of [:E, F:] : y in Z };

        then

        consider y be Point of [:E, F:] such that

         A32: p = (y - e0b) & y in Z;

        consider s be Point of E, t be Point of F such that

         A33: y = [s, t] by PRVECT_3: 18;

        

         A34: p = [(s + ( 0. E)), (t + ( - b))] by A28, A32, A33, PRVECT_3: 18

        .= [s, (t - b)] by RLVECT_1:def 4;

        ((t - b) + b) = (t - (b - b)) by RLVECT_1: 29

        .= (t - ( 0. F)) by RLVECT_1: 15

        .= t by RLVECT_1: 13;

        hence p in Z1 by A21, A32, A33, A34;

      end;

      then

       A35: Z1 = { (y - e0b) where y be Point of [:E, F:] : y in Z } by TARSKI: 2;

      

       A36: Z1 is open by A1, A27, OP2, TARSKI: 2;

      defpred FP1[ object, object] means ex x be Point of E, y be Point of F st $1 = [x, y] & $2 = ((f /. [x, (y + b)]) - c);

      

       A37: for p be object st p in Z1 holds ex w be object st w in the carrier of G & FP1[p, w]

      proof

        let p be object;

        assume p in Z1;

        then

        consider x be Point of E, y be Point of F such that

         A38: p = [x, y] by PRVECT_3: 18;

        ((f /. [x, (y + b)]) - c) is Point of G;

        hence thesis by A38;

      end;

      consider f1 be Function of Z1, G such that

       A39: for p be object st p in Z1 holds FP1[p, (f1 . p)] from FUNCT_2:sch 1( A37);

      

       A40: ( rng f1) c= the carrier of G;

      

       A41: ( dom f1) = Z1 by FUNCT_2:def 1;

      then f1 in ( PFuncs (the carrier of [:E, F:],the carrier of G)) by A40, PARTFUN1:def 3;

      then

      reconsider f1 as PartFunc of [:E, F:], G by PARTFUN1: 46;

      

       A42: for x be Point of E, y be Point of F st [x, y] in Z1 holds (f1 . (x,y)) = ((f /. [x, (y + b)]) - c)

      proof

        let x be Point of E, y be Point of F;

        assume [x, y] in Z1;

        then

        consider x0 be Point of E, y0 be Point of F such that

         A43: [x, y] = [x0, y0] & (f1 . [x, y]) = ((f /. [x0, (y0 + b)]) - c) by A39;

        x = x0 & y = y0 by A43, XTUPLE_0: 1;

        hence thesis by A43;

      end;

      defpred FP2[ object, object] means ex x be Point of E, y be Point of F st $1 = [x, y] & $2 = (Q . (f1 . (x,y)));

      

       A44: for p be object st p in Z1 holds ex w be object st w in the carrier of F & FP2[p, w]

      proof

        let p be object;

        assume

         A45: p in Z1;

        then

        consider x be Point of E, y be Point of F such that

         A46: p = [x, y] by PRVECT_3: 18;

        

         A47: (Q . (f1 /. [x, y])) is Point of F;

         [x, y] in ( dom f1) by A45, A46, FUNCT_2:def 1;

        then (f1 /. [x, y]) = (f1 . (x,y)) by PARTFUN1:def 6;

        hence thesis by A46, A47;

      end;

      consider f2 be Function of Z1, F such that

       A48: for p be object st p in Z1 holds FP2[p, (f2 . p)] from FUNCT_2:sch 1( A44);

      

       A49: ( rng f2) c= the carrier of F;

      

       A50: ( dom f2) = Z1 by FUNCT_2:def 1;

      then f2 in ( PFuncs (the carrier of [:E, F:],the carrier of F)) by A49, PARTFUN1:def 3;

      then

      reconsider f2 as PartFunc of [:E, F:], F by PARTFUN1: 46;

      

       A51: for x be Point of E, y be Point of F st [x, y] in Z1 holds (f2 . (x,y)) = (Q . (f1 . (x,y)))

      proof

        let x be Point of E, y be Point of F;

        assume [x, y] in Z1;

        then

        consider x0 be Point of E, y0 be Point of F such that

         A52: [x, y] = [x0, y0] & (f2 . [x, y]) = (Q . (f1 . (x0,y0))) by A48;

        thus thesis by A52;

      end;

      defpred FP3[ object, object] means ex x be Point of E, y be Point of F st $1 = [x, y] & $2 = (y - (f2 /. [x, y]));

      

       A53: for p be object st p in Z1 holds ex w be object st w in the carrier of F & FP3[p, w]

      proof

        let p be object;

        assume p in Z1;

        then

        consider x be Point of E, y be Point of F such that

         A54: p = [x, y] by PRVECT_3: 18;

        (y - (f2 /. [x, y])) is Point of F;

        hence thesis by A54;

      end;

      consider Fai be Function of Z1, F such that

       A55: for p be object st p in Z1 holds FP3[p, (Fai . p)] from FUNCT_2:sch 1( A53);

      

       A56: ( rng Fai) c= the carrier of F;

      

       A57: ( dom Fai) = Z1 by FUNCT_2:def 1;

      then Fai in ( PFuncs (the carrier of [:E, F:],the carrier of F)) by A56, PARTFUN1:def 3;

      then

      reconsider Fai as PartFunc of [:E, F:], F by PARTFUN1: 46;

      

       A58: for x be Point of E, y be Point of F st [x, y] in Z1 holds (Fai . (x,y)) = (y - (f2 /. [x, y]))

      proof

        let x be Point of E, y be Point of F;

        assume [x, y] in Z1;

        then

        consider x0 be Point of E, y0 be Point of F such that

         A59: [x, y] = [x0, y0] & (Fai . [x, y]) = (y0 - (f2 /. [x0, y0])) by A55;

        thus thesis by A59, XTUPLE_0: 1;

      end;

      

       A60: for z0 be Point of [:E, F:] holds for r be Real st z0 in Z1 & 0 < r holds ex s be Real st 0 < s & for z1 be Point of [:E, F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds ||.((Fai /. z1) - (Fai /. z0)).|| < r

      proof

        let z0 be Point of [:E, F:], r be Real;

        assume

         A61: z0 in Z1 & 0 < r;

        reconsider w0 = (z0 + e0b) as Point of [:E, F:];

        consider x0 be Point of E, y0 be Point of F such that

         A62: z0 = [x0, y0] by PRVECT_3: 18;

        

         A63: 0 < (2 * (BLQ + 1)) by XREAL_1: 129;

        consider ww0 be Point of [:E, F:] such that

         A64: z0 = (ww0 - e0b) & ww0 in Z by A35, A61;

        w0 = (ww0 - (e0b - e0b)) by A64, RLVECT_1: 29

        .= (ww0 - ( 0. [:E, F:])) by RLVECT_1: 15

        .= ww0 by RLVECT_1: 13;

        then

        consider s be Real such that

         A65: 0 < s & for w1 be Point of [:E, F:] st w1 in Z & ||.(w1 - w0).|| < s holds ||.((f /. w1) - (f /. w0)).|| < (r / (2 * (BLQ + 1))) by A3, A61, A63, A64, NFCONT_1: 19, XREAL_1: 139;

        reconsider s1 = ( min (s,(r / 2))) as Real;

        

         A66: 0 < (r / 2) by A61, XREAL_1: 215;

        

         A67: s1 <= s & s1 <= (r / 2) by XXREAL_0: 17;

        take s1;

        thus 0 < s1 by A65, A66, XXREAL_0: 15;

        thus for z1 be Point of [:E, F:] st z1 in Z1 & ||.(z1 - z0).|| < s1 holds ||.((Fai /. z1) - (Fai /. z0)).|| < r

        proof

          let z1 be Point of [:E, F:];

          assume

           A68: z1 in Z1 & ||.(z1 - z0).|| < s1;

          reconsider w1 = (z1 + e0b) as Point of [:E, F:];

          consider x1 be Point of E, y1 be Point of F such that

           A69: z1 = [x1, y1] by PRVECT_3: 18;

          consider ww1 be Point of [:E, F:] such that

           A70: z1 = (ww1 - e0b) & ww1 in Z by A35, A68;

          

           A71: w1 = (ww1 - (e0b - e0b)) by A70, RLVECT_1: 29

          .= (ww1 - ( 0. [:E, F:])) by RLVECT_1: 15

          .= ww1 by RLVECT_1: 13;

          (w1 - w0) = (((z1 + e0b) - e0b) - z0) by RLVECT_1: 27

          .= (z1 - z0) by RLVECT_4: 1;

          then

           A72: ||.(w1 - w0).|| < s by A67, A68, XXREAL_0: 2;

          

           A73: (Fai /. z1) = (Fai . (x1,y1)) by A57, A68, A69, PARTFUN1:def 6

          .= (y1 - (f2 /. [x1, y1])) by A58, A68, A69;

          (Fai /. z0) = (Fai . (x0,y0)) by A57, A61, A62, PARTFUN1:def 6

          .= (y0 - (f2 /. [x0, y0])) by A58, A61, A62;

          

          then ((Fai /. z1) - (Fai /. z0)) = (((y1 - (f2 /. [x1, y1])) - y0) + (f2 /. [x0, y0])) by A73, RLVECT_1: 29

          .= ((y1 - ((f2 /. [x1, y1]) + y0)) + (f2 /. [x0, y0])) by RLVECT_1: 27

          .= (((y1 - y0) - (f2 /. [x1, y1])) + (f2 /. [x0, y0])) by RLVECT_1: 27

          .= ((y1 - y0) - ((f2 /. [x1, y1]) - (f2 /. [x0, y0]))) by RLVECT_1: 29;

          then

           A75: ||.((Fai /. z1) - (Fai /. z0)).|| <= ( ||.(y1 - y0).|| + ||.((f2 /. [x1, y1]) - (f2 /. [x0, y0])).||) by NORMSP_1: 3;

          

           A76: (f2 /. [x1, y1]) = (f2 . (x1,y1)) by A50, A68, A69, PARTFUN1:def 6

          .= (Q . (f1 . (x1,y1))) by A51, A68, A69;

          

           A77: (f2 /. [x0, y0]) = (f2 . (x0,y0)) by A50, A61, A62, PARTFUN1:def 6

          .= (Q . (f1 . (x0,y0))) by A51, A61, A62;

           [x1, (y1 + b)] = [(x1 + ( 0. E)), (y1 + b)] by RLVECT_1: 4

          .= w1 by A69, PRVECT_3: 18;

          then

           A79: (f1 . (x1,y1)) = ((f /. w1) - c) by A42, A68, A69;

           [x0, (y0 + b)] = [(x0 + ( 0. E)), (y0 + b)] by RLVECT_1: 4

          .= w0 by A62, PRVECT_3: 18;

          then

           A81: (f1 . (x0,y0)) = ((f /. w0) - c) by A42, A61, A62;

          

           A82: (((f /. w1) - c) - ((f /. w0) - c)) = ((((f /. w1) - c) - (f /. w0)) + c) by RLVECT_1: 29

          .= (((f /. w1) - (c + (f /. w0))) + c) by RLVECT_1: 27

          .= ((((f /. w1) - (f /. w0)) - c) + c) by RLVECT_1: 27

          .= (((f /. w1) - (f /. w0)) - (c - c)) by RLVECT_1: 29

          .= (((f /. w1) - (f /. w0)) - ( 0. G)) by RLVECT_1: 15

          .= ((f /. w1) - (f /. w0)) by RLVECT_1: 13;

          

           A83: QQ is additive;

          

           A84: ((f2 /. [x1, y1]) - (f2 /. [x0, y0])) = ((Q . ((f /. w1) - c)) + (( - 1) * (Q . ((f /. w0) - c)))) by A76, A77, A79, A81, RLVECT_1: 16

          .= ((Q . ((f /. w1) - c)) + (Q . (( - 1) * ((f /. w0) - c)))) by LOPBAN_1:def 5

          .= (Q . (((f /. w1) - c) + (( - 1) * ((f /. w0) - c)))) by A83

          .= (Q . ((f /. w1) - (f /. w0))) by A82, RLVECT_1: 16;

          (BLQ + 0 ) < (BLQ + 1) by XREAL_1: 8;

          then

           A85: (BLQ * ||.((f /. w1) - (f /. w0)).||) <= ((BLQ + 1) * ||.((f /. w1) - (f /. w0)).||) by XREAL_1: 64;

           ||.(Q . ((f /. w1) - (f /. w0))).|| <= (BLQ * ||.((f /. w1) - (f /. w0)).||) by LOPBAN_1: 32;

          then

           A86: ||.((f2 /. [x1, y1]) - (f2 /. [x0, y0])).|| <= ((BLQ + 1) * ||.((f /. w1) - (f /. w0)).||) by A84, A85, XXREAL_0: 2;

          ( - z0) = [( - x0), ( - y0)] by A62, PRVECT_3: 18;

          then (z1 - z0) = [(x1 - x0), (y1 - y0)] by A69, PRVECT_3: 18;

          then ||.(y1 - y0).|| <= ||.(z1 - z0).|| by NORMSP35;

          then ||.(y1 - y0).|| < s1 by A68, XXREAL_0: 2;

          then

           A88: ||.(y1 - y0).|| < (r / 2) by A67, XXREAL_0: 2;

          ((BLQ + 1) * ||.((f /. w1) - (f /. w0)).||) < ((BLQ + 1) * (r / (2 * (BLQ + 1)))) by A65, A70, A71, A72, XREAL_1: 68;

          then ||.((f2 /. [x1, y1]) - (f2 /. [x0, y0])).|| < ((BLQ + 1) * (r / (2 * (BLQ + 1)))) by A86, XXREAL_0: 2;

          then ||.((f2 /. [x1, y1]) - (f2 /. [x0, y0])).|| < (r / 2) by XCMPLX_1: 92;

          then ( ||.(y1 - y0).|| + ||.((f2 /. [x1, y1]) - (f2 /. [x0, y0])).||) < ((r / 2) + (r / 2)) by A88, XREAL_1: 8;

          hence ||.((Fai /. z1) - (Fai /. z0)).|| < r by A75, XXREAL_0: 2;

        end;

      end;

      

       A89: for w0 be Point of [:E, F:] st w0 in Z holds (f * ( reproj2 w0)) is_differentiable_in (w0 `2 )

      proof

        let w0 be Point of [:E, F:];

        assume w0 in Z;

        then f is_partial_differentiable_in`2 w0 by A2, A4;

        hence (f * ( reproj2 w0)) is_differentiable_in (w0 `2 );

      end;

      

       A90: for w0 be Point of [:E, F:] st w0 in Z holds ex N be Neighbourhood of (w0 `2 ) st N c= ( dom (f * ( reproj2 w0))) & ex R be RestFunc of F, G st for w1 be Point of F st w1 in N holds (((f * ( reproj2 w0)) /. w1) - ((f * ( reproj2 w0)) /. (w0 `2 ))) = ((( diff ((f * ( reproj2 w0)),(w0 `2 ))) . (w1 - (w0 `2 ))) + (R /. (w1 - (w0 `2 ))))

      proof

        let w0 be Point of [:E, F:];

        assume w0 in Z;

        then (f * ( reproj2 w0)) is_differentiable_in (w0 `2 ) by A89;

        hence thesis by NDIFF_1:def 7;

      end;

      

       A91: for z0 be Point of [:E, F:] st z0 in Z1 holds (Fai * ( reproj2 z0)) is_differentiable_in (z0 `2 ) & ex L0,I be Point of ( R_NormSpace_of_BoundedLinearOperators (F,F)) st L0 = (Q * ((f `partial`2| Z) /. (z0 + e0b))) & I = ( id the carrier of F) & ( diff ((Fai * ( reproj2 z0)),(z0 `2 ))) = (I - L0)

      proof

        let z0 be Point of [:E, F:];

        assume

         A92: z0 in Z1;

        reconsider w0 = (z0 + e0b) as Point of [:E, F:];

        consider x0 be Point of E, y0 be Point of F such that

         A93: z0 = [x0, y0] by PRVECT_3: 18;

        consider ww0 be Point of [:E, F:] such that

         A94: z0 = (ww0 - e0b) & ww0 in Z by A35, A92;

        

         A95: w0 = (ww0 - (e0b - e0b)) by A94, RLVECT_1: 29

        .= (ww0 - ( 0. [:E, F:])) by RLVECT_1: 15

        .= ww0 by RLVECT_1: 13;

        then

        consider N be Neighbourhood of (w0 `2 ) such that

         A96: N c= ( dom (f * ( reproj2 w0))) & ex R be RestFunc of F, G st for w1 be Point of F st w1 in N holds (((f * ( reproj2 w0)) /. w1) - ((f * ( reproj2 w0)) /. (w0 `2 ))) = ((( diff ((f * ( reproj2 w0)),(w0 `2 ))) . (w1 - (w0 `2 ))) + (R /. (w1 - (w0 `2 )))) by A90, A94;

        consider R be RestFunc of F, G such that

         A97: for w1 be Point of F st w1 in N holds (((f * ( reproj2 w0)) /. w1) - ((f * ( reproj2 w0)) /. (w0 `2 ))) = ((( diff ((f * ( reproj2 w0)),(w0 `2 ))) . (w1 - (w0 `2 ))) + (R /. (w1 - (w0 `2 )))) by A96;

        reconsider L0 = (Q * ((f `partial`2| Z) /. (z0 + e0b))) as Point of ( R_NormSpace_of_BoundedLinearOperators (F,F));

        ( id the carrier of F) is Lipschitzian LinearOperator of F, F by LOPBAN_2: 3;

        then

        reconsider I = ( id the carrier of F) as Point of ( R_NormSpace_of_BoundedLinearOperators (F,F)) by LOPBAN_1:def 9;

        reconsider L1 = (I - L0) as Point of ( R_NormSpace_of_BoundedLinearOperators (F,F));

        reconsider R0 = (Q * R) as RestFunc of F, F by NDIFF_2: 9;

        reconsider R1 = (( - 1) (#) R0) as RestFunc of F, F by NDIFF_1: 29;

        

         A98: w0 = [(x0 + ( 0. E)), (y0 + b)] by A93, PRVECT_3: 18

        .= [x0, (y0 + b)] by RLVECT_1: 4;

        then

         A99: (w0 `1 ) = x0 & (w0 `2 ) = (y0 + b);

        

         A100: (z0 `1 ) = x0 & (z0 `2 ) = y0 by A93;

        set N1 = { (z - b) where z be Point of F : z in N };

        N1 is Neighbourhood of ((y0 + b) - b) by A98, NEIB1;

        then

        reconsider N1 as Neighbourhood of y0 by RLVECT_4: 1;

         A101:

        now

          let yy1 be object;

          assume

           A102: yy1 in N1;

          then

          reconsider y1 = yy1 as Point of F;

          

           A103: (( reproj2 z0) . y1) = [x0, y1] by A100, NDIFF_7:def 2;

          consider w be Point of F such that

           A104: y1 = (w - b) & w in N by A102;

          (( reproj2 w0) . w) in ( dom f) by A96, A104, FUNCT_1: 11;

          then

           A105: [(w0 `1 ), w] in ( dom f) by NDIFF_7:def 2;

          then

          reconsider x0w = [x0, w] as Point of [:E, F:] by A98;

          

           A106: ( - e0b) = [( - ( 0. E)), ( - b)] by PRVECT_3: 18;

           [x0, (w - b)] = [(x0 - ( 0. E)), (w - b)] by RLVECT_1: 13

          .= (x0w - e0b) by A106, PRVECT_3: 18;

          then

           A107: [x0, (w - b)] in Z1 by A2, A35, A98, A105;

          ( dom ( reproj2 z0)) = the carrier of F by FUNCT_2:def 1;

          hence yy1 in ( dom (Fai * ( reproj2 z0))) by A57, A103, A104, A107, FUNCT_1: 11;

        end;

        then

         A108: N1 c= ( dom (Fai * ( reproj2 z0))) by TARSKI:def 3;

         A109:

        now

          let y1 be Point of F;

          assume

           A110: y1 in N1;

          

           A111: (( reproj2 z0) . y1) = [x0, y1] by A100, NDIFF_7:def 2;

          consider w be Point of F such that

           A112: y1 = (w - b) & w in N by A110;

          (( reproj2 w0) . w) in ( dom f) by A96, A112, FUNCT_1: 11;

          then

           A113: [(w0 `1 ), w] in ( dom f) by NDIFF_7:def 2;

          reconsider x0w = [x0, w] as Point of [:E, F:] by A98, A113;

          

           A114: ( - e0b) = [( - ( 0. E)), ( - b)] by PRVECT_3: 18;

           [x0, (w - b)] = [(x0 - ( 0. E)), (w - b)] by RLVECT_1: 13

          .= (x0w - e0b) by A114, PRVECT_3: 18;

          then

           A115: [x0, (w - b)] in Z1 by A2, A35, A98, A113;

          ( dom ( reproj2 z0)) = the carrier of F by FUNCT_2:def 1;

          then

           A116: y1 in ( dom (Fai * ( reproj2 z0))) by A57, A111, A112, A115, FUNCT_1: 11;

          

           A117: ((Fai * ( reproj2 z0)) /. y1) = ((Fai * ( reproj2 z0)) . y1) by A116, PARTFUN1:def 6

          .= (Fai . (x0,y1)) by A111, A116, FUNCT_1: 12

          .= (y1 - (f2 /. [x0, y1])) by A58, A112, A115;

          

           A118: (f2 /. [x0, y1]) = (f2 . (x0,y1)) by A50, A112, A115, PARTFUN1:def 6

          .= (Q . (f1 . (x0,y1))) by A51, A112, A115;

          

           A119: [x0, (y1 + b)] = [x0, w] by A112, RLVECT_4: 1;

          

           A120: [x0, w] = (( reproj2 w0) . w) by A99, NDIFF_7:def 2;

          

           A121: ((f * ( reproj2 w0)) /. w) = ((f * ( reproj2 w0)) . w) by A96, A112, PARTFUN1:def 6

          .= (f . [x0, (y1 + b)]) by A96, A112, A119, A120, FUNCT_1: 12

          .= (f /. [x0, (y1 + b)]) by A98, A113, A119, PARTFUN1:def 6;

          

           A122: (f1 . (x0,y1)) = (((f * ( reproj2 w0)) /. w) - c) by A42, A112, A115, A121;

          

           A123: (( reproj2 z0) . y0) = [x0, y0] by A100, NDIFF_7:def 2;

          

           A124: (y0 + b) in N by A98, NFCONT_1: 4;

          (( reproj2 w0) . (y0 + b)) in ( dom f) by A96, A124, FUNCT_1: 11;

          then

           A125: [(w0 `1 ), (y0 + b)] in ( dom f) by NDIFF_7:def 2;

          reconsider x0v = [x0, (y0 + b)] as Point of [:E, F:] by A98;

          ( dom ( reproj2 z0)) = the carrier of F by FUNCT_2:def 1;

          then

           A126: y0 in ( dom (Fai * ( reproj2 z0))) by A57, A92, A93, A123, FUNCT_1: 11;

          

          then

           A127: ((Fai * ( reproj2 z0)) /. y0) = ((Fai * ( reproj2 z0)) . y0) by PARTFUN1:def 6

          .= (Fai . (x0,y0)) by A123, A126, FUNCT_1: 12

          .= (y0 - (f2 /. [x0, y0])) by A58, A92, A93;

          

           A128: (f2 /. [x0, y0]) = (f2 . (x0,y0)) by A50, A92, A93, PARTFUN1:def 6

          .= (Q . (f1 . (x0,y0))) by A51, A92, A93;

          

           A129: [x0, (y0 + b)] = (( reproj2 w0) . (y0 + b)) by A99, NDIFF_7:def 2;

          

           A130: ((f * ( reproj2 w0)) /. (y0 + b)) = ((f * ( reproj2 w0)) . (y0 + b)) by A96, A124, PARTFUN1:def 6

          .= (f . [x0, (y0 + b)]) by A96, A124, A129, FUNCT_1: 12

          .= (f /. [x0, (y0 + b)]) by A98, A125, PARTFUN1:def 6;

          

           A131: (f1 . (x0,y0)) = (((f * ( reproj2 w0)) /. (w0 `2 )) - c) by A42, A92, A93, A98, A130;

          

           A132: (f1 /. [x0, y1]) = (f1 . (x0,y1)) by A41, A112, A115, PARTFUN1:def 6;

          

           A133: (f1 /. [x0, y0]) = (f1 . (x0,y0)) by A41, A92, A93, PARTFUN1:def 6;

          

           A134: QQ is additive;

          

           A135: ((f2 /. [x0, y1]) - (f2 /. [x0, y0])) = ((Q . (f1 /. [x0, y1])) + (( - 1) * (Q . (f1 /. [x0, y0])))) by A118, A128, A132, A133, RLVECT_1: 16

          .= ((Q . (f1 /. [x0, y1])) + (Q . (( - 1) * (f1 /. [x0, y0])))) by LOPBAN_1:def 5

          .= (Q . ((f1 /. [x0, y1]) + (( - 1) * (f1 /. [x0, y0])))) by A134

          .= (Q . ((f1 /. [x0, y1]) - (f1 /. [x0, y0]))) by RLVECT_1: 16;

          

           A136: (w - (w0 `2 )) = (y1 - y0) by A98, A112, RLVECT_1: 27;

          ((f1 /. [x0, y1]) - (f1 /. [x0, y0])) = (((((f * ( reproj2 w0)) /. w) - c) - ((f * ( reproj2 w0)) /. (w0 `2 ))) + c) by A122, A131, A132, A133, RLVECT_1: 29

          .= ((((f * ( reproj2 w0)) /. w) - (c + ((f * ( reproj2 w0)) /. (w0 `2 )))) + c) by RLVECT_1: 27

          .= (((((f * ( reproj2 w0)) /. w) - ((f * ( reproj2 w0)) /. (w0 `2 ))) - c) + c) by RLVECT_1: 27

          .= (((f * ( reproj2 w0)) /. w) - ((f * ( reproj2 w0)) /. (w0 `2 ))) by RLVECT_4: 1

          .= ((( diff ((f * ( reproj2 w0)),(y0 + b))) . (y1 - y0)) + (R /. (y1 - y0))) by A97, A98, A112, A136;

          then

           A137: ((f2 /. [x0, y1]) - (f2 /. [x0, y0])) = ((Q . (( diff ((f * ( reproj2 w0)),(y0 + b))) . (y1 - y0))) + (Q . (R /. (y1 - y0)))) by A134, A135;

          

           A138: ( diff ((f * ( reproj2 w0)),(y0 + b))) = ( partdiff`2 (f,w0)) by A99, NDIFF_7:def 7

          .= ((f `partial`2| Z) /. (z0 + e0b)) by A4, A94, A95, NDIFF_7:def 11;

          set Q1 = ( modetrans (Q,G,F));

          set df1 = ( modetrans (( diff ((f * ( reproj2 w0)),(y0 + b))),F,G));

          

           A139: (Q1 * df1) is Lipschitzian LinearOperator of F, F by LOPBAN_2: 2;

          

           A140: (Q . (( diff ((f * ( reproj2 w0)),(y0 + b))) . (y1 - y0))) = (Q . (df1 . (y1 - y0))) by LOPBAN_1:def 11

          .= (Q1 . (df1 . (y1 - y0))) by LOPBAN_1:def 11

          .= ((Q * ((f `partial`2| Z) /. (z0 + e0b))) . (y1 - y0)) by A138, A139, LPB2Th4;

          R is total by NDIFF_1:def 5;

          then

           A141: ( dom R) = the carrier of F by PARTFUN1:def 2;

          ( rng R) c= the carrier of G;

          then ( rng R) c= ( dom Q) by FUNCT_2:def 1;

          then

           A142: ( dom (Q * R)) = ( dom R) by RELAT_1: 27;

          

           A143: ( dom (( - 1) (#) (QQ * R))) = the carrier of F by A141, A142, VFUNCT_1:def 4;

          

           A144: (Q . (R /. (y1 - y0))) = (Q . (R . (y1 - y0))) by A141, PARTFUN1:def 6

          .= ((Q * R) . (y1 - y0)) by A141, FUNCT_1: 13

          .= ((QQ * R) /. (y1 - y0)) by A141, A142, PARTFUN1:def 6;

          (((Fai * ( reproj2 z0)) /. y1) - ((Fai * ( reproj2 z0)) /. y0)) = (((y1 - (f2 /. [x0, y1])) - y0) + (f2 /. [x0, y0])) by A117, A127, RLVECT_1: 29

          .= ((y1 - ((f2 /. [x0, y1]) + y0)) + (f2 /. [x0, y0])) by RLVECT_1: 27

          .= (((y1 - y0) - (f2 /. [x0, y1])) + (f2 /. [x0, y0])) by RLVECT_1: 27

          .= ((y1 - y0) - ((L0 . (y1 - y0)) + (R0 /. (y1 - y0)))) by A137, A140, A144, RLVECT_1: 29

          .= (((y1 - y0) - (L0 . (y1 - y0))) - (R0 /. (y1 - y0))) by RLVECT_1: 27

          .= (((y1 - y0) + ( - (L0 . (y1 - y0)))) + (( - 1) * (R0 /. (y1 - y0)))) by RLVECT_1: 16

          .= (((I . (y1 - y0)) - (L0 . (y1 - y0))) + ((( - 1) (#) R0) /. (y1 - y0))) by A143, VFUNCT_1:def 4

          .= ((L1 . (y1 - y0)) + (R1 /. (y1 - y0))) by LOPBAN_1: 40;

          hence (((Fai * ( reproj2 z0)) /. y1) - ((Fai * ( reproj2 z0)) /. (z0 `2 ))) = ((L1 . (y1 - (z0 `2 ))) + (R1 /. (y1 - (z0 `2 )))) by A93;

        end;

        hence

         A145: (Fai * ( reproj2 z0)) is_differentiable_in (z0 `2 ) by A93, A101, NDIFF_1:def 6, TARSKI:def 3;

        take L0, I;

        thus L0 = (Q * ((f `partial`2| Z) /. (z0 + e0b))) & I = ( id the carrier of F) & ( diff ((Fai * ( reproj2 z0)),(z0 `2 ))) = (I - L0) by A93, A108, A109, A145, NDIFF_1:def 7;

      end;

      for z0 be Point of [:E, F:] st z0 in Z1 holds Fai is_partial_differentiable_in`2 z0 by A91;

      then

       A146: Fai is_partial_differentiable_on`2 Z1 by FUNCT_2:def 1;

      

       A147: ( dom (Fai `partial`2| Z1)) = Z1 & for z be Point of [:E, F:] st z in Z1 holds ex L,I be Point of ( R_NormSpace_of_BoundedLinearOperators (F,F)) st L = (Q * ((f `partial`2| Z) /. (z + e0b))) & I = ( id the carrier of F) & ((Fai `partial`2| Z1) /. z) = (I - L)

      proof

        thus ( dom (Fai `partial`2| Z1)) = Z1 by A146, NDIFF_7:def 11;

        let z be Point of [:E, F:];

        assume

         A148: z in Z1;

        then

        consider L,I be Point of ( R_NormSpace_of_BoundedLinearOperators (F,F)) such that

         A149: L = (Q * ((f `partial`2| Z) /. (z + e0b))) & I = ( id the carrier of F) & ( diff ((Fai * ( reproj2 z)),(z `2 ))) = (I - L) by A91;

        take L, I;

        thus L = (Q * ((f `partial`2| Z) /. (z + e0b))) & I = ( id the carrier of F) by A149;

        

        thus ((Fai `partial`2| Z1) /. z) = ( partdiff`2 (Fai,z)) by A146, A148, NDIFF_7:def 11

        .= (I - L) by A149, NDIFF_7:def 7;

      end;

      set FG = (Fai `partial`2| Z1);

      

       A150: for z0 be Point of [:E, F:] holds for r be Real st z0 in Z1 & 0 < r holds ex s be Real st 0 < s & for z1 be Point of [:E, F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds ||.((FG /. z1) - (FG /. z0)).|| < r

      proof

        let z0 be Point of [:E, F:], r be Real;

        reconsider w0 = (z0 + e0b) as Point of [:E, F:];

        assume

         A151: z0 in Z1 & 0 < r;

        then

        consider ww0 be Point of [:E, F:] such that

         A152: z0 = (ww0 - e0b) & ww0 in Z by A35;

        w0 = (ww0 - (e0b - e0b)) by A152, RLVECT_1: 29

        .= (ww0 - ( 0. [:E, F:])) by RLVECT_1: 15

        .= ww0 by RLVECT_1: 13;

        then

        consider s be Real such that

         A153: 0 < s & for w1 be Point of [:E, F:] st w1 in Z & ||.(w1 - w0).|| < s holds ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| < (r / (BLQ + 1)) by A5, A151, A152, NFCONT_1: 19, XREAL_1: 139;

        take s;

        thus 0 < s by A153;

        thus for z1 be Point of [:E, F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds ||.((FG /. z1) - (FG /. z0)).|| < r

        proof

          let z1 be Point of [:E, F:];

          reconsider w1 = (z1 + e0b) as Point of [:E, F:];

          assume

           A154: z1 in Z1 & ||.(z1 - z0).|| < s;

          then

          consider ww1 be Point of [:E, F:] such that

           A155: z1 = (ww1 - e0b) & ww1 in Z by A35;

          

           A156: w1 = (ww1 - (e0b - e0b)) by A155, RLVECT_1: 29

          .= (ww1 - ( 0. [:E, F:])) by RLVECT_1: 15

          .= ww1 by RLVECT_1: 13;

          

           A157: (w1 - w0) = (((z1 + e0b) - e0b) - z0) by RLVECT_1: 27

          .= (z1 - z0) by RLVECT_4: 1;

          consider Lz0,Iz0 be Point of ( R_NormSpace_of_BoundedLinearOperators (F,F)) such that

           A158: Lz0 = (Q * ((f `partial`2| Z) /. (z0 + e0b))) & Iz0 = ( id the carrier of F) & ((Fai `partial`2| Z1) /. z0) = (Iz0 - Lz0) by A147, A151;

          consider Lz1,Iz1 be Point of ( R_NormSpace_of_BoundedLinearOperators (F,F)) such that

           A159: Lz1 = (Q * ((f `partial`2| Z) /. (z1 + e0b))) & Iz1 = ( id the carrier of F) & ((Fai `partial`2| Z1) /. z1) = (Iz1 - Lz1) by A147, A154;

          ((FG /. z1) - (FG /. z0)) = (((Iz1 - Lz1) - Iz0) + Lz0) by A158, A159, RLVECT_1: 29

          .= ((Iz1 - (Iz0 + Lz1)) + Lz0) by RLVECT_1: 27

          .= (((Iz1 - Iz0) - Lz1) + Lz0) by RLVECT_1: 27

          .= ((Iz1 - Iz0) - (Lz1 - Lz0)) by RLVECT_1: 29

          .= (( 0. ( R_NormSpace_of_BoundedLinearOperators (F,F))) - (Lz1 - Lz0)) by A158, A159, RLVECT_1: 15

          .= ( - (Lz1 - Lz0)) by RLVECT_1: 14;

          then

           A160: ||.((FG /. z1) - (FG /. z0)).|| = ||.(Lz1 - Lz0).|| by NORMSP_1: 2;

          (BLQ + 0 ) < (BLQ + 1) by XREAL_1: 8;

          then

           A161: (BLQ * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||) <= ((BLQ + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||) by XREAL_1: 64;

          

           A162: (Q * (( - 1) * ((f `partial`2| Z) /. w0))) = ((1 * Q) * (( - 1) * ((f `partial`2| Z) /. w0))) by RLVECT_1:def 8

          .= ((1 * ( - 1)) * (Q * ((f `partial`2| Z) /. w0))) by LPB2Th11

          .= ( - (Q * ((f `partial`2| Z) /. w0))) by RLVECT_1: 16;

          

           A163: ((Q * ((f `partial`2| Z) /. w1)) - (Q * ((f `partial`2| Z) /. w0))) = (Q * (((f `partial`2| Z) /. w1) + (( - 1) * ((f `partial`2| Z) /. w0)))) by A162, LPB2Th9

          .= (Q * (((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0))) by RLVECT_1: 16;

          set Q1 = ( modetrans (Q,G,F));

          set fp10 = ( modetrans ((((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)),F,G));

          

           A164: (( BoundedLinearOperatorsNorm (G,F)) . Q1) = BLQ by LOPBAN_1:def 11;

           ||.(Lz1 - Lz0).|| <= ((( BoundedLinearOperatorsNorm (G,F)) . Q1) * (( BoundedLinearOperatorsNorm (F,G)) . fp10)) by A158, A159, A163, LOPBAN_2: 2;

          then ||.(Lz1 - Lz0).|| <= (BLQ * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||) by A164, LOPBAN_1:def 11;

          then

           A165: ||.(Lz1 - Lz0).|| <= ((BLQ + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||) by A161, XXREAL_0: 2;

          ((BLQ + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).||) < ((BLQ + 1) * (r / (BLQ + 1))) by A153, A154, A155, A156, A157, XREAL_1: 68;

          then ||.(Lz1 - Lz0).|| < ((BLQ + 1) * (r / (BLQ + 1))) by A165, XXREAL_0: 2;

          hence ||.((FG /. z1) - (FG /. z0)).|| < r by A160, XCMPLX_1: 87;

        end;

      end;

      

       A166: [a, (( 0. F) + b)] in Z by A6, RLVECT_1:def 4;

      then

       A167: [a, ( 0. F)] in Z1 by A21;

      

       A169: (Fai . (a,( 0. F))) = (( 0. F) - (f2 /. [a, ( 0. F)])) by A21, A58, A166;

      

       A168: (Fai . (a,( 0. F))) = ( 0. F)

      proof

        (f2 /. [a, ( 0. F)]) = (f2 . (a,( 0. F))) by A21, A50, A166, PARTFUN1:def 6

        .= (Q . (f1 . (a,( 0. F)))) by A21, A51, A166

        .= (Q . ((f /. [a, (( 0. F) + b)]) - c)) by A21, A42, A166

        .= (Q . ((f /. [a, b]) - c)) by RLVECT_1:def 4

        .= (Q . (c - c)) by A2, A6, A7, PARTFUN1:def 6

        .= (Q . ( 0. G)) by RLVECT_1: 15

        .= ( 0. F) by LOPBAN_7: 3;

        hence thesis by A169, RLVECT_1: 15;

      end;

      reconsider a0F = [a, ( 0. F)] as Point of [:E, F:] by A167;

      consider r10 be Real such that

       A170: 0 < r10 & for s be Point of [:E, F:] st s in Z1 & ||.(s - a0F).|| < r10 holds ||.(((Fai `partial`2| Z1) /. s) - ((Fai `partial`2| Z1) /. a0F)).|| < (1 / 4) by A21, A150, A166;

      consider r11 be Real such that

       A171: 0 < r11 & ( Ball (a0F,r11)) c= Z1 by A21, A36, A166, NORMSP27;

      reconsider r12 = ( min (r10,r11)) as Real;

      

       A173: r12 <= r11 & r12 <= r10 by XXREAL_0: 17;

      then

       A174: ( Ball (a0F,r12)) c= ( Ball (a0F,r11)) by LMBALL1;

       0 < r12 by A170, A171, XXREAL_0: 15;

      then

      consider r1 be Real such that

       A175: 0 < r1 & r1 < r12 & [:( Ball (a,r1)), ( Ball (( 0. F),r1)):] c= ( Ball (a0F,r12)) by NORMSP31;

       [:( Ball (a,r1)), ( Ball (( 0. F),r1)):] c= ( Ball (a0F,r11)) by A174, A175, XBOOLE_1: 1;

      then

       A176: [:( Ball (a,r1)), ( Ball (( 0. F),r1)):] c= Z1 by A171, XBOOLE_1: 1;

      

       A177: for x be Point of [:E, F:] st x in Z1 holds ((Fai `partial`2| Z1) /. x) = ( diff ((Fai * ( reproj2 x)),(x `2 )))

      proof

        let x be Point of [:E, F:];

        assume x in Z1;

        

        hence ((Fai `partial`2| Z1) /. x) = ( partdiff`2 (Fai,x)) by A146, NDIFF_7:def 11

        .= ( diff ((Fai * ( reproj2 x)),(x `2 ))) by NDIFF_7:def 7;

      end;

      

       A179: a in ( Ball (a,r1)) by A175, LMBALL2;

      ( 0. F) in ( Ball (( 0. F),r1)) by A175, LMBALL2;

      then

       A181: [a, ( 0. F)] in [:( Ball (a,r1)), ( Ball (( 0. F),r1)):] by A179, ZFMISC_1: 87;

      then [a, ( 0. F)] in Z1 by A176;

      then

      reconsider a0F = [a, ( 0. F)] as Point of [:E, F:];

      consider La0f,Ia0f be Point of ( R_NormSpace_of_BoundedLinearOperators (F,F)) such that

       A182: La0f = (Q * ((f `partial`2| Z) /. (a0F + e0b))) & Ia0f = ( id the carrier of F) & ((Fai `partial`2| Z1) /. a0F) = (Ia0f - La0f) by A147, A176, A181;

      ( partdiff`2 (f,z)) is Lipschitzian LinearOperator of F, G by LOPBAN_1:def 9;

      then

       A183: ( dom ( partdiff`2 (f,z))) = the carrier of F by FUNCT_2:def 1;

      

       A184: Q = ( modetrans ((( partdiff`2 (f,z)) " ),G,F)) by A10, LOPBAN_1:def 11;

      

       A185: ( partdiff`2 (f,z)) = ( modetrans (( partdiff`2 (f,z)),F,G)) by LOPBAN_1:def 11;

      (a0F + e0b) = [(a + ( 0. E)), (( 0. F) + b)] by PRVECT_3: 18

      .= [a, (( 0. F) + b)] by RLVECT_1: 4

      .= z by A6, RLVECT_1: 4;

      

      then

       A186: La0f = (Q * ( partdiff`2 (f,z))) by A4, A6, A182, NDIFF_7:def 11

      .= Ia0f by A8, A10, A182, A183, A184, A185, FUNCT_1: 39;

      

       A187: ((Fai `partial`2| Z1) /. [a, ( 0. F)]) = ( 0. ( R_NormSpace_of_BoundedLinearOperators (F,F))) by A182, A186, RLVECT_1: 15;

      

       A188: for x be Point of E, y be Point of F st x in ( Ball (a,r1)) & y in ( Ball (( 0. F),r1)) holds ||.((Fai `partial`2| Z1) /. [x, y]).|| < (1 / 4)

      proof

        let x be Point of E, y be Point of F;

        assume x in ( Ball (a,r1)) & y in ( Ball (( 0. F),r1));

        then

         A190: [x, y] in [:( Ball (a,r1)), ( Ball (( 0. F),r1)):] by ZFMISC_1: 87;

        then [x, y] in Z1 by A176;

        then

        reconsider s = [x, y] as Point of [:E, F:];

        s in ( Ball (a0F,r12)) by A175, A190;

        then ex q be Element of [:E, F:] st s = q & ||.(a0F - q).|| < r12;

        then ||.(s - a0F).|| < r12 by NORMSP_1: 7;

        then ||.(s - a0F).|| < r10 by A173, XXREAL_0: 2;

        then ||.(((Fai `partial`2| Z1) /. s) - ((Fai `partial`2| Z1) /. a0F)).|| < (1 / 4) by A170, A176, A190;

        hence thesis by A187, RLVECT_1: 13;

      end;

      reconsider r2 = (r1 / 2) as Real;

       0 < (1 / 2) & 0 < (r1 / 2) by A175, XREAL_1: 215;

      then

      consider ar10 be Real such that

       A191: 0 < ar10 & for s be Point of [:E, F:] st s in Z1 & ||.(s - a0F).|| < ar10 holds ||.((Fai /. s) - (Fai /. a0F)).|| < ((1 / 2) * r2) by A60, A167, XREAL_1: 129;

      consider ar12 be Real such that

       A192: 0 < ar12 & ar12 < ar10 & [:( Ball (a,ar12)), ( Ball (( 0. F),ar12)):] c= ( Ball (a0F,ar10)) by A191, NORMSP31;

      reconsider ar11 = ( min (ar10,ar12)) as Real;

      

       A193: 0 < ar11 by A192, XXREAL_0: 21;

      ar11 <= ar10 & ar11 <= ar12 by XXREAL_0: 17;

      then

       A195: ( Ball (a,ar11)) c= ( Ball (a,ar12)) by LMBALL1;

      reconsider ar1 = ( min (ar11,r1)) as Real;

      

       A196: 0 < ar1 by A175, A193, XXREAL_0: 21;

      

       A197: ar1 <= ar11 & ar1 <= r1 by XXREAL_0: 17;

      then

       A198: ( Ball (a,ar1)) c= ( Ball (a,r1)) by LMBALL1;

      

       A199: ( Ball (a,ar1)) c= ( Ball (a,ar11)) by A197, LMBALL1;

      

       A200: for x be Point of E st x in ( Ball (a,ar1)) holds ||.(Fai /. [x, ( 0. F)]).|| <= ((1 / 2) * r2)

      proof

        let x be Point of E;

        assume

         A201: x in ( Ball (a,ar1));

        ( 0. F) in ( Ball (( 0. F),r1)) by A175, LMBALL2;

        then

         A202: [x, ( 0. F)] in [:( Ball (a,r1)), ( Ball (( 0. F),r1)):] by A198, A201, ZFMISC_1: 87;

        then [x, ( 0. F)] in Z1 by A176;

        then

        reconsider x0F = [x, ( 0. F)] as Point of [:E, F:];

        

         A203: x in ( Ball (a,ar11)) by A199, A201;

        ( 0. F) in ( Ball (( 0. F),ar12)) by A192, LMBALL2;

        then [x, ( 0. F)] in [:( Ball (a,ar12)), ( Ball (( 0. F),ar12)):] by A195, A203, ZFMISC_1: 87;

        then x0F in ( Ball (a0F,ar10)) by A192;

        then ex q be Element of [:E, F:] st q = x0F & ||.(a0F - q).|| < ar10;

        then ||.(x0F - a0F).|| < ar10 by NORMSP_1: 7;

        then

         A204: ||.((Fai /. x0F) - (Fai /. a0F)).|| < ((1 / 2) * r2) by A176, A191, A202;

        (Fai /. a0F) = ( 0. F) by A146, A167, A168, PARTFUN1:def 6;

        hence thesis by A204, RLVECT_1: 13;

      end;

      reconsider r0 = ( min ((r1 / 2),ar1)) as Real;

      

       A205: 0 < (r1 / 2) by A175, XREAL_1: 215;

      then

       A206: 0 < r0 by A196, XXREAL_0: 21;

      

       A207: r0 <= (r1 / 2) by XXREAL_0: 17;

      (r1 / 2) < r1 by A175, XREAL_1: 216;

      then r0 < r1 by A207, XXREAL_0: 2;

      then

       A208: ( Ball (a,r0)) c= ( Ball (a,r1)) by LMBALL1;

      

       A209: for x be Point of E st x in ( Ball (a,r0)) holds ||.(Fai /. [x, ( 0. F)]).|| <= ((1 / 2) * r2)

      proof

        let x be Point of E;

        assume

         A210: x in ( Ball (a,r0));

        r0 <= ar1 by XXREAL_0: 17;

        then ( Ball (a,r0)) c= ( Ball (a,ar1)) by LMBALL1;

        hence ||.(Fai /. [x, ( 0. F)]).|| <= ((1 / 2) * r2) by A200, A210;

      end;

      take r0, r2;

      thus 0 < r0 & 0 < r2 by A196, A205, XXREAL_0: 21;

      

       A211: ( cl_Ball (( 0. F),r2)) c= ( Ball (( 0. F),r1)) by A175, LMBALL1X, XREAL_1: 216;

      then [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] c= [:( Ball (a,r1)), ( Ball (( 0. F),r1)):] by A208, ZFMISC_1: 96;

      then

       A212: [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] c= Z1 by A176, XBOOLE_1: 1;

      

       A213: for x be Point of E st x in ( Ball (a,r0)) holds for y1,y2 be Point of F st y1 in ( cl_Ball (( 0. F),r2)) & y2 in ( cl_Ball (( 0. F),r2)) holds ||.((Fai /. [x, y1]) - (Fai /. [x, y2])).|| <= ((1 / 2) * ||.(y1 - y2).||)

      proof

        let x be Point of E;

        assume

         A214: x in ( Ball (a,r0));

        let y1,y2 be Point of F;

        assume that

         A215: y1 in ( cl_Ball (( 0. F),r2)) and

         A216: y2 in ( cl_Ball (( 0. F),r2));

        

         A217: [.y1, y2.] c= ( cl_Ball (( 0. F),r2)) by A215, A216, LMCLOSE2;

        

         A218: ].y1, y2.[ c= [.y1, y2.] by XBOOLE_1: 36;

         [x, y1] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A214, A215, ZFMISC_1: 87;

        then [x, y1] in Z1 by A212;

        then

        reconsider s = [x, y1] as Point of [:E, F:];

        reconsider Fs = (Fai * ( reproj2 s)) as PartFunc of F, F;

        

         A219: for y be object st y in [.y1, y2.] holds y in ( dom Fs)

        proof

          let y be object;

          assume

           A220: y in [.y1, y2.];

          then [x, y] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A214, A217, ZFMISC_1: 87;

          then

           A221: [x, y] in Z1 by A212;

          

           A222: y in the carrier of F by A220;

          (s `1 ) = x;

          then

           A223: (( reproj2 s) . y) in Z1 by A220, A221, NDIFF_7:def 2;

          y in ( dom ( reproj2 s)) by A222, FUNCT_2:def 1;

          hence y in ( dom Fs) by A146, A223, FUNCT_1: 11;

        end;

        

         A224: for y be Point of F st y in [.y1, y2.] holds Fs is_differentiable_in y

        proof

          let y be Point of F;

          assume y in [.y1, y2.];

          then

           A225: [x, y] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A214, A217, ZFMISC_1: 87;

          then [x, y] in Z1 by A212;

          then

          reconsider s1 = [x, y] as Point of [:E, F:];

          

           A226: (Fai * ( reproj2 s1)) is_differentiable_in (s1 `2 ) by A91, A212, A225;

          (s1 `1 ) = (s `1 );

          hence thesis by A226, REP2;

        end;

        

         A227: for y be Point of F st y in [.y1, y2.] holds Fs is_continuous_in y by A224, NDIFF_1: 44;

        

         A228: for y be Point of F st y in ].y1, y2.[ holds Fs is_differentiable_in y by A218, A224;

        

         A229: for y be Point of F st y in ].y1, y2.[ holds ||.( diff (Fs,y)).|| <= (1 / 2)

        proof

          let y be Point of F;

          assume y in ].y1, y2.[;

          then

           A230: y in [.y1, y2.] by A218;

          then

           A231: y in ( cl_Ball (( 0. F),r2)) by A217;

          

           A232: [x, y] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A214, A217, A230, ZFMISC_1: 87;

          then [x, y] in Z1 by A212;

          then

          reconsider s1 = [x, y] as Point of [:E, F:];

           ||.((Fai `partial`2| Z1) /. [x, y]).|| <= (1 / 4) by A188, A208, A211, A214, A231;

          then

           A233: ||.( diff ((Fai * ( reproj2 s1)),(s1 `2 ))).|| <= (1 / 4) by A177, A212, A232;

          (s1 `1 ) = (s `1 );

          then (Fai * ( reproj2 s1)) = Fs by REP2;

          hence thesis by A233, XXREAL_0: 2;

        end;

        

         A234: ||.((Fs /. y2) - (Fs /. y1)).|| <= ((1 / 2) * ||.(y2 - y1).||) by A219, A227, A228, A229, NDIFF_5: 19, TARSKI:def 3;

         [x, y1] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] & [x, y2] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A214, A215, A216, ZFMISC_1: 87;

        then

         A237: [x, y1] in Z1 & [x, y2] in Z1 by A212;

        

         A235: ( dom ( reproj2 s)) = the carrier of F by FUNCT_2:def 1;

        

         A236: y1 in [.y1, y2.] & y2 in [.y1, y2.] by RLTOPSP1: 68;

        

        then

         A238: (Fs /. y1) = ((Fai * ( reproj2 s)) . y1) by A219, PARTFUN1:def 6

        .= (Fai . (( reproj2 s) . y1)) by A235, FUNCT_1: 13

        .= (Fai . [(s `1 ), y1]) by NDIFF_7:def 2

        .= (Fai /. [x, y1]) by A146, A237, PARTFUN1:def 6;

        

         A239: (Fs /. y2) = ((Fai * ( reproj2 s)) . y2) by A219, A236, PARTFUN1:def 6

        .= (Fai . (( reproj2 s) . y2)) by A235, FUNCT_1: 13

        .= (Fai . [(s `1 ), y2]) by NDIFF_7:def 2

        .= (Fai /. [x, y2]) by A146, A237, PARTFUN1:def 6;

         ||.((Fs /. y2) - (Fs /. y1)).|| = ||.((Fai /. [x, y1]) - (Fai /. [x, y2])).|| by A238, A239, NORMSP_1: 7;

        hence thesis by A234, NORMSP_1: 7;

      end;

      

       A240: for x be Point of E, y be Point of F st x in ( Ball (a,r0)) & y in ( cl_Ball (( 0. F),r2)) holds (Fai . (x,y)) in ( cl_Ball (( 0. F),r2))

      proof

        let x be Point of E, y be Point of F;

        assume

         A241: x in ( Ball (a,r0)) & y in ( cl_Ball (( 0. F),r2));

        then [x, y] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by ZFMISC_1: 87;

        then

         A242: [x, y] in Z1 by A212;

        

         A243: ( 0. F) in ( cl_Ball (( 0. F),r2)) by A205, LMBALL2;

        ex p be Point of F st p = y & ||.(( 0. F) - p).|| <= r2 by A241;

        then ||.(y - ( 0. F)).|| <= r2 by NORMSP_1: 7;

        then

         A244: ((1 / 2) * ||.(y - ( 0. F)).||) <= ((1 / 2) * r2) by XREAL_1: 64;

        

         A245: ||.(Fai /. [x, ( 0. F)]).|| <= ((1 / 2) * r2) by A209, A241;

         ||.((Fai /. [x, y]) - (Fai /. [x, ( 0. F)])).|| <= ((1 / 2) * ||.(y - ( 0. F)).||) by A213, A241, A243;

        then

         A246: ||.((Fai /. [x, y]) - (Fai /. [x, ( 0. F)])).|| <= ((1 / 2) * r2) by A244, XXREAL_0: 2;

        

         A247: (Fai . (x,y)) = (Fai /. [x, y]) by A146, A242, PARTFUN1:def 6;

        then

        reconsider Fxy = (Fai . (x,y)) as Point of F;

        (Fxy - ( 0. F)) = ((Fai /. [x, y]) - ((Fai /. [x, ( 0. F)]) - (Fai /. [x, ( 0. F)]))) by A247, RLVECT_1: 15

        .= (((Fai /. [x, y]) - (Fai /. [x, ( 0. F)])) + (Fai /. [x, ( 0. F)])) by RLVECT_1: 29;

        then

         A248: ||.(Fxy - ( 0. F)).|| <= ( ||.((Fai /. [x, y]) - (Fai /. [x, ( 0. F)])).|| + ||.(Fai /. [x, ( 0. F)]).||) by NORMSP_1:def 1;

        ( ||.((Fai /. [x, y]) - (Fai /. [x, ( 0. F)])).|| + ||.(Fai /. [x, ( 0. F)]).||) <= (((1 / 2) * r2) + ((1 / 2) * r2)) by A245, A246, XREAL_1: 7;

        then ||.(Fxy - ( 0. F)).|| <= r2 by A248, XXREAL_0: 2;

        then ||.(( 0. F) - Fxy).|| <= r2 by NORMSP_1: 7;

        hence (Fai . (x,y)) in ( cl_Ball (( 0. F),r2));

      end;

      

       A249: [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] c= ( dom Fai) by A212, FUNCT_2:def 1;

      

       A251: ( Ball (a,r0)) <> {} by A206, LMBALL2;

      

       A252: ( cl_Ball (( 0. F),r2)) <> {} by A205, LMBALL2;

      

       A253: for y be Point of F st y in ( cl_Ball (( 0. F),r2)) holds for x0 be Point of E st x0 in ( Ball (a,r0)) holds for e be Real st 0 < e holds ex d be Real st 0 < d & for x1 be Point of E st x1 in ( Ball (a,r0)) & ||.(x1 - x0).|| < d holds ||.((Fai /. [x1, y]) - (Fai /. [x0, y])).|| < e

      proof

        let y be Point of F;

        assume

         A254: y in ( cl_Ball (( 0. F),r2));

        let x0 be Point of E;

        assume x0 in ( Ball (a,r0));

        then

         A257: [x0, y] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A254, ZFMISC_1: 87;

        then [x0, y] in Z1 by A212;

        then

        reconsider z0 = [x0, y] as Point of [:E, F:];

        let e be Real;

        assume

         A256: 0 < e;

        consider s be Real such that

         A258: 0 < s & for z1 be Point of [:E, F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds ||.((Fai /. z1) - (Fai /. z0)).|| < e by A60, A212, A256, A257;

        take s;

        thus 0 < s by A258;

        let x1 be Point of E;

        assume

         A259: x1 in ( Ball (a,r0)) & ||.(x1 - x0).|| < s;

        then

         A260: [x1, y] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A254, ZFMISC_1: 87;

        then [x1, y] in Z1 by A212;

        then

        reconsider z1 = [x1, y] as Point of [:E, F:];

        ( - z0) = [( - x0), ( - y)] by PRVECT_3: 18;

        

        then (z1 - z0) = [(x1 - x0), (y - y)] by PRVECT_3: 18

        .= [(x1 - x0), ( 0. F)] by RLVECT_1: 15;

        then ||.(z1 - z0).|| = ||.(x1 - x0).|| by LMNR1;

        hence ||.((Fai /. [x1, y]) - (Fai /. [x0, y])).|| < e by A212, A258, A259, A260;

      end;

      then

      consider Psi be PartFunc of E, F such that

       A262: Psi is_continuous_on ( Ball (a,r0)) & ( dom Psi) = ( Ball (a,r0)) & ( rng Psi) c= ( cl_Ball (( 0. F),r2)) & for x be Point of E st x in ( Ball (a,r0)) holds (Fai . (x,(Psi . x))) = (Psi . x) by A213, A240, A249, A251, A252, FIXPOINT3;

      for z be object holds z in ( cl_Ball (b,r2)) iff z in { (y + b) where y be Point of F : y in ( cl_Ball (( 0. F),r2)) }

      proof

        let z be object;

        hereby

          assume z in ( cl_Ball (b,r2));

          then

          consider p be Point of F such that

           A263: p = z & ||.(b - p).|| <= r2;

          reconsider y = (p - b) as Point of F;

          

           A264: (y + b) = (p - (b - b)) by RLVECT_1: 29

          .= (p - ( 0. F)) by RLVECT_1: 15

          .= p by RLVECT_1: 13;

           ||.(( 0. F) - y).|| = ||.(y - ( 0. F)).|| by NORMSP_1: 7

          .= ||.y.|| by RLVECT_1: 13;

          then ||.(( 0. F) - y).|| <= r2 by A263, NORMSP_1: 7;

          then y in ( cl_Ball (( 0. F),r2));

          hence z in { (y + b) where y be Point of F : y in ( cl_Ball (( 0. F),r2)) } by A263, A264;

        end;

        assume z in { (y + b) where y be Point of F : y in ( cl_Ball (( 0. F),r2)) };

        then

        consider y be Point of F such that

         A265: z = (y + b) & y in ( cl_Ball (( 0. F),r2));

        

         A266: ||.((y + b) - b).|| = ||.(y + (b - b)).|| by RLVECT_1: 28

        .= ||.(y + ( 0. F)).|| by RLVECT_1: 15

        .= ||.y.|| by RLVECT_1: 4;

        ex p be Point of F st p = y & ||.(( 0. F) - p).|| <= r2 by A265;

        then ||.(y - ( 0. F)).|| <= r2 by NORMSP_1: 7;

        then ||.((y + b) - b).|| <= r2 by A266, RLVECT_1: 13;

        then ||.(b - (y + b)).|| <= r2 by NORMSP_1: 7;

        hence z in ( cl_Ball (b,r2)) by A265;

      end;

      then

       A267: ( cl_Ball (b,r2)) = { (y + b) where y be Point of F : y in ( cl_Ball (( 0. F),r2)) } by TARSKI: 2;

      

       A268: (K .: [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):]) c= (K .: Z1) by A212, RELAT_1: 123;

      

       A269: (K .: Z1) = (H " (H .: Z)) by A19, A20, FUNCT_1: 85

      .= Z by A15, A19, FUNCT_1: 94;

      for y be object holds (y in [:( Ball (a,r0)), ( cl_Ball (b,r2)):] iff ex x be object st x in ( dom K) & x in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] & y = (K . x))

      proof

        let y be object;

        hereby

          assume y in [:( Ball (a,r0)), ( cl_Ball (b,r2)):];

          then

          consider d,w be object such that

           A270: d in ( Ball (a,r0)) & w in ( cl_Ball (b,r2)) & y = [d, w] by ZFMISC_1:def 2;

          reconsider d as Point of E by A270;

          reconsider w as Point of F by A270;

          reconsider b2 = (w - b) as Point of F;

           [d, b2] is set by TARSKI: 1;

          then

          reconsider p = [d, b2] as Point of [:E, F:] by PRVECT_3: 18;

          consider y0 be Point of F such that

           A271: w = (y0 + b) & y0 in ( cl_Ball (( 0. F),r2)) by A267, A270;

          

           A272: (w - b) = (y0 + (b - b)) by A271, RLVECT_1: 28

          .= (y0 + ( 0. F)) by RLVECT_1: 15

          .= y0 by RLVECT_1:def 4;

          

          then y = [(d + ( 0. E)), (b2 + b)] by A270, A271, RLVECT_1:def 4

          .= (p + e0b) by PRVECT_3: 18

          .= ((1 * p) + e0b) by RLVECT_1:def 8

          .= (K . p) by A16;

          hence ex x be object st x in ( dom K) & x in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] & y = (K . x) by A17, A270, A271, A272, ZFMISC_1: 87;

        end;

        given x be object such that

         A273: x in ( dom K) & x in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] & y = (K . x);

        reconsider p = x as Point of [:E, F:] by A273;

        

         A274: (K . x) = ((1 * p) + e0b) by A16

        .= (p + e0b) by RLVECT_1:def 8;

        consider z be Point of E, w be Point of F such that

         A275: p = [z, w] by PRVECT_3: 18;

        

         A276: (p + e0b) = [(z + ( 0. E)), (w + b)] by A275, PRVECT_3: 18

        .= [z, (w + b)] by RLVECT_1:def 4;

        

         A277: z in ( Ball (a,r0)) & w in ( cl_Ball (( 0. F),r2)) by A273, A275, ZFMISC_1: 87;

        then (w + b) in ( cl_Ball (b,r2)) by A267;

        hence y in [:( Ball (a,r0)), ( cl_Ball (b,r2)):] by A273, A274, A276, A277, ZFMISC_1: 87;

      end;

      hence [:( Ball (a,r0)), ( cl_Ball (b,r2)):] c= Z by A268, A269, FUNCT_1:def 6;

      deffunc FX11( object) = ((Psi /. $1) + b);

      

       A278: for y be object st y in ( Ball (a,r0)) holds FX11(y) in ( cl_Ball (b,r2))

      proof

        let y be object such that

         A279: y in ( Ball (a,r0));

        reconsider yp = y as Point of E by A279;

        (Psi . yp) in ( rng Psi) by A262, A279, FUNCT_1: 3;

        then (Psi . yp) in ( cl_Ball (( 0. F),r2)) by A262;

        then (Psi /. yp) in ( cl_Ball (( 0. F),r2)) by A262, A279, PARTFUN1:def 6;

        hence FX11(y) in ( cl_Ball (b,r2)) by A267;

      end;

      consider Eta be Function of ( Ball (a,r0)), ( cl_Ball (b,r2)) such that

       A280: for y be object st y in ( Ball (a,r0)) holds (Eta . y) = FX11(y) from FUNCT_2:sch 2( A278);

      

       A281: ( rng Eta) c= ( cl_Ball (b,r2));

      ( cl_Ball (b,r2)) <> {} by A205, LMBALL2;

      then

       A282: ( dom Eta) = ( Ball (a,r0)) by FUNCT_2:def 1;

      ( rng Eta) c= the carrier of F by XBOOLE_1: 1;

      then

      reconsider Eta as PartFunc of E, F by A282, RELSET_1: 4;

      

       A284: for x0 be Point of E holds for r be Real st x0 in ( Ball (a,r0)) & 0 < r holds ex s be Real st 0 < s & for x1 be Point of E st x1 in ( Ball (a,r0)) & ||.(x1 - x0).|| < s holds ||.((Eta /. x1) - (Eta /. x0)).|| < r

      proof

        let x0 be Point of E;

        let r be Real;

        assume

         A285: x0 in ( Ball (a,r0)) & 0 < r;

        then

        consider s be Real such that

         A286: 0 < s & for x1 be Point of E st x1 in ( Ball (a,r0)) & ||.(x1 - x0).|| < s holds ||.((Psi /. x1) - (Psi /. x0)).|| < r by A262, NFCONT_1: 19;

        take s;

        thus 0 < s by A286;

        let x1 be Point of E;

        assume

         A287: x1 in ( Ball (a,r0)) & ||.(x1 - x0).|| < s;

        

        then

         A288: (Eta /. x1) = (Eta . x1) by A282, PARTFUN1:def 6

        .= ((Psi /. x1) + b) by A280, A287;

        (Eta /. x0) = (Eta . x0) by A282, A285, PARTFUN1:def 6

        .= ((Psi /. x0) + b) by A280, A285;

        

        then ((Eta /. x1) - (Eta /. x0)) = ((((Psi /. x1) + b) - b) - (Psi /. x0)) by A288, RLVECT_1: 27

        .= ((Psi /. x1) - (Psi /. x0)) by RLVECT_4: 1;

        hence ||.((Eta /. x1) - (Eta /. x0)).|| < r by A286, A287;

      end;

      

       A290: for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(Eta . x))) = c

      proof

        let x be Point of E;

        assume

         A291: x in ( Ball (a,r0));

        then

         A292: (Psi . x) in ( rng Psi) by A262, FUNCT_1: 3;

        then

        reconsider y = (Psi . x) as Point of F;

        

         A293: y in ( cl_Ball (( 0. F),r2)) & (Fai . (x,y)) = y by A262, A291, A292;

        

         A294: [x, y] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A262, A291, A292, ZFMISC_1: 87;

        then y = (y - (f2 /. [x, y])) by A58, A212, A293;

        then ( - ( - (f2 /. [x, y]))) = ( - ( 0. F)) by RLVECT_1: 9;

        then (f2 /. [x, y]) = ( - ( 0. F)) by RLVECT_1: 17;

        then

         A295: (f2 /. [x, y]) = ( 0. F) by RLVECT_1: 12;

        (f2 . (x,y)) = (f2 /. [x, y]) by A50, A212, A294, PARTFUN1:def 6;

        then

         A296: (Q . (f1 . (x,y))) = ( 0. F) by A51, A212, A294, A295;

        (f1 . (x,y)) = (f1 /. [x, y]) by A41, A212, A294, PARTFUN1:def 6;

        then (f1 . (x,y)) = ( 0. G) by A8, A10, A296, LQ2;

        then ( 0. G) = ((f /. [x, (y + b)]) - c) by A42, A212, A294;

        then

         A297: (f /. [x, (y + b)]) = c by RLVECT_1: 21;

        (y + b) = ((Psi /. x) + b) by A262, A291, PARTFUN1:def 6

        .= (Eta . x) by A280, A291;

        hence thesis by A2, A21, A212, A294, A297, PARTFUN1:def 6;

      end;

      

       A298: for x be Point of E st x in ( Ball (a,r0)) holds ex y be Point of F st y in ( cl_Ball (b,r2)) & (f . (x,y)) = c

      proof

        let x be Point of E;

        assume

         A299: x in ( Ball (a,r0));

        then

         A300: (Eta . x) in ( rng Eta) by A282, FUNCT_1: 3;

        then

        reconsider y = (Eta . x) as Point of F;

        take y;

        thus y in ( cl_Ball (b,r2)) by A281, A300;

        thus (f . (x,y)) = c by A290, A299;

      end;

      

       A301: for x be Point of E st x in ( Ball (a,r0)) holds (for y1,y2 be Point of F st y1 in ( cl_Ball (b,r2)) & y2 in ( cl_Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c holds y1 = y2)

      proof

        let x be Point of E;

        assume

         A302: x in ( Ball (a,r0));

        let y1,y2 be Point of F;

        assume

         A303: y1 in ( cl_Ball (b,r2)) & y2 in ( cl_Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c;

        then

        consider y10 be Point of F such that

         A304: y1 = (y10 + b) & y10 in ( cl_Ball (( 0. F),r2)) by A267;

        consider y20 be Point of F such that

         A305: y2 = (y20 + b) & y20 in ( cl_Ball (( 0. F),r2)) by A267, A303;

        

         A306: [x, y10] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A302, A304, ZFMISC_1: 87;

        

         A307: [x, y20] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A302, A305, ZFMISC_1: 87;

        

         A308: [x, y10] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A302, A304, ZFMISC_1: 87;

        

         A309: [x, y20] in [:( Ball (a,r0)), ( cl_Ball (( 0. F),r2)):] by A302, A305, ZFMISC_1: 87;

        (f . (x,y1)) = (f /. [x, y1]) by A2, A21, A212, A304, A306, PARTFUN1:def 6;

        then ((f /. [x, (y10 + b)]) - c) = ( 0. G) by A303, A304, RLVECT_1: 5;

        then (f1 . (x,y10)) = ( 0. G) by A42, A212, A308;

        then (Q . (f1 . (x,y10))) = ( 0. F) by LOPBAN_7: 3;

        then (f2 . (x,y10)) = ( 0. F) by A51, A212, A308;

        then (f2 /. [x, y10]) = ( 0. F) by A50, A212, A308, PARTFUN1:def 6;

        

        then

         A311: (Fai . (x,y10)) = (y10 - ( 0. F)) by A58, A212, A308

        .= y10 by RLVECT_1: 13;

        (f . (x,y2)) = (f /. [x, y2]) by A2, A21, A212, A305, A307, PARTFUN1:def 6;

        then ((f /. [x, (y20 + b)]) - c) = ( 0. G) by A303, A305, RLVECT_1: 5;

        then (f1 . (x,y20)) = ( 0. G) by A42, A212, A309;

        then (Q . (f1 . (x,y20))) = ( 0. F) by LOPBAN_7: 3;

        then (f2 . (x,y20)) = ( 0. F) by A51, A212, A309;

        then (f2 /. [x, y20]) = ( 0. F) by A50, A212, A309, PARTFUN1:def 6;

        

        then (Fai . (x,y20)) = (y20 - ( 0. F)) by A58, A212, A309

        .= y20 by RLVECT_1: 13;

        hence y1 = y2 by A213, A240, A249, A253, A302, A304, A305, A311, FIXPOINT2;

      end;

      

       A313: a in ( Ball (a,r0)) & b in ( cl_Ball (b,r2)) by A206, A207, LMBALL2;

      

       A314: (Eta . a) in ( rng Eta) by A206, A282, FUNCT_1: 3, LMBALL2;

      (f . (a,(Eta . a))) = c by A206, A290, LMBALL2;

      then

       A315: (Eta . a) = b by A7, A281, A301, A313, A314;

      for Eta1,Eta2 be PartFunc of E, F st ( dom Eta1) = ( Ball (a,r0)) & ( rng Eta1) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(Eta1 . x))) = c) & ( dom Eta2) = ( Ball (a,r0)) & ( rng Eta2) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(Eta2 . x))) = c) holds Eta1 = Eta2

      proof

        let Eta1,Eta2 be PartFunc of E, F;

        assume that

         A316: ( dom Eta1) = ( Ball (a,r0)) & ( rng Eta1) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(Eta1 . x))) = c) and

         A317: ( dom Eta2) = ( Ball (a,r0)) & ( rng Eta2) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(Eta2 . x))) = c);

        for x be object st x in ( dom Eta1) holds (Eta1 . x) = (Eta2 . x)

        proof

          let x0 be object;

          assume

           A318: x0 in ( dom Eta1);

          then

          reconsider x = x0 as Point of E;

          

           A319: (Eta1 . x0) in ( rng Eta1) by A318, FUNCT_1: 3;

          

           A320: (Eta2 . x0) in ( rng Eta2) by A316, A317, A318, FUNCT_1: 3;

          (f . (x,(Eta1 . x))) = c & (f . (x,(Eta2 . x))) = c by A316, A317, A318;

          hence thesis by A301, A316, A317, A318, A319, A320;

        end;

        hence Eta1 = Eta2 by A316, A317, FUNCT_1: 2;

      end;

      hence thesis by A281, A282, A284, A290, A298, A301, A315, NFCONT_1: 19;

    end;

    theorem :: NDIFF_8:36

    for E,G be RealNormSpace, F be RealBanachSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, a be Point of E, b be Point of F, c be Point of G, z be Point of [:E, F:] st Z is open & ( dom f) = Z & f is_continuous_on Z & f is_partial_differentiable_on`2 Z & (f `partial`2| Z) is_continuous_on Z & z = [a, b] & z in Z & (f . (a,b)) = c & ( partdiff`2 (f,z)) is one-to-one & (( partdiff`2 (f,z)) " ) is Lipschitzian LinearOperator of G, F holds ex r1,r2 be Real st 0 < r1 & 0 < r2 & [:( Ball (a,r1)), ( cl_Ball (b,r2)):] c= Z & (for x be Point of E st x in ( Ball (a,r1)) holds ex y be Point of F st y in ( Ball (b,r2)) & (f . (x,y)) = c) & (for x be Point of E st x in ( Ball (a,r1)) holds (for y1,y2 be Point of F st y1 in ( Ball (b,r2)) & y2 in ( Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c holds y1 = y2)) & (ex g be PartFunc of E, F st g is_continuous_on ( Ball (a,r1)) & ( dom g) = ( Ball (a,r1)) & ( rng g) c= ( Ball (b,r2)) & (g . a) = b & for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g . x))) = c) & (for g1,g2 be PartFunc of E, F st ( dom g1) = ( Ball (a,r1)) & ( rng g1) c= ( Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g1 . x))) = c) & ( dom g2) = ( Ball (a,r1)) & ( rng g2) c= ( Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g2 . x))) = c) holds g1 = g2)

    proof

      let E,G be RealNormSpace, F be RealBanachSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, a be Point of E, b be Point of F, c be Point of G, z be Point of [:E, F:] such that

       A1: Z is open and

       A2: ( dom f) = Z and

       A3: f is_continuous_on Z and

       A4: f is_partial_differentiable_on`2 Z and

       A5: (f `partial`2| Z) is_continuous_on Z and

       A6: z = [a, b] & z in Z and

       A7: (f . (a,b)) = c and

       A8: ( partdiff`2 (f,z)) is one-to-one and

       A9: (( partdiff`2 (f,z)) " ) is Lipschitzian LinearOperator of G, F;

      consider r1,r2 be Real such that

       A10: 0 < r1 & 0 < r2 and

       A11: [:( Ball (a,r1)), ( cl_Ball (b,r2)):] c= Z and (for x be Point of E st x in ( Ball (a,r1)) holds ex y be Point of F st y in ( cl_Ball (b,r2)) & (f . (x,y)) = c) and

       A12: for x be Point of E st x in ( Ball (a,r1)) holds (for y1,y2 be Point of F st y1 in ( cl_Ball (b,r2)) & y2 in ( cl_Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c holds y1 = y2) and

       A13: (ex g be PartFunc of E, F st g is_continuous_on ( Ball (a,r1)) & ( dom g) = ( Ball (a,r1)) & ( rng g) c= ( cl_Ball (b,r2)) & (g . a) = b & for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g . x))) = c) & (for g1,g2 be PartFunc of E, F st ( dom g1) = ( Ball (a,r1)) & ( rng g1) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g1 . x))) = c) & ( dom g2) = ( Ball (a,r1)) & ( rng g2) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g2 . x))) = c) holds g1 = g2) by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th1;

      consider g be PartFunc of E, F such that

       A14: g is_continuous_on ( Ball (a,r1)) & ( dom g) = ( Ball (a,r1)) & ( rng g) c= ( cl_Ball (b,r2)) & (g . a) = b & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g . x))) = c) & (for g1,g2 be PartFunc of E, F st ( dom g1) = ( Ball (a,r1)) & ( rng g1) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g1 . x))) = c) & ( dom g2) = ( Ball (a,r1)) & ( rng g2) c= ( cl_Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g2 . x))) = c) holds g1 = g2) by A13;

      a in ( Ball (a,r1)) by A10, LMBALL2;

      then (g | ( Ball (a,r1))) is_continuous_in a by A14, NFCONT_1:def 7;

      then

      consider r3 be Real such that

       A15: 0 < r3 & for x1 be Point of E st x1 in ( dom g) & ||.(x1 - a).|| < r3 holds ||.((g /. x1) - (g /. a)).|| < r2 by A10, A14, NFCONT_1: 7;

      reconsider r0 = ( min (r1,r3)) as Real;

      

       A16: 0 < r0 by A10, A15, XXREAL_0: 21;

      

       A17: r0 <= r1 & r0 <= r3 by XXREAL_0: 17;

      take r0, r2;

      thus 0 < r0 & 0 < r2 by A10, A15, XXREAL_0: 21;

      

       A18: ( Ball (a,r0)) c= ( Ball (a,r1)) & ( Ball (a,r0)) c= ( Ball (a,r3)) by A17, LMBALL1;

      then

       A19: [:( Ball (a,r0)), ( cl_Ball (b,r2)):] c= [:( Ball (a,r1)), ( cl_Ball (b,r2)):] by ZFMISC_1: 96;

      

       A20: for x be Point of E st x in ( Ball (a,r0)) holds ex y be Point of F st y in ( Ball (b,r2)) & (f . (x,y)) = c

      proof

        let x be Point of E;

        assume

         A21: x in ( Ball (a,r0));

        

         A22: (g /. x) = (g . x) by A14, A18, A21, PARTFUN1:def 6;

        take y = (g /. x);

        x in ( Ball (a,r3)) by A18, A21;

        then ex q be Element of E st x = q & ||.(a - q).|| < r3;

        then ||.(x - a).|| < r3 by NORMSP_1: 7;

        then ||.((g /. x) - (g /. a)).|| < r2 by A14, A15, A18, A21;

        then

         A23: ||.((g /. a) - (g /. x)).|| < r2 by NORMSP_1: 7;

        (g /. a) = b by A10, A14, LMBALL2, PARTFUN1:def 6;

        hence y in ( Ball (b,r2)) by A23;

        thus (f . (x,y)) = c by A14, A18, A21, A22;

      end;

      

       A24: for x be Point of E st x in ( Ball (a,r0)) holds (for y1,y2 be Point of F st y1 in ( Ball (b,r2)) & y2 in ( Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c holds y1 = y2)

      proof

        let x be Point of E;

        assume

         A25: x in ( Ball (a,r0));

        let y1,y2 be Point of F;

        assume

         A26: y1 in ( Ball (b,r2)) & y2 in ( Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c;

        ( Ball (b,r2)) c= ( cl_Ball (b,r2)) by LMBALL1;

        hence thesis by A12, A18, A25, A26;

      end;

      reconsider g1 = (g | ( Ball (a,r0))) as PartFunc of E, F;

      g is_continuous_on ( Ball (a,r0)) by A14, A18, NFCONT_1: 23;

      then

       A27: g1 is_continuous_on ( Ball (a,r0)) by NFCONT_1: 21;

      

       A28: ( dom g1) = ( Ball (a,r0)) by A14, A17, LMBALL1, RELAT_1: 62;

      

       A29: for y be object st y in ( rng g1) holds y in ( Ball (b,r2))

      proof

        let y be object;

        assume y in ( rng g1);

        then

        consider x be object such that

         A30: x in ( dom g1) & y = (g1 . x) by FUNCT_1:def 3;

        reconsider x as Point of E by A30;

        

         A31: (g /. x) = (g . x) by A14, A18, A28, A30, PARTFUN1:def 6;

        

         A32: (g1 . x) = (g . x) by A30, FUNCT_1: 47;

        x in ( Ball (a,r3)) by A18, A28, A30;

        then ex q be Element of E st x = q & ||.(a - q).|| < r3;

        then ||.(x - a).|| < r3 by NORMSP_1: 7;

        then ||.((g /. x) - (g /. a)).|| < r2 by A14, A15, A18, A28, A30;

        then

         A33: ||.((g /. a) - (g /. x)).|| < r2 by NORMSP_1: 7;

        (g /. a) = b by A10, A14, LMBALL2, PARTFUN1:def 6;

        hence y in ( Ball (b,r2)) by A30, A31, A32, A33;

      end;

      

       A34: (g1 . a) = b by A14, A16, A28, FUNCT_1: 47, LMBALL2;

      

       A35: for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(g1 . x))) = c

      proof

        let x be Point of E;

        assume

         A36: x in ( Ball (a,r0));

        

        hence (f . (x,(g1 . x))) = (f . (x,(g . x))) by A28, FUNCT_1: 47

        .= c by A14, A18, A36;

      end;

      for g1,g2 be PartFunc of E, F st ( dom g1) = ( Ball (a,r0)) & ( rng g1) c= ( Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(g1 . x))) = c) & ( dom g2) = ( Ball (a,r0)) & ( rng g2) c= ( Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(g2 . x))) = c) holds g1 = g2

      proof

        let g1,g2 be PartFunc of E, F;

        assume

         A38: ( dom g1) = ( Ball (a,r0)) & ( rng g1) c= ( Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(g1 . x))) = c) & ( dom g2) = ( Ball (a,r0)) & ( rng g2) c= ( Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r0)) holds (f . (x,(g2 . x))) = c);

        for x be object st x in ( dom g1) holds (g1 . x) = (g2 . x)

        proof

          let x0 be object;

          assume

           A39: x0 in ( dom g1);

          then

          reconsider x = x0 as Point of E;

          

           A40: (g1 . x0) in ( rng g1) by A39, FUNCT_1: 3;

          then

          reconsider y1 = (g1 . x0) as Point of F;

          

           A41: (g2 . x0) in ( rng g2) by A38, A39, FUNCT_1: 3;

          then

          reconsider y2 = (g2 . x0) as Point of F;

          y1 in ( Ball (b,r2)) & y2 in ( Ball (b,r2)) & (f . (x,y1)) = c & (f . (x,y2)) = c by A38, A39, A40, A41;

          hence thesis by A24, A38, A39;

        end;

        hence g1 = g2 by A38, FUNCT_1: 2;

      end;

      hence thesis by A11, A19, A20, A24, A27, A28, A29, A34, A35, TARSKI:def 3, XBOOLE_1: 1;

    end;