ndiff_9.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_9:1

    

     LMDIFF: for E,F be RealNormSpace, f be PartFunc of E, F, Z be Subset of E, z be Point of E st Z is open & z in Z & Z c= ( dom f) & f is_differentiable_in z holds (f | Z) is_differentiable_in z & ( diff (f,z)) = ( diff ((f | Z),z))

    proof

      let E,F be RealNormSpace, f be PartFunc of E, F, Z be Subset of E, z be Point of E;

      assume

       A1: Z is open & z in Z & Z c= ( dom f) & f is_differentiable_in z;

      then

      consider N be Neighbourhood of z such that

       A2: N c= ( dom f) & ex R be RestFunc of E, F st for x be Point of E st x in N holds ((f /. x) - (f /. z)) = ((( diff (f,z)) . (x - z)) + (R /. (x - z))) by NDIFF_1:def 7;

      consider r be Real such that

       A3: r > 0 & ( Ball (z,r)) c= Z by A1, NDIFF_8: 20;

      ( Ball (z,r)) = { y where y be Point of E : ||.(y - z).|| < r } by NDIFF_8: 17;

      then Z is Neighbourhood of z by A3, NFCONT_1:def 1;

      then

      reconsider NZ = (N /\ Z) as Neighbourhood of z by NDIFF_5: 8;

      

       A4: ( dom (f | Z)) = (( dom f) /\ Z) by RELAT_1: 61;

      

       A5: (N /\ Z) c= (( dom f) /\ Z) by A2, XBOOLE_1: 26;

      consider R be RestFunc of E, F such that

       A6: for x be Point of E st x in N holds ((f /. x) - (f /. z)) = ((( diff (f,z)) . (x - z)) + (R /. (x - z))) by A2;

      

       A7: for x be Point of E st x in NZ holds (((f | Z) /. x) - ((f | Z) /. z)) = ((( diff (f,z)) . (x - z)) + (R /. (x - z)))

      proof

        let x be Point of E;

        assume

         A8: x in NZ;

        then

         A9: x in N & x in Z by XBOOLE_0:def 4;

        

        then

         A15: (f /. x) = (f . x) by A2, PARTFUN1:def 6

        .= ((f | Z) . x) by A9, FUNCT_1: 49

        .= ((f | Z) /. x) by A4, A5, A8, PARTFUN1:def 6;

        

         A14: z in NZ by NFCONT_1: 4;

        (f /. z) = (f . z) by A1, PARTFUN1:def 6

        .= ((f | Z) . z) by A1, FUNCT_1: 49

        .= ((f | Z) /. z) by A4, A5, A14, PARTFUN1:def 6;

        hence thesis by A6, A9, A15;

      end;

      hence (f | Z) is_differentiable_in z by A2, A4, NDIFF_1:def 6, XBOOLE_1: 26;

      hence ( diff (f,z)) = ( diff ((f | Z),z)) by A4, A5, A7, NDIFF_1:def 7;

    end;

    theorem :: NDIFF_9:2

    

     LMPDIFF: for E,F,G be RealNormSpace, f be PartFunc of [:E, F:], G, Z be Subset of [:E, F:], z be Point of [:E, F:] st Z is open & z in Z & Z c= ( dom f) holds (f is_partial_differentiable_in`1 z implies ((f | Z) is_partial_differentiable_in`1 z & ( partdiff`1 (f,z)) = ( partdiff`1 ((f | Z),z)))) & (f is_partial_differentiable_in`2 z implies ((f | Z) is_partial_differentiable_in`2 z & ( partdiff`2 (f,z)) = ( partdiff`2 ((f | Z),z))))

    proof

      let E,F,G be RealNormSpace, f be PartFunc of [:E, F:], G, Z be Subset of [:E, F:], z be Point of [:E, F:];

      assume

       A1: Z is open & z in Z & Z c= ( dom f);

      

       A2: ex x1 be Point of E, x2 be Point of F st z = [x1, x2] by PRVECT_3: 18;

      thus f is_partial_differentiable_in`1 z implies ((f | Z) is_partial_differentiable_in`1 z & ( partdiff`1 (f,z)) = ( partdiff`1 ((f | Z),z)))

      proof

        assume

         A4: f is_partial_differentiable_in`1 z;

        set g = (f * ( reproj1 z));

        consider N be Neighbourhood of (z `1 ) such that

         A6: N c= ( dom g) & ex R be RestFunc of E, G st for x be Point of E st x in N holds ((g /. x) - (g /. (z `1 ))) = ((( partdiff`1 (f,z)) . (x - (z `1 ))) + (R /. (x - (z `1 )))) by A4, NDIFF_1:def 7;

        consider R be RestFunc of E, G such that

         A7: for x be Point of E st x in N holds ((g /. x) - (g /. (z `1 ))) = ((( partdiff`1 (f,z)) . (x - (z `1 ))) + (R /. (x - (z `1 )))) by A6;

        set h = ((f | Z) * ( reproj1 z));

        

         A9: (( reproj1 z) . (z `1 )) = [(z `1 ), (z `2 )] by NDIFF_7:def 1

        .= z by A2;

        consider r1 be Real such that

         A10: r1 > 0 & ( Ball (z,r1)) c= Z by A1, NDIFF_8: 20;

        

         A11: ( Ball (z,r1)) = { y where y be Point of [:E, F:] : ||.(y - z).|| < r1 } by NDIFF_8: 17;

        consider r2 be Real such that

         A13: r2 > 0 & { y where y be Point of E : ||.(y - (z `1 )).|| < r2 } c= N by NFCONT_1:def 1;

        set r = ( min (r1,r2));

        

         A14: 0 < r & r <= r1 & r <= r2 by A10, A13, XXREAL_0: 15, XXREAL_0: 17;

        set M = ( Ball ((z `1 ),r));

        

         A15: M = { y where y be Point of E : ||.(y - (z `1 )).|| < r } by NDIFF_8: 17;

        then

        reconsider M as Neighbourhood of (z `1 ) by A14, NFCONT_1:def 1;

        

         A17: { y where y be Point of E : ||.(y - (z `1 )).|| < r2 } = ( Ball ((z `1 ),r2)) by NDIFF_8: 17;

        

         A18: M c= ( Ball ((z `1 ),r2)) by A14, NDIFF_8: 15;

        

         A19: M c= N & for x be Point of E st x in M holds (( reproj1 z) . x) in Z

        proof

          thus M c= N by A13, A17, A18, XBOOLE_1: 1;

          let x be Point of E;

          assume x in M;

          then

           A20: ex y be Point of E st x = y & ||.(y - (z `1 )).|| < r by A15;

          

           A21: (( reproj1 z) . x) = [x, (z `2 )] by NDIFF_7:def 1;

          ( - z) = [( - (z `1 )), ( - (z `2 ))] by A2, PRVECT_3: 18;

          

          then ((( reproj1 z) . x) - z) = [(x - (z `1 )), ((z `2 ) - (z `2 ))] by A21, PRVECT_3: 18

          .= [(x - (z `1 )), ( 0. F)] by RLVECT_1: 15;

          then ||.((( reproj1 z) . x) - z).|| = ||.(x - (z `1 )).|| by NDIFF_8: 2;

          then ||.((( reproj1 z) . x) - z).|| < r1 by A14, A20, XXREAL_0: 2;

          then (( reproj1 z) . x) in { y where y be Point of [:E, F:] : ||.(y - z).|| < r1 };

          hence (( reproj1 z) . x) in Z by A10, A11;

        end;

        

         A22: ( dom ( reproj1 z)) = the carrier of E by FUNCT_2:def 1;

        

         A23: ( dom (f | Z)) = Z by A1, RELAT_1: 62;

        

         A24: M c= ( dom h)

        proof

          let x be object;

          assume

           A25: x in M;

          then (( reproj1 z) . x) in Z by A19;

          hence x in ( dom h) by A22, A23, A25, FUNCT_1: 11;

        end;

        

         A27: for x be Point of E st x in M holds ((h /. x) - (h /. (z `1 ))) = ((( partdiff`1 (f,z)) . (x - (z `1 ))) + (R /. (x - (z `1 ))))

        proof

          let x be Point of E;

          assume

           A28: x in M;

          then

           A29: x in N by A19;

          

           A30: (z `1 ) in N by NFCONT_1: 4;

          

           A31: (z `1 ) in M by NFCONT_1: 4;

          

           A33: (h /. x) = (h . x) by A24, A28, PARTFUN1:def 6

          .= ((f | Z) . (( reproj1 z) . x)) by A22, FUNCT_1: 13

          .= (f . (( reproj1 z) . x)) by A19, A28, FUNCT_1: 49

          .= ((f * ( reproj1 z)) . x) by A22, FUNCT_1: 13

          .= (g /. x) by A6, A29, PARTFUN1:def 6;

          (h /. (z `1 )) = (h . (z `1 )) by A24, A31, PARTFUN1:def 6

          .= ((f | Z) . (( reproj1 z) . (z `1 ))) by A22, FUNCT_1: 13

          .= (f . (( reproj1 z) . (z `1 ))) by A1, A9, FUNCT_1: 49

          .= ((f * ( reproj1 z)) . (z `1 )) by A22, FUNCT_1: 13

          .= (g /. (z `1 )) by A6, A30, PARTFUN1:def 6;

          hence thesis by A7, A19, A28, A33;

        end;

        then

         A35: h is_differentiable_in (z `1 ) by A24, NDIFF_1:def 6;

        thus (f | Z) is_partial_differentiable_in`1 z by A24, A27, NDIFF_1:def 6;

        thus ( partdiff`1 ((f | Z),z)) = ( partdiff`1 (f,z)) by A35, A24, A27, NDIFF_1:def 7;

      end;

      assume

       A38: f is_partial_differentiable_in`2 z;

      set g = (f * ( reproj2 z));

      consider N be Neighbourhood of (z `2 ) such that

       A40: N c= ( dom g) & ex R be RestFunc of F, G st for x be Point of F st x in N holds ((g /. x) - (g /. (z `2 ))) = ((( partdiff`2 (f,z)) . (x - (z `2 ))) + (R /. (x - (z `2 )))) by A38, NDIFF_1:def 7;

      consider R be RestFunc of F, G such that

       A41: for x be Point of F st x in N holds ((g /. x) - (g /. (z `2 ))) = ((( partdiff`2 (f,z)) . (x - (z `2 ))) + (R /. (x - (z `2 )))) by A40;

      set h = ((f | Z) * ( reproj2 z));

      

       A43: (( reproj2 z) . (z `2 )) = [(z `1 ), (z `2 )] by NDIFF_7:def 2

      .= z by A2;

      consider r1 be Real such that

       A44: r1 > 0 & ( Ball (z,r1)) c= Z by A1, NDIFF_8: 20;

      

       A45: ( Ball (z,r1)) = { y where y be Point of [:E, F:] : ||.(y - z).|| < r1 } by NDIFF_8: 17;

      consider r2 be Real such that

       A47: r2 > 0 & { y where y be Point of F : ||.(y - (z `2 )).|| < r2 } c= N by NFCONT_1:def 1;

      set r = ( min (r1,r2));

      

       A48: 0 < r & r <= r1 & r <= r2 by A44, A47, XXREAL_0: 15, XXREAL_0: 17;

      set M = ( Ball ((z `2 ),r));

      

       A49: M = { y where y be Point of F : ||.(y - (z `2 )).|| < r } by NDIFF_8: 17;

      then

      reconsider M as Neighbourhood of (z `2 ) by A48, NFCONT_1:def 1;

      

       A51: { y where y be Point of F : ||.(y - (z `2 )).|| < r2 } = ( Ball ((z `2 ),r2)) by NDIFF_8: 17;

      

       A52: M c= ( Ball ((z `2 ),r2)) by A48, NDIFF_8: 15;

      

       A53: M c= N & for x be Point of F st x in M holds (( reproj2 z) . x) in Z

      proof

        thus M c= N by A47, A51, A52, XBOOLE_1: 1;

        let x be Point of F;

        assume x in M;

        then

         A54: ex y be Point of F st x = y & ||.(y - (z `2 )).|| < r by A49;

        

         A55: (( reproj2 z) . x) = [(z `1 ), x] by NDIFF_7:def 2;

        ( - z) = [( - (z `1 )), ( - (z `2 ))] by A2, PRVECT_3: 18;

        

        then ((( reproj2 z) . x) - z) = [((z `1 ) - (z `1 )), (x - (z `2 ))] by A55, PRVECT_3: 18

        .= [( 0. E), (x - (z `2 ))] by RLVECT_1: 15;

        then ||.((( reproj2 z) . x) - z).|| = ||.(x - (z `2 )).|| by NDIFF_8: 3;

        then ||.((( reproj2 z) . x) - z).|| < r1 by A48, A54, XXREAL_0: 2;

        then (( reproj2 z) . x) in { y where y be Point of [:E, F:] : ||.(y - z).|| < r1 };

        hence (( reproj2 z) . x) in Z by A44, A45;

      end;

      

       A56: ( dom ( reproj2 z)) = the carrier of F by FUNCT_2:def 1;

      

       A57: ( dom (f | Z)) = Z by A1, RELAT_1: 62;

      

       A58: M c= ( dom h)

      proof

        let x be object;

        assume

         A59: x in M;

        then (( reproj2 z) . x) in Z by A53;

        hence x in ( dom h) by A56, A57, A59, FUNCT_1: 11;

      end;

      

       A61: for x be Point of F st x in M holds ((h /. x) - (h /. (z `2 ))) = ((( partdiff`2 (f,z)) . (x - (z `2 ))) + (R /. (x - (z `2 ))))

      proof

        let x be Point of F;

        assume

         A62: x in M;

        then

         A63: x in N by A53;

        

         A64: (z `2 ) in N by NFCONT_1: 4;

        

         A65: (z `2 ) in M by NFCONT_1: 4;

        

         A67: (h /. x) = (h . x) by A58, A62, PARTFUN1:def 6

        .= ((f | Z) . (( reproj2 z) . x)) by A56, FUNCT_1: 13

        .= (f . (( reproj2 z) . x)) by A53, A62, FUNCT_1: 49

        .= ((f * ( reproj2 z)) . x) by A56, FUNCT_1: 13

        .= (g /. x) by A40, A63, PARTFUN1:def 6;

        (h /. (z `2 )) = (h . (z `2 )) by A58, A65, PARTFUN1:def 6

        .= ((f | Z) . (( reproj2 z) . (z `2 ))) by A56, FUNCT_1: 13

        .= (f . (( reproj2 z) . (z `2 ))) by A1, A43, FUNCT_1: 49

        .= ((f * ( reproj2 z)) . (z `2 )) by A56, FUNCT_1: 13

        .= (g /. (z `2 )) by A40, A64, PARTFUN1:def 6;

        hence thesis by A41, A53, A62, A67;

      end;

      hence (f | Z) is_partial_differentiable_in`2 z by A58, NDIFF_1:def 6;

      h is_differentiable_in (z `2 ) by A58, A61, NDIFF_1:def 6;

      hence ( partdiff`2 ((f | Z),z)) = ( partdiff`2 (f,z)) by A58, A61, NDIFF_1:def 7;

    end;

    theorem :: NDIFF_9:3

    

     LmTh47: for X,E,G,F be RealNormSpace, BL be BilinearOperator of E, F, G, f be PartFunc of X, E, g be PartFunc of X, F, S be Subset of X st BL is_continuous_on the carrier of [:E, F:] & S c= ( dom f) & S c= ( dom g) & (for s be Point of X st s in S holds f is_continuous_in s) & (for s be Point of X st s in S holds g is_continuous_in s) holds ex H be PartFunc of X, G st ( dom H) = S & (for s be Point of X st s in S holds (H . s) = (BL . ((f . s),(g . s)))) & H is_continuous_on S

    proof

      let X,E,G,F be RealNormSpace, BL be BilinearOperator of E, F, G, f be PartFunc of X, E, g be PartFunc of X, F, S be Subset of X;

      assume that

       A1: BL is_continuous_on the carrier of [:E, F:] and

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

       A3: (for s be Point of X st s in S holds f is_continuous_in s) and

       A4: (for s be Point of X st s in S holds g is_continuous_in s);

      defpred P1[ object, object] means ex t be Point of X st t = $1 & $2 = (BL . ((f . t),(g . t)));

      

       A5: for x be object st x in S holds ex y be object st y in the carrier of G & P1[x, y]

      proof

        let x be object;

        assume

         A6: x in S;

        then

        reconsider t = x as Point of X;

        take y = (BL . ((f . t),(g . t)));

        

         A7: (f . t) in ( rng f) & (g . t) in ( rng g) by A2, A6, FUNCT_1: 3;

        then

        reconsider p = (f . t) as Point of E;

        reconsider q = (g . t) as Point of F by A7;

         [p, q] is set by TARSKI: 1;

        then [p, q] is Point of [:E, F:] by PRVECT_3: 18;

        hence y in the carrier of G & P1[x, y] by FUNCT_2: 5;

      end;

      consider H be Function of S, G such that

       A8: for z be object st z in S holds P1[z, (H . z)] from FUNCT_2:sch 1( A5);

      

       A9: ( dom H) = S by FUNCT_2:def 1;

      ( rng H) c= the carrier of G;

      then H in ( PFuncs (the carrier of X,the carrier of G)) by A9, PARTFUN1:def 3;

      then

      reconsider H as PartFunc of X, G by PARTFUN1: 46;

      take H;

      thus

       A12: ( dom H) = S by FUNCT_2:def 1;

      thus

       A13: for s be Point of X st s in S holds (H . s) = (BL . ((f . s),(g . s)))

      proof

        let s be Point of X;

        assume s in S;

        then ex t be Point of X st t = s & (H . s) = (BL . ((f . t),(g . t))) by A8;

        hence thesis;

      end;

      for x0 be Point of X holds for r be Real st x0 in S & 0 < r holds ex pq be Real st 0 < pq & for x1 be Point of X st x1 in S & ||.(x1 - x0).|| < pq holds ||.((H /. x1) - (H /. x0)).|| < r

      proof

        let x0 be Point of X;

        let r be Real;

        assume

         A16: x0 in S & 0 < r;

        then

         A17: f is_continuous_in x0 by A3;

        

         A18: g is_continuous_in x0 by A4, A16;

        

         A20: (f . x0) in ( rng f) & (g . x0) in ( rng g) by A2, A16, FUNCT_1: 3;

         [(f . x0), (g . x0)] is set by TARSKI: 1;

        then

        reconsider z0 = [(f . x0), (g . x0)] as Point of [:E, F:] by A20, PRVECT_3: 18;

        consider s be Real such that

         A21: 0 < s & for z1 be Point of [:E, F:] st z1 in the carrier of [:E, F:] & ||.(z1 - z0).|| < s holds ||.((BL /. z1) - (BL /. z0)).|| < r by A1, A16, NFCONT_1: 19;

        set s1 = (s / 2);

        consider p be Real such that

         A23: 0 < p & for x1 be Point of X st x1 in ( dom f) & ||.(x1 - x0).|| < p holds ||.((f /. x1) - (f /. x0)).|| < s1 by A17, A21, NFCONT_1: 7, XREAL_1: 215;

        consider q be Real such that

         A24: 0 < q & for x1 be Point of X st x1 in ( dom g) & ||.(x1 - x0).|| < q holds ||.((g /. x1) - (g /. x0)).|| < s1 by A18, A21, NFCONT_1: 7, XREAL_1: 215;

        set pq = ( min (p,q));

        

         A25: 0 < pq & pq <= p & pq <= q by A23, A24, XXREAL_0: 15, XXREAL_0: 17;

        take pq;

        thus 0 < pq by A23, A24, XXREAL_0: 15;

        thus for x1 be Point of X st x1 in S & ||.(x1 - x0).|| < pq holds ||.((H /. x1) - (H /. x0)).|| < r

        proof

          let x1 be Point of X;

          assume

           A26: x1 in S & ||.(x1 - x0).|| < pq;

          then

           A27: ||.(x1 - x0).|| < p & ||.(x1 - x0).|| < q by A25, XXREAL_0: 2;

          then

           A29: ||.((f /. x1) - (f /. x0)).|| < s1 by A2, A23, A26;

          

           A30: ||.((g /. x1) - (g /. x0)).|| < s1 by A2, A24, A26, A27;

          

           A32: (f . x1) in ( rng f) & (g . x1) in ( rng g) by A2, A26, FUNCT_1: 3;

           [(f . x1), (g . x1)] is set by TARSKI: 1;

          then

          reconsider z1 = [(f . x1), (g . x1)] as Point of [:E, F:] by A32, PRVECT_3: 18;

          

           A33: z1 = [(f /. x1), (g . x1)] by A2, A26, PARTFUN1:def 6

          .= [(f /. x1), (g /. x1)] by A2, A26, PARTFUN1:def 6;

          z0 = [(f /. x0), (g . x0)] by A2, A16, PARTFUN1:def 6

          .= [(f /. x0), (g /. x0)] by A2, A16, PARTFUN1:def 6;

          then ( - z0) = [( - (f /. x0)), ( - (g /. x0))] by PRVECT_3: 18;

          then (z1 - z0) = [((f /. x1) - (f /. x0)), ((g /. x1) - (g /. x0))] by A33, PRVECT_3: 18;

          then

           A35: ||.(z1 - z0).|| = ( sqrt (( ||.((f /. x1) - (f /. x0)).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 ))) by NDIFF_8: 1;

          

           A36: ( ||.((f /. x1) - (f /. x0)).|| ^2 ) <= (s1 ^2 ) by A29, SQUARE_1: 15;

          ( ||.((g /. x1) - (g /. x0)).|| ^2 ) <= (s1 ^2 ) by A30, SQUARE_1: 15;

          then

           A38: (( ||.((f /. x1) - (f /. x0)).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 )) <= (((s ^2 ) / 4) + ((s ^2 ) / 4)) by A36, XREAL_1: 7;

          ((s ^2 ) / 2) < (s ^2 ) by A21, XREAL_1: 129, XREAL_1: 216;

          then (( ||.((f /. x1) - (f /. x0)).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 )) < (s ^2 ) by A38, XXREAL_0: 2;

          then ( sqrt (( ||.((f /. x1) - (f /. x0)).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 ))) < ( sqrt (s ^2 )) by SQUARE_1: 27;

          then

           A40: ||.(z1 - z0).|| < s by A21, A35, SQUARE_1: 22;

          

           A41: (H /. x1) = (H . x1) by A12, A26, PARTFUN1:def 6

          .= (BL . ((f . x1),(g . x1))) by A13, A26

          .= (BL /. z1);

          (H /. x0) = (H . x0) by A12, A16, PARTFUN1:def 6

          .= (BL . ((f . x0),(g . x0))) by A13, A16

          .= (BL /. z0);

          hence ||.((H /. x1) - (H /. x0)).|| < r by A21, A40, A41;

        end;

      end;

      hence H is_continuous_on S by A12, NFCONT_1: 19;

    end;

    theorem :: NDIFF_9:4

    

     LmTh471: for E,F be RealNormSpace, g be PartFunc of E, F, A be Subset of E st g is_continuous_on A & ( dom g) = A holds ex xg be PartFunc of E, [:E, F:] st ( dom xg) = A & (for x be Point of E st x in A holds (xg . x) = [x, (g . x)]) & xg is_continuous_on A

    proof

      let E,F be RealNormSpace, g be PartFunc of E, F, S be Subset of E;

      assume that

       A1: g is_continuous_on S and

       A2: ( dom g) = S;

      defpred P1[ object, object] means ex t be Point of E st t = $1 & $2 = [t, (g . t)];

      

       A3: for x be object st x in S holds ex y be object st y in the carrier of [:E, F:] & P1[x, y]

      proof

        let x be object;

        assume

         A4: x in S;

        then

        reconsider t = x as Point of E;

        take y = [t, (g . t)];

        (g . t) in ( rng g) by A2, A4, FUNCT_1: 3;

        then

        reconsider q = (g . t) as Point of F;

         [t, q] is set by TARSKI: 1;

        then [t, q] is Point of [:E, F:] by PRVECT_3: 18;

        hence y in the carrier of [:E, F:] & P1[x, y];

      end;

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

       A6: for z be object st z in S holds P1[z, (H . z)] from FUNCT_2:sch 1( A3);

      

       A7: ( dom H) = S by FUNCT_2:def 1;

      ( rng H) c= the carrier of [:E, F:];

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

      then

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

      take H;

      thus ( dom H) = S by FUNCT_2:def 1;

      thus

       A11: for s be Point of E st s in S holds (H . s) = [s, (g . s)]

      proof

        let s be Point of E;

        assume s in S;

        then ex t be Point of E st t = s & (H . s) = [t, (g . t)] by A6;

        hence thesis;

      end;

      for x0 be Point of E holds for r be Real st x0 in S & 0 < r holds ex pq be Real st 0 < pq & for x1 be Point of E st x1 in S & ||.(x1 - x0).|| < pq holds ||.((H /. x1) - (H /. x0)).|| < r

      proof

        let x0 be Point of E;

        let r be Real;

        assume

         A12: x0 in S & 0 < r;

        then

         A14: (g . x0) in ( rng g) by A2, FUNCT_1: 3;

         [x0, (g . x0)] is set by TARSKI: 1;

        then

        reconsider z0 = [x0, (g . x0)] as Point of [:E, F:] by A14, PRVECT_3: 18;

        

         A15: 0 < (r / 2) & (r / 2) < r by A12, XREAL_1: 215, XREAL_1: 216;

        consider q be Real such that

         A16: 0 < q & for x1 be Point of E st x1 in S & ||.(x1 - x0).|| < q holds ||.((g /. x1) - (g /. x0)).|| < (r / 2) by A1, A12, NFCONT_1: 19, XREAL_1: 215;

        set pq = ( min (q,(r / 2)));

        

         A17: 0 < pq & pq <= q & pq <= (r / 2) by A15, A16, XXREAL_0: 15, XXREAL_0: 17;

        take pq;

        thus 0 < pq by A15, A16, XXREAL_0: 15;

        thus for x1 be Point of E st x1 in S & ||.(x1 - x0).|| < pq holds ||.((H /. x1) - (H /. x0)).|| < r

        proof

          let x1 be Point of E;

          assume

           A18: x1 in S & ||.(x1 - x0).|| < pq;

          then ||.(x1 - x0).|| < q by A17, XXREAL_0: 2;

          then

           A21: ||.((g /. x1) - (g /. x0)).|| < (r / 2) by A16, A18;

          

           A23: (g . x1) in ( rng g) by A2, A18, FUNCT_1: 3;

           [x1, (g . x1)] is set by TARSKI: 1;

          then

          reconsider z1 = [x1, (g . x1)] as Point of [:E, F:] by A23, PRVECT_3: 18;

          

           A24: z1 = [x1, (g /. x1)] by A2, A18, PARTFUN1:def 6;

          z0 = [x0, (g /. x0)] by A2, A12, PARTFUN1:def 6;

          then ( - z0) = [( - x0), ( - (g /. x0))] by PRVECT_3: 18;

          then (z1 - z0) = [(x1 - x0), ((g /. x1) - (g /. x0))] by A24, PRVECT_3: 18;

          then

           A26: ||.(z1 - z0).|| = ( sqrt (( ||.(x1 - x0).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 ))) by NDIFF_8: 1;

           ||.(x1 - x0).|| < (r / 2) by A17, A18, XXREAL_0: 2;

          then

           A27: ( ||.(x1 - x0).|| ^2 ) < ((r / 2) ^2 ) by SQUARE_1: 16;

          ( ||.((g /. x1) - (g /. x0)).|| ^2 ) <= ((r / 2) ^2 ) by A21, SQUARE_1: 15;

          then

           A29: (( ||.(x1 - x0).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 )) <= (((r ^2 ) / 4) + ((r ^2 ) / 4)) by A27, XREAL_1: 7;

          ((r ^2 ) / 2) < (r ^2 ) by A12, XREAL_1: 129, XREAL_1: 216;

          then (( ||.(x1 - x0).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 )) < (r ^2 ) by A29, XXREAL_0: 2;

          then

           A31: ( sqrt (( ||.(x1 - x0).|| ^2 ) + ( ||.((g /. x1) - (g /. x0)).|| ^2 ))) < ( sqrt (r ^2 )) by SQUARE_1: 27;

          

           A32: (H /. x1) = (H . x1) by A7, A18, PARTFUN1:def 6

          .= z1 by A11, A18;

          (H /. x0) = (H . x0) by A7, A12, PARTFUN1:def 6

          .= z0 by A11, A12;

          hence ||.((H /. x1) - (H /. x0)).|| < r by A12, A26, A31, A32, SQUARE_1: 22;

        end;

      end;

      hence H is_continuous_on S by A7, NFCONT_1: 19;

    end;

    theorem :: NDIFF_9:5

    

     NFCONT112: for S,T,V be RealNormSpace holds for x0 be Point of V holds for f1 be PartFunc of the carrier of V, the carrier of S holds for f2 be PartFunc of the carrier of S, the carrier of T st x0 in ( dom (f2 * f1)) & f1 is_continuous_in x0 & f2 is_continuous_in (f1 /. x0) holds (f2 * f1) is_continuous_in x0

    proof

      let S,T,V be RealNormSpace;

      let x0 be Point of V;

      let f1 be PartFunc of the carrier of V, the carrier of S;

      let f2 be PartFunc of the carrier of S, the carrier of T;

      assume

       A1: x0 in ( dom (f2 * f1));

      assume that

       A2: f1 is_continuous_in x0 and

       A3: f2 is_continuous_in (f1 /. x0);

      thus x0 in ( dom (f2 * f1)) by A1;

      let s1 be sequence of V;

      assume that

       A4: ( rng s1) c= ( dom (f2 * f1)) and

       A5: s1 is convergent & ( lim s1) = x0;

      

       A6: ( dom (f2 * f1)) c= ( dom f1) by RELAT_1: 25;

      

       B6: ( rng (f1 /* s1)) c= ( dom f2)

      proof

        let x be object;

        assume x in ( rng (f1 /* s1));

        then

        consider n be Element of NAT such that

         A7: x = ((f1 /* s1) . n) by FUNCT_2: 113;

        (s1 . n) in ( rng s1) by VALUED_0: 28;

        then (f1 . (s1 . n)) in ( dom f2) by A4, FUNCT_1: 11;

        hence x in ( dom f2) by A4, A6, A7, FUNCT_2: 108, XBOOLE_1: 1;

      end;

       A9:

      now

        let n be Element of NAT ;

        (s1 . n) in ( rng s1) by VALUED_0: 28;

        then

         A10: (s1 . n) in ( dom f1) by A4, FUNCT_1: 11;

        

        thus (((f2 * f1) /* s1) . n) = ((f2 * f1) . (s1 . n)) by A4, FUNCT_2: 108

        .= (f2 . (f1 . (s1 . n))) by A10, FUNCT_1: 13

        .= (f2 . ((f1 /* s1) . n)) by A4, A6, FUNCT_2: 108, XBOOLE_1: 1

        .= ((f2 /* (f1 /* s1)) . n) by B6, FUNCT_2: 108;

      end;

      then

       A10: (f2 /* (f1 /* s1)) = ((f2 * f1) /* s1) by FUNCT_2: 63;

      ( rng s1) c= ( dom f1) by A4, A6, XBOOLE_1: 1;

      then

       A11: ((f1 /* s1) is convergent & (f1 /. x0) = ( lim (f1 /* s1))) by A2, A5, NFCONT_1:def 5;

      ((f2 * f1) /. x0) = (f2 /. (f1 /. x0)) by A1, PARTFUN2: 3

      .= ( lim (f2 /* (f1 /* s1))) by A3, B6, A11, NFCONT_1:def 5

      .= ( lim ((f2 * f1) /* s1)) by A9, FUNCT_2: 63;

      hence (((f2 * f1) /* s1) is convergent & ((f2 * f1) /. x0) = ( lim ((f2 * f1) /* s1))) by A3, B6, A10, A11, NFCONT_1:def 5;

    end;

    theorem :: NDIFF_9:6

    

     LM0: for E,F be RealNormSpace, z be Point of [:E, F:], x be Point of E, y be Point of F st z = [x, y] holds ||.z.|| <= ( ||.x.|| + ||.y.||)

    proof

      let E,F be RealNormSpace, z be Point of [:E, F:], x be Point of E, y be Point of F;

      assume z = [x, y];

      then

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

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

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

      hence thesis by A2, SQUARE_1: 22;

    end;

    theorem :: NDIFF_9:7

    

     Th0: for E,F,G be RealNormSpace, L be LinearOperator of [:E, F:], G holds ex L1 be LinearOperator of E, G, L2 be LinearOperator of F, G st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y]))

    proof

      let E,F,G be RealNormSpace, L be LinearOperator of [:E, F:], G;

      deffunc FH1( Point of E) = (L /. [$1, ( 0. F)]);

      consider L1 be Function of the carrier of E, the carrier of G such that

       A1: for x be Point of E holds (L1 . x) = FH1(x) from FUNCT_2:sch 4;

      

       A4: for s,t be Element of E holds (L1 . (s + t)) = ((L1 . s) + (L1 . t))

      proof

        let s,t be Element of E;

         [s, ( 0. F)] is set & [t, ( 0. F)] is set by TARSKI: 1;

        then

        reconsider z = [s, ( 0. F)], w = [t, ( 0. F)] as Point of [:E, F:] by PRVECT_3: 18;

        (z + w) = [(s + t), (( 0. F) + ( 0. F))] by PRVECT_3: 18

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

        

        hence (L1 . (s + t)) = (L /. (z + w)) by A1

        .= ((L /. z) + (L /. w)) by VECTSP_1:def 20

        .= ((L1 . s) + (L /. [t, ( 0. F)])) by A1

        .= ((L1 . s) + (L1 . t)) by A1;

      end;

      for s be Element of E holds for r be Real holds (L1 . (r * s)) = (r * (L1 . s))

      proof

        let s be Element of E, r be Real;

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

        then

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

        (r * z) = [(r * s), (r * ( 0. F))] by PRVECT_3: 18

        .= [(r * s), ( 0. F)] by RLVECT_1: 10;

        

        hence (L1 . (r * s)) = (L /. (r * z)) by A1

        .= (r * (L /. z)) by LOPBAN_1:def 5

        .= (r * (L1 . s)) by A1;

      end;

      then

      reconsider L1 as LinearOperator of E, G by A4, LOPBAN_1:def 5, VECTSP_1:def 20;

      deffunc FH2( Point of F) = (L /. [( 0. E), $1]);

      consider L2 be Function of the carrier of F, the carrier of G such that

       A7: for x be Point of F holds (L2 . x) = FH2(x) from FUNCT_2:sch 4;

      

       A10: for s,t be Element of F holds (L2 . (s + t)) = ((L2 . s) + (L2 . t))

      proof

        let s,t be Element of F;

         [( 0. E), s] is set & [( 0. E), t] is set by TARSKI: 1;

        then

        reconsider z = [( 0. E), s], w = [( 0. E), t] as Point of [:E, F:] by PRVECT_3: 18;

        (z + w) = [(( 0. E) + ( 0. E)), (s + t)] by PRVECT_3: 18

        .= [( 0. E), (s + t)] by RLVECT_1: 4;

        

        hence (L2 . (s + t)) = (L /. (z + w)) by A7

        .= ((L /. z) + (L /. w)) by VECTSP_1:def 20

        .= ((L2 . s) + (L /. [( 0. E), t])) by A7

        .= ((L2 . s) + (L2 . t)) by A7;

      end;

      for s be Element of F holds for r be Real holds (L2 . (r * s)) = (r * (L2 . s))

      proof

        let s be Element of F, r be Real;

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

        then

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

        (r * z) = [(r * ( 0. E)), (r * s)] by PRVECT_3: 18

        .= [( 0. E), (r * s)] by RLVECT_1: 10;

        

        hence (L2 . (r * s)) = (L /. (r * z)) by A7

        .= (r * (L /. z)) by LOPBAN_1:def 5

        .= (r * (L2 . s)) by A7;

      end;

      then

      reconsider L2 as LinearOperator of F, G by A10, LOPBAN_1:def 5, VECTSP_1:def 20;

      for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))

      proof

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

         [x, y] is set & [x, ( 0. F)] is set & [( 0. E), y] is set by TARSKI: 1;

        then

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

        (z1 + z2) = [(x + ( 0. E)), (( 0. F) + y)] by PRVECT_3: 18

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

        .= z by RLVECT_1: 4;

        

        hence (L . [x, y]) = ((L /. z1) + (L /. z2)) by VECTSP_1:def 20

        .= ((L1 . x) + (L /. z2)) by A1

        .= ((L1 . x) + (L2 . y)) by A7;

      end;

      hence ex L1 be LinearOperator of E, G, L2 be LinearOperator of F, G st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y])) by A1, A7;

    end;

    theorem :: NDIFF_9:8

    

     Th0X: for E,F,G be RealNormSpace, L be LinearOperator of [:E, F:], G, L11 be LinearOperator of E, G, L12 be LinearOperator of F, G, L21 be LinearOperator of E, G, L22 be LinearOperator of F, G st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L11 . x) + (L12 . y))) & (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L21 . x) + (L22 . y))) holds L11 = L21 & L12 = L22

    proof

      let E,F,G be RealNormSpace, L be LinearOperator of [:E, F:], G;

      let L11 be LinearOperator of E, G, L12 be LinearOperator of F, G, L21 be LinearOperator of E, G, L22 be LinearOperator of F, G;

      assume that

       A1: (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L11 . x) + (L12 . y))) and

       A2: (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L21 . x) + (L22 . y)));

      now

        let x be Point of E;

        

         A4: (L22 . ( 0. F)) = ( 0. G) by LOPBAN_7: 3;

        (L12 . ( 0. F)) = ( 0. G) by LOPBAN_7: 3;

        

        hence (L11 . x) = ((L11 . x) + (L12 . ( 0. F))) by RLVECT_1: 4

        .= (L . [x, ( 0. F)]) by A1

        .= ((L21 . x) + (L22 . ( 0. F))) by A2

        .= (L21 . x) by A4, RLVECT_1: 4;

      end;

      hence L11 = L21 by FUNCT_2:def 8;

      now

        let y be Point of F;

        

         A6: (L21 . ( 0. E)) = ( 0. G) by LOPBAN_7: 3;

        (L11 . ( 0. E)) = ( 0. G) by LOPBAN_7: 3;

        

        hence (L12 . y) = ((L11 . ( 0. E)) + (L12 . y)) by RLVECT_1: 4

        .= (L . [( 0. E), y]) by A1

        .= ((L21 . ( 0. E)) + (L22 . y)) by A2

        .= (L22 . y) by A6, RLVECT_1: 4;

      end;

      hence L12 = L22 by FUNCT_2:def 8;

    end;

    theorem :: NDIFF_9:9

    

     Th1: for E,F,G be RealNormSpace, L1 be LinearOperator of E, G, L2 be LinearOperator of F, G holds ex L be LinearOperator of [:E, F:], G st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y]))

    proof

      let E,F,G be RealNormSpace, L1 be LinearOperator of E, G, L2 be LinearOperator of F, G;

      defpred P1[ object, object] means ex x be Point of E, y be Point of F st $1 = [x, y] & $2 = ((L1 . x) + (L2 . y));

      

       A1: for z be Element of [:E, F:] holds ex y be Element of G st P1[z, y]

      proof

        let z be Element of [:E, F:];

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

         A2: z = [x, y] by PRVECT_3: 18;

        take w = ((L1 . x) + (L2 . y));

        thus P1[z, w] by A2;

      end;

      consider L be Function of [:E, F:], G such that

       A3: for z be Element of [:E, F:] holds P1[z, (L . z)] from FUNCT_2:sch 3( A1);

      

       A4: for z,w be Point of [:E, F:] holds (L . (z + w)) = ((L . z) + (L . w))

      proof

        let z,w be Point of [:E, F:];

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

         A5: z = [x1, y1] & (L . z) = ((L1 . x1) + (L2 . y1)) by A3;

        consider x2 be Point of E, y2 be Point of F such that

         A6: w = [x2, y2] & (L . w) = ((L1 . x2) + (L2 . y2)) by A3;

        

         A7: (z + w) = [(x1 + x2), (y1 + y2)] by A5, A6, PRVECT_3: 18;

        consider x3 be Point of E, y3 be Point of F such that

         A8: (z + w) = [x3, y3] & (L . (z + w)) = ((L1 . x3) + (L2 . y3)) by A3;

        

         A9: x3 = (x1 + x2) & y3 = (y1 + y2) by A7, A8, XTUPLE_0: 1;

        ((L . z) + (L . w)) = ((((L1 . x1) + (L2 . y1)) + (L1 . x2)) + (L2 . y2)) by A5, A6, RLVECT_1:def 3

        .= ((((L1 . x1) + (L1 . x2)) + (L2 . y1)) + (L2 . y2)) by RLVECT_1:def 3

        .= (((L1 . x1) + (L1 . x2)) + ((L2 . y1) + (L2 . y2))) by RLVECT_1:def 3

        .= ((L1 . (x1 + x2)) + ((L2 . y1) + (L2 . y2))) by VECTSP_1:def 20

        .= (L . (z + w)) by A8, A9, VECTSP_1:def 20;

        hence thesis;

      end;

      for z be Element of [:E, F:] holds for r be Real holds (L . (r * z)) = (r * (L . z))

      proof

        let z be Element of [:E, F:], r be Real;

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

         A10: z = [x1, y1] & (L . z) = ((L1 . x1) + (L2 . y1)) by A3;

        

         A11: (r * z) = [(r * x1), (r * y1)] by A10, PRVECT_3: 18;

        consider x2 be Point of E, y2 be Point of F such that

         A12: (r * z) = [x2, y2] & (L . (r * z)) = ((L1 . x2) + (L2 . y2)) by A3;

        x2 = (r * x1) & y2 = (r * y1) by A11, A12, XTUPLE_0: 1;

        

        hence (L . (r * z)) = ((r * (L1 . x1)) + (L2 . (r * y1))) by A12, LOPBAN_1:def 5

        .= ((r * (L1 . x1)) + (r * (L2 . y1))) by LOPBAN_1:def 5

        .= (r * (L . z)) by A10, RLVECT_1:def 5;

      end;

      then

      reconsider L as LinearOperator of [:E, F:], G by A4, LOPBAN_1:def 5, VECTSP_1:def 20;

      take L;

      thus

       A14: for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))

      proof

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

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

        then

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

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

         A15: z = [x1, y1] & (L . z) = ((L1 . x1) + (L2 . y1)) by A3;

        x = x1 & y1 = y by A15, XTUPLE_0: 1;

        hence (L . [x, y]) = ((L1 . x) + (L2 . y)) by A15;

      end;

      thus for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])

      proof

        let x be Point of E;

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

        then [x, ( 0. F)] is Point of [:E, F:] by PRVECT_3: 18;

        then [x, ( 0. F)] in the carrier of [:E, F:];

        then

         A16: [x, ( 0. F)] in ( dom L) by FUNCT_2:def 1;

        

        thus (L1 . x) = ((L1 . x) + ( 0. G)) by RLVECT_1: 4

        .= ((L1 . x) + (L2 . ( 0. F))) by LOPBAN_7: 3

        .= (L . [x, ( 0. F)]) by A14

        .= (L /. [x, ( 0. F)]) by A16, PARTFUN1:def 6;

      end;

      thus for y be Point of F holds (L2 . y) = (L /. [( 0. E), y])

      proof

        let y be Point of F;

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

        then [( 0. E), y] is Point of [:E, F:] by PRVECT_3: 18;

        then [( 0. E), y] in the carrier of [:E, F:];

        then

         A17: [( 0. E), y] in ( dom L) by FUNCT_2:def 1;

        

        thus (L2 . y) = (( 0. G) + (L2 . y)) by RLVECT_1: 4

        .= ((L1 . ( 0. E)) + (L2 . y)) by LOPBAN_7: 3

        .= (L . [( 0. E), y]) by A14

        .= (L /. [( 0. E), y]) by A17, PARTFUN1:def 6;

      end;

    end;

    theorem :: NDIFF_9:10

    

     Th2: for E,F,G be RealNormSpace, L be Lipschitzian LinearOperator of [:E, F:], G holds ex L1 be Lipschitzian LinearOperator of E, G, L2 be Lipschitzian LinearOperator of F, G st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y]))

    proof

      let E,F,G be RealNormSpace, L be Lipschitzian LinearOperator of [:E, F:], G;

      consider L1 be LinearOperator of E, G, L2 be LinearOperator of F, G such that

       A1: (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y])) by Th0;

      consider K be Real such that

       A2: 0 <= K & for z be VECTOR of [:E, F:] holds ||.(L . z).|| <= (K * ||.z.||) by LOPBAN_1:def 8;

      now

        let x be Point of E;

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

        then

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

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

        then

         A3: z in ( dom L) by FUNCT_2:def 1;

        

         A4: (L1 . x) = (L /. [x, ( 0. F)]) by A1

        .= (L . z) by A3, PARTFUN1:def 6;

         ||.z.|| = ||.x.|| by NDIFF_8: 2;

        hence ||.(L1 . x).|| <= (K * ||.x.||) by A2, A4;

      end;

      then

       A5: L1 is Lipschitzian by A2, LOPBAN_1:def 8;

      now

        let y be Point of F;

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

        then

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

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

        then

         A6: z in ( dom L) by FUNCT_2:def 1;

        

         A7: (L2 . y) = (L /. [( 0. E), y]) by A1

        .= (L . z) by A6, PARTFUN1:def 6;

         ||.z.|| = ||.y.|| by NDIFF_8: 3;

        hence ||.(L2 . y).|| <= (K * ||.y.||) by A2, A7;

      end;

      then L2 is Lipschitzian by A2, LOPBAN_1:def 8;

      hence thesis by A1, A5;

    end;

    theorem :: NDIFF_9:11

    for E,F,G be RealNormSpace, L1 be Lipschitzian LinearOperator of E, G, L2 be Lipschitzian LinearOperator of F, G holds ex L be Lipschitzian LinearOperator of [:E, F:], G st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y]))

    proof

      let E,F,G be RealNormSpace, L1 be Lipschitzian LinearOperator of E, G, L2 be Lipschitzian LinearOperator of F, G;

      consider L be LinearOperator of [:E, F:], G such that

       A1: (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y])) by Th1;

      consider K1 be Real such that

       A2: 0 <= K1 & for x be VECTOR of E holds ||.(L1 . x).|| <= (K1 * ||.x.||) by LOPBAN_1:def 8;

      consider K2 be Real such that

       A3: 0 <= K2 & for y be VECTOR of F holds ||.(L2 . y).|| <= (K2 * ||.y.||) by LOPBAN_1:def 8;

      now

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

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

         A5: z = [x, y] by PRVECT_3: 18;

        (L . z) = ((L1 . x) + (L2 . y)) by A1, A5;

        then

         A7: ||.(L . z).|| <= ( ||.(L1 . x).|| + ||.(L2 . y).||) by NORMSP_1:def 1;

        

         A8: ||.(L1 . x).|| <= (K1 * ||.x.||) & ||.(L2 . y).|| <= (K2 * ||.y.||) by A2, A3;

        

         A9: (K1 * ||.x.||) <= (K1 * ||.z.||) by A2, A5, NDIFF_8: 21, XREAL_1: 64;

        (K2 * ||.y.||) <= (K2 * ||.z.||) by A3, A5, NDIFF_8: 21, XREAL_1: 64;

        then ||.(L1 . x).|| <= (K1 * ||.z.||) & ||.(L2 . y).|| <= (K2 * ||.z.||) by A8, A9, XXREAL_0: 2;

        then ( ||.(L1 . x).|| + ||.(L2 . y).||) <= ((K1 * ||.z.||) + (K2 * ||.z.||)) by XREAL_1: 7;

        hence ||.(L . z).|| <= ((K1 + K2) * ||.z.||) by A7, XXREAL_0: 2;

      end;

      then L is Lipschitzian by A2, A3, LOPBAN_1:def 8;

      hence thesis by A1;

    end;

    theorem :: NDIFF_9:12

    for E,F,G be RealNormSpace, L be Point of ( R_NormSpace_of_BoundedLinearOperators ( [:E, F:],G)) holds ex L1 be Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)), L2 be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) & (for x be Point of E holds (L1 . x) = (L . [x, ( 0. F)])) & (for y be Point of F holds (L2 . y) = (L . [( 0. E), y])) & ||.L.|| <= ( ||.L1.|| + ||.L2.||) & ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.||

    proof

      let E,F,G be RealNormSpace, LP be Point of ( R_NormSpace_of_BoundedLinearOperators ( [:E, F:],G));

      reconsider L = LP as Lipschitzian LinearOperator of [:E, F:], G by LOPBAN_1:def 9;

      consider L1 be Lipschitzian LinearOperator of E, G, L2 be Lipschitzian LinearOperator of F, G such that

       A1: (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L1 . x) + (L2 . y))) and

       A2: (for x be Point of E holds (L1 . x) = (L /. [x, ( 0. F)])) and

       A3: (for y be Point of F holds (L2 . y) = (L /. [( 0. E), y])) by Th2;

      reconsider LP1 = L1 as Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;

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

      take LP1, LP2;

      thus for x be Point of E, y be Point of F holds (LP . [x, y]) = ((LP1 . x) + (LP2 . y)) by A1;

      thus for x be Point of E holds (LP1 . x) = (LP . [x, ( 0. F)])

      proof

        let x be Point of E;

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

        then [x, ( 0. F)] is Point of [:E, F:] by PRVECT_3: 18;

        then [x, ( 0. F)] in the carrier of [:E, F:];

        then

         A4: [x, ( 0. F)] in ( dom L) by FUNCT_2:def 1;

        

        thus (LP1 . x) = (L /. [x, ( 0. F)]) by A2

        .= (LP . [x, ( 0. F)]) by A4, PARTFUN1:def 6;

      end;

      thus for y be Point of F holds (LP2 . y) = (LP . [( 0. E), y])

      proof

        let y be Point of F;

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

        then [( 0. E), y] is Point of [:E, F:] by PRVECT_3: 18;

        then [( 0. E), y] in the carrier of [:E, F:];

        then

         A5: [( 0. E), y] in ( dom L) by FUNCT_2:def 1;

        

        thus (LP2 . y) = (L /. [( 0. E), y]) by A3

        .= (LP . [( 0. E), y]) by A5, PARTFUN1:def 6;

      end;

      

       A7: ||.LP.|| = ( upper_bound ( PreNorms ( modetrans (LP, [:E, F:],G)))) by LOPBAN_1:def 13

      .= ( upper_bound ( PreNorms L)) by LOPBAN_1: 29;

      for t be Real st t in ( PreNorms L) holds t <= ( ||.LP1.|| + ||.LP2.||)

      proof

        let t be Real;

        assume t in ( PreNorms L);

        then

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

         A8: t = ||.(L . w).|| & ||.w.|| <= 1;

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

         A9: w = [x, y] by PRVECT_3: 18;

         ||.x.|| <= ||.w.|| by A9, NDIFF_8: 21;

        then

         A10: ||.x.|| <= 1 by A8, XXREAL_0: 2;

         ||.y.|| <= ||.w.|| by A9, NDIFF_8: 21;

        then

         A11: ||.y.|| <= 1 by A8, XXREAL_0: 2;

        (L . w) = ((L1 . x) + (L2 . y)) by A1, A9;

        then

         A12: ||.(L . w).|| <= ( ||.(L1 . x).|| + ||.(L2 . y).||) by NORMSP_1:def 1;

        

         A13: ||.(L1 . x).|| <= ( ||.LP1.|| * ||.x.||) by LOPBAN_1: 32;

        ( ||.LP1.|| * ||.x.||) <= ( ||.LP1.|| * 1) by A10, XREAL_1: 64;

        then

         A14: ||.(L1 . x).|| <= ||.LP1.|| by A13, XXREAL_0: 2;

        

         A15: ||.(L2 . y).|| <= ( ||.LP2.|| * ||.y.||) by LOPBAN_1: 32;

        ( ||.LP2.|| * ||.y.||) <= ( ||.LP2.|| * 1) by A11, XREAL_1: 64;

        then ||.(L2 . y).|| <= ||.LP2.|| by A15, XXREAL_0: 2;

        then ( ||.(L1 . x).|| + ||.(L2 . y).||) <= ( ||.LP1.|| + ||.LP2.||) by A14, XREAL_1: 7;

        hence thesis by A8, A12, XXREAL_0: 2;

      end;

      hence ||.LP.|| <= ( ||.LP1.|| + ||.LP2.||) by A7, SEQ_4: 45;

      

       A17: ||.LP1.|| = ( upper_bound ( PreNorms ( modetrans (LP1,E,G)))) by LOPBAN_1:def 13

      .= ( upper_bound ( PreNorms L1)) by LOPBAN_1: 29;

      for t be Real st t in ( PreNorms L1) holds t <= ||.LP.||

      proof

        let t be Real;

        assume t in ( PreNorms L1);

        then

        consider x be Point of E such that

         A18: t = ||.(L1 . x).|| & ||.x.|| <= 1;

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

        then

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

        

         A19: ||.w.|| <= 1 by A18, NDIFF_8: 2;

        

         A20: (L . w) = ((L1 . x) + (L2 . ( 0. F))) by A1

        .= ((L1 . x) + ( 0. G)) by LOPBAN_7: 3

        .= (L1 . x) by RLVECT_1:def 4;

        

         A21: ||.(L . w).|| <= ( ||.LP.|| * ||.w.||) by LOPBAN_1: 32;

        ( ||.LP.|| * ||.w.||) <= ( ||.LP.|| * 1) by A19, XREAL_1: 64;

        hence t <= ||.LP.|| by A18, A20, A21, XXREAL_0: 2;

      end;

      hence ||.LP1.|| <= ||.LP.|| by A17, SEQ_4: 45;

      

       A23: ||.LP2.|| = ( upper_bound ( PreNorms ( modetrans (LP2,F,G)))) by LOPBAN_1:def 13

      .= ( upper_bound ( PreNorms L2)) by LOPBAN_1: 29;

      for t be Real st t in ( PreNorms L2) holds t <= ||.LP.||

      proof

        let t be Real;

        assume t in ( PreNorms L2);

        then

        consider x be Point of F such that

         A24: t = ||.(L2 . x).|| & ||.x.|| <= 1;

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

        then

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

        

         A25: ||.x.|| = ||.w.|| by NDIFF_8: 3;

        

         A26: (L . w) = ((L1 . ( 0. E)) + (L2 . x)) by A1

        .= (( 0. G) + (L2 . x)) by LOPBAN_7: 3

        .= (L2 . x) by RLVECT_1:def 4;

        

         A27: ||.(L . w).|| <= ( ||.LP.|| * ||.w.||) by LOPBAN_1: 32;

        ( ||.LP.|| * ||.w.||) <= ( ||.LP.|| * 1) by A24, A25, XREAL_1: 64;

        hence t <= ||.LP.|| by A24, A26, A27, XXREAL_0: 2;

      end;

      hence ||.LP2.|| <= ||.LP.|| by A23, SEQ_4: 45;

    end;

    theorem :: NDIFF_9:13

    for E,F,G be RealNormSpace, L be Point of ( R_NormSpace_of_BoundedLinearOperators ( [:E, F:],G)), L11,L12 be Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)), L21,L22 be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) st (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L11 . x) + (L21 . y))) & (for x be Point of E, y be Point of F holds (L . [x, y]) = ((L12 . x) + (L22 . y))) holds L11 = L12 & L21 = L22

    proof

      let E,F,G be RealNormSpace, L be Point of ( R_NormSpace_of_BoundedLinearOperators ( [:E, F:],G)), L11,L12 be Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)), L21,L22 be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G));

      assume

       A1: for x be Point of E, y be Point of F holds (L . [x, y]) = ((L11 . x) + (L21 . y));

      assume

       A2: for x be Point of E, y be Point of F holds (L . [x, y]) = ((L12 . x) + (L22 . y));

      reconsider LP = L as Lipschitzian LinearOperator of [:E, F:], G by LOPBAN_1:def 9;

      reconsider LP11 = L11, LP12 = L12 as Lipschitzian LinearOperator of E, G by LOPBAN_1:def 9;

      reconsider LP21 = L21, LP22 = L22 as Lipschitzian LinearOperator of F, G by LOPBAN_1:def 9;

      

       A3: for x be Point of E, y be Point of F holds (LP . [x, y]) = ((LP11 . x) + (LP21 . y)) by A1;

      for x be Point of E, y be Point of F holds (LP . [x, y]) = ((LP12 . x) + (LP22 . y)) by A2;

      hence L11 = L12 & L21 = L22 by A3, Th0X;

    end;

    begin

    theorem :: NDIFF_9:14

    

     Th4: for E,G,F be RealNormSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, z be Point of [:E, F:] st f is_differentiable_in z holds f is_partial_differentiable_in`1 z & f is_partial_differentiable_in`2 z & for dx be Point of E, dy be Point of F holds (( diff (f,z)) . [dx, dy]) = ((( partdiff`1 (f,z)) . dx) + (( partdiff`2 (f,z)) . dy))

    proof

      let E,G,F be RealNormSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, z be Point of [:E, F:];

      assume

       A1: f is_differentiable_in z;

      reconsider y = (( IsoCPNrSP (E,F)) . z) as Point of ( product <*E, F*>);

      ((( IsoCPNrSP (E,F)) " ) . (( IsoCPNrSP (E,F)) . z)) = z by FUNCT_2: 26;

      then

       A3: (f * (( IsoCPNrSP (E,F)) " )) is_differentiable_in y by A1, NDIFF_7: 28;

      then

       A4: f is_partial_differentiable_in`1 z & f is_partial_differentiable_in`2 z by NDIFF_5: 41, NDIFF_7: 34;

      consider N be Neighbourhood of z such that

       A5: N c= ( dom f) & ex R be RestFunc of [:E, F:], G st for w be Point of [:E, F:] st w in N holds ((f /. w) - (f /. z)) = ((( diff (f,z)) . (w - z)) + (R /. (w - z))) by A1, NDIFF_1:def 7;

      consider R be RestFunc of [:E, F:], G such that

       A6: for w be Point of [:E, F:] st w in N holds ((f /. w) - (f /. z)) = ((( diff (f,z)) . (w - z)) + (R /. (w - z))) by A5;

      reconsider L = ( diff (f,z)) as Lipschitzian LinearOperator of [:E, F:], G by LOPBAN_1:def 9;

      consider L1 be Lipschitzian LinearOperator of E, G, L2 be Lipschitzian LinearOperator of F, G such that

       A7: (for dx be Point of E, dy be Point of F holds (L . [dx, dy]) = ((L1 . dx) + (L2 . dy))) and (for dx be Point of E holds (L1 . dx) = (L /. [dx, ( 0. F)])) and (for dy be Point of F holds (L2 . dy) = (L /. [( 0. E), dy])) by Th2;

      reconsider LL1 = L1 as Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;

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

      set g1 = (f * ( reproj1 z));

      set g2 = (f * ( reproj2 z));

      reconsider x = (z `1 ) as Point of E;

      reconsider y = (z `2 ) as Point of F;

      

       A9: ex x1 be Point of E, x2 be Point of F st z = [x1, x2] by PRVECT_3: 18;

      then

       A10: z = [x, y];

      consider r0 be Real such that

       A14: 0 < r0 & { y where y be Point of [:E, F:] : ||.(y - z).|| < r0 } c= N by NFCONT_1:def 1;

      

       A15: { y where y be Point of [:E, F:] : ||.(y - z).|| < r0 } = ( Ball (z,r0)) by NDIFF_8: 17;

      consider r be Real such that

       A16: 0 < r & r < r0 & [:( Ball (x,r)), ( Ball (y,r)):] c= ( Ball (z,r0)) by A9, A14, NDIFF_8: 22;

      

       A17: [:( Ball (x,r)), ( Ball (y,r)):] c= N by A14, A15, A16, XBOOLE_1: 1;

      deffunc FP1( Point of E) = (R /. [$1, ( 0. F)]);

      consider R1 be Function of the carrier of E, the carrier of G such that

       A18: for p be Point of E holds (R1 . p) = FP1(p) from FUNCT_2:sch 4;

      

       A20: for dx be Point of E holds (R1 /. dx) = (R /. [dx, ( 0. F)]) by A18;

      deffunc FP2( Point of F) = (R /. [( 0. E), $1]);

      consider R2 be Function of the carrier of F, the carrier of G such that

       A21: for p be Point of F holds (R2 . p) = FP2(p) from FUNCT_2:sch 4;

      

       A23: for dy be Point of F holds (R2 /. dy) = (R /. [( 0. E), dy]) by A21;

      for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Point of E st z <> ( 0. E) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R1 /. z).||) < r

      proof

        let r be Real;

        assume

         A25: r > 0 ;

        R is total by NDIFF_1:def 5;

        then

        consider d be Real such that

         A26: d > 0 & for z be Point of [:E, F:] st z <> ( 0. [:E, F:]) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r by A25, NDIFF_1: 23;

        take d;

        thus d > 0 by A26;

        let x1 be Point of E;

        assume

         A27: x1 <> ( 0. E) & ||.x1.|| < d;

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

        then

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

        

         A28: z <> ( 0. [:E, F:]) by A27, XTUPLE_0: 1;

        

         A29: (R /. z) = (R1 /. x1) by A18;

         ||.z.|| = ||.x1.|| by NDIFF_8: 2;

        hence (( ||.x1.|| " ) * ||.(R1 /. x1).||) < r by A26, A27, A28, A29;

      end;

      then

      reconsider R1 as RestFunc of E, G by NDIFF_1: 23;

      for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Point of F st z <> ( 0. F) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R2 /. z).||) < r

      proof

        let r be Real;

        assume

         A32: r > 0 ;

        R is total by NDIFF_1:def 5;

        then

        consider d be Real such that

         A33: d > 0 & for z be Point of [:E, F:] st z <> ( 0. [:E, F:]) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r by A32, NDIFF_1: 23;

        take d;

        thus d > 0 by A33;

        let y1 be Point of F;

        assume

         A34: y1 <> ( 0. F) & ||.y1.|| < d;

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

        then

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

        

         A35: z <> ( 0. [:E, F:]) by A34, XTUPLE_0: 1;

        

         A36: (R /. z) = (R2 /. y1) by A21;

         ||.z.|| = ||.y1.|| by NDIFF_8: 3;

        hence (( ||.y1.|| " ) * ||.(R2 /. y1).||) < r by A33, A34, A35, A36;

      end;

      then

      reconsider R2 as RestFunc of F, G by NDIFF_1: 23;

      reconsider N1 = ( Ball (x,r)) as Neighbourhood of x by A16, NDIFF_8: 19;

      reconsider N2 = ( Ball (y,r)) as Neighbourhood of y by A16, NDIFF_8: 19;

      

       A37: N1 c= ( dom g1)

      proof

        let s be object;

        assume

         A39: s in N1;

        then

        reconsider t = s as Point of E;

        

         A40: ( dom ( reproj1 z)) = the carrier of E by FUNCT_2:def 1;

        

         A41: (( reproj1 z) . t) = [t, y] by NDIFF_7:def 1;

        t in ( Ball (x,r)) & y in ( Ball (y,r)) by A16, A39, NDIFF_8: 13;

        then [t, y] in [:( Ball (x,r)), ( Ball (y,r)):] by ZFMISC_1: 87;

        then (( reproj1 z) . t) in N by A17, A41;

        hence s in ( dom g1) by A5, A40, FUNCT_1: 11;

      end;

      

       B42: N2 c= ( dom g2)

      proof

        let s be object;

        assume

         A43: s in N2;

        then

        reconsider t = s as Point of F;

        

         A44: ( dom ( reproj2 z)) = the carrier of F by FUNCT_2:def 1;

        

         A45: (( reproj2 z) . t) = [x, t] by NDIFF_7:def 2;

        t in ( Ball (y,r)) & x in ( Ball (x,r)) by A16, A43, NDIFF_8: 13;

        then [x, t] in [:( Ball (x,r)), ( Ball (y,r)):] by ZFMISC_1: 87;

        then (( reproj2 z) . t) in N by A17, A45;

        hence s in ( dom g2) by A5, A44, FUNCT_1: 11;

      end;

      for x1 be Point of E st x1 in N1 holds ((g1 /. x1) - (g1 /. x)) = ((LL1 . (x1 - x)) + (R1 /. (x1 - x)))

      proof

        let x1 be Point of E;

        assume

         A48: x1 in N1;

        then

         A50: (( reproj1 z) . x1) in ( dom f) by A37, FUNCT_1: 11;

        

         A51: (( reproj1 z) . x1) = [x1, y] by NDIFF_7:def 1;

        x1 in ( Ball (x,r)) & y in ( Ball (y,r)) by A16, A48, NDIFF_8: 13;

        then

         A52: [x1, y] in [:( Ball (x,r)), ( Ball (y,r)):] by ZFMISC_1: 87;

        

         A53: x in N1 by A16, NDIFF_8: 13;

        then

         A54: (( reproj1 z) . x) in ( dom f) by A37, FUNCT_1: 11;

        ( - z) = [( - x), ( - y)] by A9, PRVECT_3: 18;

        

        then

         A56: ((( reproj1 z) . x1) - z) = [(x1 - x), (y - y)] by A51, PRVECT_3: 18

        .= [(x1 - x), ( 0. F)] by RLVECT_1: 15;

        

         A57: (g1 /. x1) = (g1 . x1) by A37, A48, PARTFUN1:def 6

        .= (f . (( reproj1 z) . x1)) by A37, A48, FUNCT_1: 12

        .= (f /. (( reproj1 z) . x1)) by A50, PARTFUN1:def 6;

        (g1 /. x) = (g1 . x) by A37, A53, PARTFUN1:def 6

        .= (f . (( reproj1 z) . x)) by A37, A53, FUNCT_1: 12

        .= (f /. (( reproj1 z) . x)) by A54, PARTFUN1:def 6

        .= (f /. z) by A10, NDIFF_7:def 1;

        

        hence ((g1 /. x1) - (g1 /. x)) = ((( diff (f,z)) . ((( reproj1 z) . x1) - z)) + (R /. ((( reproj1 z) . x1) - z))) by A6, A17, A51, A52, A57

        .= (((L1 . (x1 - x)) + (L2 . ( 0. F))) + (R /. [(x1 - x), ( 0. F)])) by A7, A56

        .= (((L1 . (x1 - x)) + ( 0. G)) + (R /. [(x1 - x), ( 0. F)])) by LOPBAN_7: 3

        .= ((L1 . (x1 - x)) + (R /. [(x1 - x), ( 0. F)])) by RLVECT_1: 4

        .= ((LL1 . (x1 - x)) + (R1 /. (x1 - x))) by A20;

      end;

      then

       A59: LL1 = ( partdiff`1 (f,z)) by A4, A37, NDIFF_1:def 7;

      for y1 be Point of F st y1 in N2 holds ((g2 /. y1) - (g2 /. y)) = ((LL2 . (y1 - y)) + (R2 /. (y1 - y)))

      proof

        let y1 be Point of F;

        assume

         A61: y1 in N2;

        then

         A63: (( reproj2 z) . y1) in ( dom f) by B42, FUNCT_1: 11;

        

         A64: (( reproj2 z) . y1) = [x, y1] by NDIFF_7:def 2;

        x in ( Ball (x,r)) & y1 in ( Ball (y,r)) by A16, A61, NDIFF_8: 13;

        then

         A65: [x, y1] in [:( Ball (x,r)), ( Ball (y,r)):] by ZFMISC_1: 87;

        

         A66: y in N2 by A16, NDIFF_8: 13;

        then

         A67: (( reproj2 z) . y) in ( dom f) by B42, FUNCT_1: 11;

        ( - z) = [( - x), ( - y)] by A9, PRVECT_3: 18;

        

        then

         A69: ((( reproj2 z) . y1) - z) = [(x - x), (y1 - y)] by A64, PRVECT_3: 18

        .= [( 0. E), (y1 - y)] by RLVECT_1: 15;

        

         A70: (g2 /. y1) = (g2 . y1) by B42, A61, PARTFUN1:def 6

        .= (f . (( reproj2 z) . y1)) by B42, A61, FUNCT_1: 12

        .= (f /. (( reproj2 z) . y1)) by A63, PARTFUN1:def 6;

        (g2 /. y) = (g2 . y) by B42, A66, PARTFUN1:def 6

        .= (f . (( reproj2 z) . y)) by B42, A66, FUNCT_1: 12

        .= (f /. (( reproj2 z) . y)) by A67, PARTFUN1:def 6

        .= (f /. z) by A10, NDIFF_7:def 2;

        

        hence ((g2 /. y1) - (g2 /. y)) = ((( diff (f,z)) . ((( reproj2 z) . y1) - z)) + (R /. ((( reproj2 z) . y1) - z))) by A6, A17, A64, A65, A70

        .= (((L1 . ( 0. E)) + (L2 . (y1 - y))) + (R /. [( 0. E), (y1 - y)])) by A7, A69

        .= ((( 0. G) + (L2 . (y1 - y))) + (R /. [( 0. E), (y1 - y)])) by LOPBAN_7: 3

        .= ((L2 . (y1 - y)) + (R /. [( 0. E), (y1 - y)])) by RLVECT_1: 4

        .= ((LL2 . (y1 - y)) + (R2 /. (y1 - y))) by A23;

      end;

      then LL2 = ( partdiff`2 (f,z)) by A4, B42, NDIFF_1:def 7;

      hence thesis by A3, A7, A59, NDIFF_5: 41, NDIFF_7: 34;

    end;

    theorem :: NDIFF_9:15

    

     Th5: for E,G,F be RealNormSpace, 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:], r1,r2 be Real, g be PartFunc of E, F, P be Lipschitzian LinearOperator of E, G, Q be Lipschitzian LinearOperator of G, F st Z is open & ( dom f) = Z & z = [a, b] & z in Z & (f . (a,b)) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & ( dom g) = ( Ball (a,r1)) & ( rng g) c= ( Ball (b,r2)) & (g . a) = b & g is_continuous_in a & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g . x))) = c) & ( partdiff`2 (f,z)) is one-to-one & Q = (( partdiff`2 (f,z)) " ) & P = ( partdiff`1 (f,z)) holds g is_differentiable_in a & ( diff (g,a)) = ( - (Q * P))

    proof

      let E,G,F be RealNormSpace, 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:], r1,r2 be Real, g be PartFunc of E, F, P be Lipschitzian LinearOperator of E, G, Q be Lipschitzian LinearOperator of G, F;

      assume

       A1: Z is open & ( dom f) = Z & z = [a, b] & z in Z & (f . (a,b)) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & ( dom g) = ( Ball (a,r1)) & ( rng g) c= ( Ball (b,r2)) & (g . a) = b & g is_continuous_in a & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g . x))) = c) & ( partdiff`2 (f,z)) is one-to-one & Q = (( partdiff`2 (f,z)) " ) & P = ( partdiff`1 (f,z));

      then

       A5: (g /. a) = b by NDIFF_8: 13, PARTFUN1:def 6;

      reconsider S = ( partdiff`2 (f,z)) as Lipschitzian LinearOperator of F, G by LOPBAN_1:def 9;

      

       A8: (Q * P) is Lipschitzian LinearOperator of E, F by LOPBAN_2: 2;

      then

      reconsider L = (Q * P) as Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)) by LOPBAN_1:def 9;

      

       A9: (( - 1) * L) is Lipschitzian LinearOperator of E, F by LOPBAN_1:def 9;

      reconsider NL = (( - 1) * L) as PartFunc of E, F by LOPBAN_1:def 9;

      

       A10: ( dom NL) = the carrier of E by A9, FUNCT_2:def 1

      .= ( dom (Q * P)) by FUNCT_2:def 1;

       A11:

      now

        let x be VECTOR of E;

        assume x in ( dom NL);

        

        hence (NL /. x) = ((( - 1) * L) . x) by PARTFUN1:def 6

        .= (( - 1) * ((Q * P) /. x)) by LOPBAN_1: 36;

      end;

      

       A15: ( - L) = (( - 1) * L) by RLVECT_1: 16

      .= (( - 1) (#) (Q * P)) by A10, A11, VFUNCT_1:def 4

      .= ( - (Q * P)) by VFUNCT_1: 23;

      consider N0 be Neighbourhood of z such that

       A16: N0 c= ( dom f) & ex R be RestFunc of [:E, F:], G st for w be Point of [:E, F:] st w in N0 holds ((f /. w) - (f /. z)) = ((( diff (f,z)) . (w - z)) + (R /. (w - z))) by A1, NDIFF_1:def 7;

      consider R be RestFunc of [:E, F:], G such that

       A17: for w be Point of [:E, F:] st w in N0 holds ((f /. w) - (f /. z)) = ((( diff (f,z)) . (w - z)) + (R /. (w - z))) by A16;

      consider r0 be Real such that

       A20: 0 < r0 & { y where y be Point of [:E, F:] : ||.(y - z).|| < r0 } c= N0 by NFCONT_1:def 1;

      

       A21: { y where y be Point of [:E, F:] : ||.(y - z).|| < r0 } = ( Ball (z,r0)) by NDIFF_8: 17;

      consider r3 be Real such that

       A22: 0 < r3 & r3 < r0 & [:( Ball (a,r3)), ( Ball (b,r3)):] c= ( Ball (z,r0)) by A1, A20, NDIFF_8: 22;

      

       A23: [:( Ball (a,r3)), ( Ball (b,r3)):] c= N0 by A20, A21, A22, XBOOLE_1: 1;

      reconsider r4 = ( min (r1,r3)) as Real;

      

       A24: 0 < r4 by A1, A22, XXREAL_0: 15;

      r4 <= r1 & r4 <= r3 by XXREAL_0: 17;

      then

       A26: ( Ball (a,r4)) c= ( Ball (a,r1)) & ( Ball (a,r4)) c= ( Ball (a,r3)) by NDIFF_8: 15;

      consider r5 be Real such that

       A27: 0 < r5 & for x1 be Point of E st x1 in ( dom g) & ||.(x1 - a).|| < r5 holds ||.((g /. x1) - (g /. a)).|| < r3 by A1, A22, NFCONT_1: 7;

      reconsider r6 = ( min (r4,r5)) as Real;

      

       A28: 0 < r6 by A24, A27, XXREAL_0: 15;

      r6 <= r4 & r6 <= r5 by XXREAL_0: 17;

      then

       A30: ( Ball (a,r6)) c= ( Ball (a,r4)) & ( Ball (a,r6)) c= ( Ball (a,r5)) by NDIFF_8: 15;

      reconsider N = ( Ball (a,r6)) as Neighbourhood of a by A28, NDIFF_8: 19;

      deffunc FR1( Point of E) = ( - (Q . (R /. [$1, ((g /. (a + $1)) - (g /. a))])));

      consider R1 be Function of the carrier of E, the carrier of F such that

       A31: for p be Point of E holds (R1 . p) = FR1(p) from FUNCT_2:sch 4;

      

       A33: N c= ( dom g) by A1, A26, A30, XBOOLE_1: 1;

      

       A34: for x be Point of E st x in N holds ((g /. x) - (g /. a)) = ((( - L) . (x - a)) + (R1 /. (x - a)))

      proof

        let x be Point of E;

        assume x in N;

        then

         A36: x in ( Ball (a,r4)) & x in ( Ball (a,r5)) by A30;

        then x in { y where y be Point of E : ||.(y - a).|| < r5 } by NDIFF_8: 17;

        then ex q be Element of E st x = q & ||.(q - a).|| < r5;

        then ||.((g /. x) - (g /. a)).|| < r3 by A1, A26, A27, A36;

        then (g /. x) in { y where y be Point of F : ||.(y - b).|| < r3 } by A5;

        then

         A39: (g /. x) in ( Ball (b,r3)) by NDIFF_8: 17;

        

         A41: (f . (x,(g . x))) = c by A1, A26, A36;

        

         A42: [x, (g /. x)] in [:( Ball (a,r3)), ( Ball (b,r3)):] by A26, A36, A39, ZFMISC_1: 87;

        then

         A45: [x, (g /. x)] in N0 by A23;

        then

        reconsider w = [x, (g /. x)] as Point of [:E, F:];

        

         A47: ((f /. w) - (f /. z)) = ((( diff (f,z)) . (w - z)) + (R /. (w - z))) by A17, A23, A42;

        

         A48: (f /. z) = c by A1, PARTFUN1:def 6;

        

         A50: (f /. w) = (f . [x, (g /. x)]) by A16, A45, PARTFUN1:def 6

        .= c by A1, A26, A36, A41, PARTFUN1:def 6;

        ( - z) = [( - a), ( - b)] by A1, PRVECT_3: 18;

        

        then

         A52: (w - z) = [(x - a), ((g /. x) - b)] by PRVECT_3: 18

        .= [(x - a), ((g /. x) - (g /. a))] by A1, NDIFF_8: 13, PARTFUN1:def 6;

        then (( diff (f,z)) . (w - z)) = ((( partdiff`1 (f,z)) . (x - a)) + (( partdiff`2 (f,z)) . ((g /. x) - (g /. a)))) by A1, Th4;

        then ( 0. G) = (((P . (x - a)) + (S . ((g /. x) - (g /. a)))) + (R /. (w - z))) by A1, A47, A48, A50, RLVECT_1: 15;

        then ( 0. F) = (Q . (((P . (x - a)) + (S . ((g /. x) - (g /. a)))) + (R /. (w - z)))) by LOPBAN_7: 3;

        

        then ( 0. F) = ((Q . ((P . (x - a)) + (S . ((g /. x) - (g /. a))))) + (Q . (R /. (w - z)))) by VECTSP_1:def 20

        .= (((Q . (P . (x - a))) + (Q . (S . ((g /. x) - (g /. a))))) + (Q . (R /. (w - z)))) by VECTSP_1:def 20

        .= ((((Q * P) . (x - a)) + (Q . (S . ((g /. x) - (g /. a))))) + (Q . (R /. (w - z)))) by FUNCT_2: 15

        .= ((((Q * P) . (x - a)) + ((g /. x) - (g /. a))) + (Q . (R /. (w - z)))) by A1, FUNCT_2: 26;

        then (( 0. F) - (Q . (R /. (w - z)))) = (((Q * P) . (x - a)) + ((g /. x) - (g /. a))) by RLVECT_4: 1;

        

        then

         A53: (( - (Q . (R /. (w - z)))) - ((Q * P) . (x - a))) = ((((g /. x) - (g /. a)) + ((Q * P) . (x - a))) - ((Q * P) . (x - a))) by RLVECT_1: 14

        .= ((g /. x) - (g /. a)) by RLVECT_4: 1;

        

         A54: ( dom ( - (Q * P))) = ( dom (Q * P)) by VFUNCT_1:def 5

        .= the carrier of E by FUNCT_2:def 1;

        

         A55: ( - ((Q * P) . (x - a))) = ( - ((Q * P) /. (x - a)))

        .= (( - (Q * P)) /. (x - a)) by A54, VFUNCT_1:def 5

        .= (( - L) . (x - a)) by A15, A54, PARTFUN1:def 6;

        (R1 /. (x - a)) = ( - (Q . (R /. [(x - a), ((g /. ((x - a) + a)) - (g /. a))]))) by A31

        .= ( - (Q . (R /. (w - z)))) by A52, RLVECT_4: 1;

        hence ((g /. x) - (g /. a)) = ((( - L) . (x - a)) + (R1 /. (x - a))) by A53, A55;

      end;

      defpred FP[ Point of E, object] means $2 = [$1, ((g /. (a + $1)) - (g /. a))];

      

       A59: for dx be Element of the carrier of E holds ex dy be Element of the carrier of [:E, F:] st FP[dx, dy]

      proof

        let x be Element of the carrier of E;

         [x, ((g /. (a + x)) - (g /. a))] is set by TARSKI: 1;

        then

        reconsider y = [x, ((g /. (a + x)) - (g /. a))] as Point of [:E, F:] by PRVECT_3: 18;

        take y;

        thus y = [x, ((g /. (a + x)) - (g /. a))];

      end;

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

       A60: for dx be Element of the carrier of E holds FP[dx, (V . dx)] from FUNCT_2:sch 3( A59);

      

       A62: R is total by NDIFF_1:def 5;

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

      set BLQ = ||.Q1.||;

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

      then

      consider dr be Real such that

       A65: dr > 0 & for dz be Point of [:E, F:] st dz <> ( 0. [:E, F:]) & ||.dz.|| < dr holds (( ||.dz.|| " ) * ||.(R /. dz).||) < (1 / (2 * (BLQ + 1))) by A62, NDIFF_1: 23;

      consider dr1 be Real such that

       A66: 0 < dr1 & dr1 < dr & [:( Ball (a,dr1)), ( Ball ((g /. a),dr1)):] c= ( Ball (z,dr)) by A1, A5, A65, NDIFF_8: 22;

      consider dr2 be Real such that

       A67: 0 < dr2 & for x1 be Point of E st x1 in ( dom g) & ||.(x1 - a).|| < dr2 holds ||.((g /. x1) - (g /. a)).|| < dr1 by A1, A66, NFCONT_1: 7;

      reconsider dr3 = ( min (dr1,dr2)) as Real;

      

       A69: dr3 <= dr1 & dr3 <= dr2 by XXREAL_0: 17;

      reconsider dr4 = ( min (dr3,r1)) as Real;

       0 < dr3 by A66, A67, XXREAL_0: 15;

      then

       A71: 0 < dr4 by A1, XXREAL_0: 15;

      

       A72: dr4 <= dr3 & dr4 <= r1 by XXREAL_0: 17;

      

       A74: for dx be Point of E st dx <> ( 0. E) & ||.dx.|| < dr4 holds ||.(R /. (V . dx)).|| <= ((1 / (2 * (BLQ + 1))) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||))

      proof

        let dx be Point of E;

        set x1 = (a + dx);

        assume

         A75: dx <> ( 0. E) & ||.dx.|| < dr4;

        then

         A76: ||.(x1 - a).|| < dr4 by RLVECT_4: 1;

        then ||.(x1 - a).|| < dr3 by A72, XXREAL_0: 2;

        then

         A78: ||.(x1 - a).|| < dr1 & ||.(x1 - a).|| < dr2 by A69, XXREAL_0: 2;

        then ||.(a - x1).|| < dr1 by NORMSP_1: 7;

        then

         A79: x1 in ( Ball (a,dr1));

         ||.(a - x1).|| < dr4 by A76, NORMSP_1: 7;

        then ||.(a - x1).|| < r1 & ||.(a - x1).|| < dr3 by A72, XXREAL_0: 2;

        then x1 in ( Ball (a,r1));

        then ||.((g /. x1) - (g /. a)).|| < dr1 by A1, A67, A78;

        then ||.((g /. a) - (g /. x1)).|| < dr1 by NORMSP_1: 7;

        then (g /. x1) in ( Ball ((g /. a),dr1));

        then [x1, (g /. x1)] in [:( Ball (a,dr1)), ( Ball ((g /. a),dr1)):] by A79, ZFMISC_1: 87;

        then [x1, (g /. x1)] in ( Ball (z,dr)) by A66;

        then

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

         A84: w = [x1, (g /. x1)] & ||.(z - w).|| < dr;

        ( - z) = [( - a), ( - (g /. a))] by A1, A5, PRVECT_3: 18;

        then

         A86: (w - z) = [(x1 - a), ((g /. x1) - (g /. a))] by A84, PRVECT_3: 18;

        

         A87: ||.(w - z).|| < dr by A84, NORMSP_1: 7;

        (x1 - a) = dx by RLVECT_4: 1;

        then

         A88: (w - z) <> ( 0. [:E, F:]) by A75, A86, XTUPLE_0: 1;

        then ||.(w - z).|| <> 0 by NORMSP_0:def 5;

        then ((( ||.(w - z).|| " ) * ||.(R /. (w - z)).||) * ||.(w - z).||) < ((1 / (2 * (BLQ + 1))) * ||.(w - z).||) by A65, A87, A88, XREAL_1: 68;

        then (( ||.(w - z).|| " ) * ( ||.(R /. (w - z)).|| * ||.(w - z).||)) < ((1 / (2 * (BLQ + 1))) * ||.(w - z).||);

        then

         A91: ||.(R /. (w - z)).|| < ((1 / (2 * (BLQ + 1))) * ||.(w - z).||) by A88, NORMSP_0:def 5, XCMPLX_1: 203;

        

         A92: (V . dx) = [dx, ((g /. (a + dx)) - (g /. a))] by A60

        .= [(x1 - a), ((g /. x1) - (g /. a))] by RLVECT_4: 1;

        then

         A94: ((1 / (2 * (BLQ + 1))) * ||.(V . dx).||) <= ((1 / (2 * (BLQ + 1))) * ( ||.(x1 - a).|| + ||.((g /. x1) - (g /. a)).||)) by LM0, XREAL_1: 64;

        (g /. x1) = (g /. (a + dx)) & (x1 - a) = dx by RLVECT_4: 1;

        hence ||.(R /. (V . dx)).|| <= ((1 / (2 * (BLQ + 1))) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)) by A86, A91, A92, A94, XXREAL_0: 2;

      end;

      

       A95: for dx be Point of E st dx <> ( 0. E) & ||.dx.|| < dr4 holds ||.(R1 /. dx).|| <= ((1 / 2) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||))

      proof

        let dx be Point of E;

        assume dx <> ( 0. E) & ||.dx.|| < dr4;

        then

         A97: ||.(R /. (V . dx)).|| <= ((1 / (2 * (BLQ + 1))) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)) by A74;

        

         A98: ||.(Q . (R /. (V . dx))).|| <= (BLQ * ||.(R /. (V . dx)).||) by LOPBAN_1: 32;

        

         A99: (BLQ * ||.(R /. (V . dx)).||) <= (BLQ * ((1 / (2 * (BLQ + 1))) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||))) by A97, XREAL_1: 64;

        

         A101: (BLQ * (1 / (2 * (BLQ + 1)))) = ((1 * BLQ) / (2 * (BLQ + 1)))

        .= ((1 / 2) * (BLQ / (BLQ + 1))) by XCMPLX_1: 103;

        (BLQ + 0 ) <= (BLQ + 1) by XREAL_1: 7;

        then (BLQ / (BLQ + 1)) <= 1 by XREAL_1: 183;

        then ((1 / 2) * (BLQ / (BLQ + 1))) <= ((1 / 2) * 1) by XREAL_1: 64;

        then ((BLQ * (1 / (2 * (BLQ + 1)))) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)) <= ((1 / 2) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)) by A101, XREAL_1: 64;

        then (BLQ * ||.(R /. (V . dx)).||) <= ((1 / 2) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)) by A99, XXREAL_0: 2;

        then

         A102: ||.(Q . (R /. (V . dx))).|| <= ((1 / 2) * ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)) by A98, XXREAL_0: 2;

        ( - (Q . (R /. (V . dx)))) = ( - (Q . (R /. [dx, ((g /. (a + dx)) - (g /. a))]))) by A60

        .= (R1 /. dx) by A31;

        hence thesis by A102, NORMSP_1: 2;

      end;

      set LQ = ||.L.||;

      reconsider dr5 = ( min (r6,dr4)) as Real;

      

       A104: 0 < dr5 by A28, A71, XXREAL_0: 15;

      

       A105: dr5 <= r6 & dr5 <= dr4 by XXREAL_0: 17;

      

       A107: for dx be Point of E st dx <> ( 0. E) & ||.dx.|| < dr5 holds ||.((g /. (a + dx)) - (g /. a)).|| <= (((2 * LQ) + 1) * ||.dx.||)

      proof

        let dx be Point of E;

        assume

         A108: dx <> ( 0. E) & ||.dx.|| < dr5;

        then

         A109: ||.dx.|| < dr4 by A105, XXREAL_0: 2;

        

         A111: ||.dx.|| < r6 by A105, A108, XXREAL_0: 2;

        set x1 = (a + dx);

        

         A112: (x1 - a) = dx by RLVECT_4: 1;

        then ||.(a - x1).|| < r6 by A111, NORMSP_1: 7;

        then x1 in N;

        then ((g /. x1) - (g /. a)) = ((( - L) . (x1 - a)) + (R1 /. (x1 - a))) by A34;

        then

         A114: ||.((g /. x1) - (g /. a)).|| <= ( ||.(( - L) . (x1 - a)).|| + ||.(R1 /. (x1 - a)).||) by NORMSP_1:def 1;

        (( - L) . (x1 - a)) = ((( - 1) * L) . (x1 - a)) by RLVECT_1: 16

        .= (( - 1) * ((Q * P) . (x1 - a))) by LOPBAN_1: 36

        .= ( - ((Q * P) . (x1 - a))) by RLVECT_1: 16;

        then ||.(( - L) . (x1 - a)).|| = ||.((Q * P) . (x1 - a)).|| by NORMSP_1: 2;

        then

         A115: ||.(( - L) . (x1 - a)).|| <= (LQ * ||.(x1 - a).||) by A8, LOPBAN_1: 32;

         ||.(R1 /. (x1 - a)).|| <= ((1 / 2) * ( ||.(x1 - a).|| + ||.((g /. x1) - (g /. a)).||)) by A95, A108, A109, A112;

        then ( ||.(( - L) . (x1 - a)).|| + ||.(R1 /. (x1 - a)).||) <= ((LQ * ||.(x1 - a).||) + (((1 / 2) * ||.(x1 - a).||) + ((1 / 2) * ||.((g /. x1) - (g /. a)).||))) by A115, XREAL_1: 7;

        then ||.((g /. x1) - (g /. a)).|| <= (((LQ * ||.(x1 - a).||) + ((1 / 2) * ||.(x1 - a).||)) + ((1 / 2) * ||.((g /. x1) - (g /. a)).||)) by A114, XXREAL_0: 2;

        then ( ||.((g /. x1) - (g /. a)).|| - ((1 / 2) * ||.((g /. x1) - (g /. a)).||)) <= ((((LQ * ||.(x1 - a).||) + ((1 / 2) * ||.(x1 - a).||)) + ((1 / 2) * ||.((g /. x1) - (g /. a)).||)) - ((1 / 2) * ||.((g /. x1) - (g /. a)).||)) by XREAL_1: 9;

        then (2 * ((1 / 2) * ||.((g /. x1) - (g /. a)).||)) <= (2 * ((LQ * ||.(x1 - a).||) + ((1 / 2) * ||.(x1 - a).||))) by XREAL_1: 64;

        hence ||.((g /. (a + dx)) - (g /. a)).|| <= (((2 * LQ) + 1) * ||.dx.||) by A112;

      end;

      for r be Real st r > 0 holds ex d be Real st d > 0 & for dx be Point of E st dx <> ( 0. E) & ||.dx.|| < d holds (( ||.dx.|| " ) * ||.(R1 /. dx).||) < r

      proof

        let r be Real;

        assume

         A117: r > 0 ;

        

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

        then 0 < (r / ((BLQ + 1) * ((2 * LQ) + 2))) by A117, XREAL_1: 139;

        then

        consider d1 be Real such that

         A122: d1 > 0 & for dz be Point of [:E, F:] st dz <> ( 0. [:E, F:]) & ||.dz.|| < d1 holds (( ||.dz.|| " ) * ||.(R /. dz).||) < (r / ((BLQ + 1) * ((2 * LQ) + 2))) by A62, NDIFF_1: 23;

        consider r3 be Real such that

         A123: 0 < r3 & r3 < d1 & [:( Ball (a,r3)), ( Ball (b,r3)):] c= ( Ball (z,d1)) by A1, A122, NDIFF_8: 22;

        reconsider r4 = ( min (r1,r3)) as Real;

        

         A124: 0 < r4 by A1, A123, XXREAL_0: 15;

        

         A125: r4 <= r1 & r4 <= r3 by XXREAL_0: 17;

        consider r5 be Real such that

         A127: 0 < r5 & for x1 be Point of E st x1 in ( dom g) & ||.(x1 - a).|| < r5 holds ||.((g /. x1) - (g /. a)).|| < r3 by A1, A123, NFCONT_1: 7;

        reconsider r6 = ( min (r4,r5)) as Real;

        

         A128: 0 < r6 by A124, A127, XXREAL_0: 15;

        

         A129: r6 <= r4 & r6 <= r5 by XXREAL_0: 17;

        reconsider d = ( min (r6,dr5)) as Real;

        

         A132: d <= r6 & d <= dr5 by XXREAL_0: 17;

        take d;

        thus 0 < d by A104, A128, XXREAL_0: 15;

        let dx be Point of E;

        assume

         A133: dx <> ( 0. E) & ||.dx.|| < d;

        set x1 = (a + dx);

         [dx, ((g /. (a + dx)) - (g /. a))] is set by TARSKI: 1;

        then

        reconsider dz = [dx, ((g /. (a + dx)) - (g /. a))] as Point of [:E, F:] by PRVECT_3: 18;

        

         A134: dz <> ( 0. [:E, F:]) by A133, XTUPLE_0: 1;

        

         A137: ||.dx.|| < dr5 by A132, A133, XXREAL_0: 2;

        

         A138: ||.dx.|| < r6 by A132, A133, XXREAL_0: 2;

        then

         A139: ||.dx.|| < r5 by A129, XXREAL_0: 2;

         ||.dx.|| < r4 by A129, A138, XXREAL_0: 2;

        then

         A140: ||.dx.|| < r1 & ||.dx.|| < r3 by A125, XXREAL_0: 2;

        then ||.(x1 - a).|| < r1 by RLVECT_4: 1;

        then ||.(a - x1).|| < r1 by NORMSP_1: 7;

        then

         A141: x1 in ( dom g) by A1;

         ||.(x1 - a).|| < r5 by A139, RLVECT_4: 1;

        then ||.((g /. x1) - (g /. a)).|| < r3 by A127, A141;

        then ||.((g /. a) - (g /. x1)).|| < r3 by NORMSP_1: 7;

        then

         A142: (g /. x1) in ( Ball (b,r3)) by A5;

         ||.(x1 - a).|| < r3 by A140, RLVECT_4: 1;

        then ||.(a - x1).|| < r3 by NORMSP_1: 7;

        then x1 in ( Ball (a,r3));

        then [x1, (g /. x1)] in [:( Ball (a,r3)), ( Ball (b,r3)):] by A142, ZFMISC_1: 87;

        then [x1, (g /. x1)] in ( Ball (z,d1)) by A123;

        then

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

         A145: w = [x1, (g /. x1)] & ||.(z - w).|| < d1;

        ( - z) = [( - a), ( - (g /. a))] by A1, A5, PRVECT_3: 18;

        

        then (w - z) = [(x1 - a), ((g /. x1) - (g /. a))] by A145, PRVECT_3: 18

        .= dz by RLVECT_4: 1;

        then

         A148: ||.dz.|| < d1 by A145, NORMSP_1: 7;

        (R1 /. dx) = ( - (Q . (R /. [dx, ((g /. (a + dx)) - (g /. a))]))) by A31;

        then ||.(R1 /. dx).|| = ||.(Q . (R /. [dx, ((g /. (a + dx)) - (g /. a))])).|| by NORMSP_1: 2;

        then

         A150: ||.(R1 /. dx).|| <= (BLQ * ||.(R /. [dx, ((g /. (a + dx)) - (g /. a))]).||) by LOPBAN_1: 32;

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

        then (BLQ * ||.(R /. [dx, ((g /. (a + dx)) - (g /. a))]).||) <= ((BLQ + 1) * ||.(R /. [dx, ((g /. (a + dx)) - (g /. a))]).||) by XREAL_1: 64;

        then ||.(R1 /. dx).|| <= ((BLQ + 1) * ||.(R /. [dx, ((g /. (a + dx)) - (g /. a))]).||) by A150, XXREAL_0: 2;

        then (( ||.dx.|| " ) * ||.(R1 /. dx).||) <= (( ||.dx.|| " ) * ((BLQ + 1) * ||.(R /. [dx, ((g /. (a + dx)) - (g /. a))]).||)) by XREAL_1: 64;

        then (( ||.dx.|| " ) * ||.(R1 /. dx).||) <= ((( ||.dx.|| " ) * (BLQ + 1)) * ||.(R /. dz).||);

        then

         A152: (( ||.dx.|| " ) * ||.(R1 /. dx).||) <= ((( ||.dx.|| " ) * (BLQ + 1)) * (( ||.dz.|| " ) * ( ||.(R /. dz).|| * ||.dz.||))) by A134, NORMSP_0:def 5, XCMPLX_1: 203;

        

         A153: ||.dz.|| <= ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) by LM0;

         ||.((g /. (a + dx)) - (g /. a)).|| <= (((2 * LQ) + 1) * ||.dx.||) by A107, A133, A137;

        then ( ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) <= ( ||.dx.|| + (((2 * LQ) + 1) * ||.dx.||)) by XREAL_1: 7;

        then ||.dz.|| <= ( ||.dx.|| + (((2 * LQ) + 1) * ||.dx.||)) by A153, XXREAL_0: 2;

        then (( ||.dx.|| " ) * ||.dz.||) <= (( ||.dx.|| " ) * ( ||.dx.|| + (((2 * LQ) + 1) * ||.dx.||))) by XREAL_1: 64;

        then (( ||.dx.|| " ) * ||.dz.||) <= ((( ||.dx.|| " ) * ( ||.dx.|| * 1)) + (( ||.dx.|| " ) * (((2 * LQ) + 1) * ||.dx.||)));

        then (( ||.dx.|| " ) * ||.dz.||) <= (1 + (( ||.dx.|| " ) * (((2 * LQ) + 1) * ||.dx.||))) by A133, NORMSP_0:def 5, XCMPLX_1: 203;

        then (( ||.dx.|| " ) * ||.dz.||) <= (1 + ((2 * LQ) + 1)) by A133, NORMSP_0:def 5, XCMPLX_1: 203;

        then (((BLQ + 1) * (( ||.dz.|| " ) * ||.(R /. dz).||)) * (( ||.dx.|| " ) * ||.dz.||)) <= (((BLQ + 1) * (( ||.dz.|| " ) * ||.(R /. dz).||)) * ((2 * LQ) + 2)) by XREAL_1: 64;

        then

         A159: (( ||.dx.|| " ) * ||.(R1 /. dx).||) <= (((BLQ + 1) * ((2 * LQ) + 2)) * (( ||.dz.|| " ) * ||.(R /. dz).||)) by A152, XXREAL_0: 2;

        (((BLQ + 1) * ((2 * LQ) + 2)) * (( ||.dz.|| " ) * ||.(R /. dz).||)) < (((BLQ + 1) * ((2 * LQ) + 2)) * (r / ((BLQ + 1) * ((2 * LQ) + 2)))) by A120, A122, A134, A148, XREAL_1: 68;

        then (((BLQ + 1) * ((2 * LQ) + 2)) * (( ||.dz.|| " ) * ||.(R /. dz).||)) < r by A120, XCMPLX_1: 87;

        hence (( ||.dx.|| " ) * ||.(R1 /. dx).||) < r by A159, XXREAL_0: 2;

      end;

      then

       A162: R1 is RestFunc of E, F by NDIFF_1: 23;

      hence g is_differentiable_in a by A1, A26, A30, A34, NDIFF_1:def 6, XBOOLE_1: 1;

      hence ( diff (g,a)) = ( - (Q * P)) by A15, A33, A34, A162, NDIFF_1:def 7;

    end;

    reserve X,Y,Z for non trivial RealBanachSpace;

    theorem :: NDIFF_9:16

    

     LMTh3: for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds ex K,s be Real st 0 <= K & 0 < s & for du be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds (u + du) is invertible & ||.((( Inv (u + du)) - ( Inv u)) - ( - ((( Inv u) * du) * ( Inv u)))).|| <= (K * ( ||.du.|| * ||.du.||))

    proof

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: u is invertible;

      set s1 = (1 / ||.( Inv u).||);

      set AG = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      

       A3: 0 < ||.( Inv u).|| by A1, LOPBAN13: 12;

      set s2 = ((1 / 2) / ||.( Inv u).||);

      

       A5: 0 < s2 by A3, XREAL_1: 139;

      set s12 = ( min (s1,s2));

      

       A7: 0 < s12 & s12 <= s1 & s12 <= s2 by A3, A5, XXREAL_0: 15, XXREAL_0: 17;

      set K = (((2 * ||.( Inv u).||) * ||.( Inv u).||) * ||.( Inv u).||);

      take K, s12;

      thus 0 <= K & 0 < s12 by A3, A5, XXREAL_0: 15;

      let du be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A8: ||.du.|| < s12;

      then

       A9: ||.du.|| < s1 by A7, XXREAL_0: 2;

      hence (u + du) is invertible by A1, LOPBAN13: 13;

      consider w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X), s,I be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)) such that

       A11: w = (( Inv u) * du) & s = w & I = ( id X) & ||.s.|| < 1 & (( - w) GeoSeq ) is norm_summable & (I + s) is invertible & ||.( Inv (I + s)).|| <= (1 / (1 - ||.s.||)) & ( Inv (I + s)) = ( Sum (( - w) GeoSeq )) & ( Inv (u + du)) = (( Inv (I + s)) * ( Inv u)) by A1, A9, LOPBAN13: 13;

      reconsider sA = s as Point of AG;

      

       A13: (I * ( Inv u)) = (( id the carrier of X) * ( modetrans (( Inv u),Y,X))) by A11, LOPBAN_1:def 11

      .= ( modetrans (( Inv u),Y,X)) by FUNCT_2: 17

      .= ( Inv u) by LOPBAN_1:def 11;

      reconsider IIu = (I * ( Inv u)) as Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X));

      set L = ((( Inv u) * du) * ( Inv u));

      

       A14: ((( Inv (u + du)) - ( Inv u)) - ( - ((( Inv u) * du) * ( Inv u)))) = (((( Inv (I + s)) * ( Inv u)) - IIu) + L) by A11, A13, RLVECT_1: 17

      .= (((( Inv (I + s)) - I) * ( Inv u)) + L) by LOPBAN13: 20;

      

       A15: (( Inv (I + s)) * (I + s)) = I by A11, LOPBAN13: 22;

      (( Inv (I + s)) * I) = (( modetrans (( Inv (I + s)),X,X)) * ( id the carrier of X)) by A11, LOPBAN_1:def 11

      .= ( modetrans (( Inv (I + s)),X,X)) by FUNCT_2: 17

      .= ( Inv (I + s)) by LOPBAN_1:def 11;

      

      then

       A17: (( Inv (I + s)) - I) = (( Inv (I + s)) * (I - (I + s))) by A15, LOPBAN13: 19

      .= (( Inv (I + s)) * ( - (( Inv u) * du))) by A11, LOPBAN13: 21;

      

      then

       A19: ((( Inv (I + s)) - I) * ( Inv u)) = (( - (( Inv (I + s)) * (( Inv u) * du))) * ( Inv u)) by LOPBAN13: 26

      .= ( - ((( Inv (I + s)) * (( Inv u) * du)) * ( Inv u))) by LOPBAN13: 26

      .= ( - (( Inv (I + s)) * L)) by LOPBAN13: 10;

      (I * L) = (( id the carrier of X) * ( modetrans (L,Y,X))) by A11, LOPBAN_1:def 11

      .= ( modetrans (L,Y,X)) by FUNCT_2: 17

      .= L by LOPBAN_1:def 11;

      

      then (( - (( Inv (I + s)) * L)) + L) = ((I * L) - (( Inv (I + s)) * L))

      .= ((I - ( Inv (I + s))) * L) by LOPBAN13: 20

      .= (( - (( Inv (I + s)) - I)) * L) by RLVECT_1: 33

      .= ( - ((( Inv (I + s)) * ( - (( Inv u) * du))) * ((( Inv u) * du) * ( Inv u)))) by A17, LOPBAN13: 26;

      

      then ((( Inv (u + du)) - ( Inv u)) - ( - ((( Inv u) * du) * ( Inv u)))) = ( - (( - (( Inv (I + s)) * (( Inv u) * du))) * ((( Inv u) * du) * ( Inv u)))) by A14, A19, LOPBAN13: 26

      .= ( - ( - ((( Inv (I + s)) * (( Inv u) * du)) * ((( Inv u) * du) * ( Inv u))))) by LOPBAN13: 26

      .= ((( Inv (I + s)) * (( Inv u) * du)) * ((( Inv u) * du) * ( Inv u))) by RLVECT_1: 17;

      then

       A22: ||.((( Inv (u + du)) - ( Inv u)) - ( - ((( Inv u) * du) * ( Inv u)))).|| <= ( ||.(( Inv (I + s)) * (( Inv u) * du)).|| * ||.((( Inv u) * du) * ( Inv u)).||) by LOPBAN13: 18;

      

       A23: ||.(( Inv (I + s)) * (( Inv u) * du)).|| <= ( ||.( Inv (I + s)).|| * ||.(( Inv u) * du).||) by LOPBAN13: 18;

      ( ||.( Inv (I + s)).|| * ||.(( Inv u) * du).||) <= ( ||.( Inv (I + s)).|| * ( ||.( Inv u).|| * ||.du.||)) by LOPBAN13: 18, XREAL_1: 64;

      then

       A25: ||.(( Inv (I + s)) * (( Inv u) * du)).|| <= ( ||.( Inv (I + s)).|| * ( ||.( Inv u).|| * ||.du.||)) by A23, XXREAL_0: 2;

      

       A26: ( ||.(( Inv u) * du).|| * ||.( Inv u).||) <= (( ||.( Inv u).|| * ||.du.||) * ||.( Inv u).||) by LOPBAN13: 18, XREAL_1: 64;

       ||.((( Inv u) * du) * ( Inv u)).|| <= ( ||.(( Inv u) * du).|| * ||.( Inv u).||) by LOPBAN13: 18;

      then ||.((( Inv u) * du) * ( Inv u)).|| <= (( ||.( Inv u).|| * ||.du.||) * ||.( Inv u).||) by A26, XXREAL_0: 2;

      then ( ||.(( Inv (I + s)) * (( Inv u) * du)).|| * ||.((( Inv u) * du) * ( Inv u)).||) <= (( ||.( Inv (I + s)).|| * ( ||.( Inv u).|| * ||.du.||)) * (( ||.( Inv u).|| * ||.du.||) * ||.( Inv u).||)) by A25, XREAL_1: 66;

      then

       A28: ||.((( Inv (u + du)) - ( Inv u)) - ( - ((( Inv u) * du) * ( Inv u)))).|| <= (( ||.( Inv (I + s)).|| * ( ||.( Inv u).|| * ||.du.||)) * (( ||.( Inv u).|| * ||.du.||) * ||.( Inv u).||)) by A22, XXREAL_0: 2;

      

       A29: ||.s.|| <= ( ||.( Inv u).|| * ||.du.||) by A11, LOPBAN13: 18;

       ||.du.|| < s2 by A7, A8, XXREAL_0: 2;

      then ( ||.( Inv u).|| * ||.du.||) <= ( ||.( Inv u).|| * ((1 / 2) / ||.( Inv u).||)) by XREAL_1: 64;

      then ( ||.( Inv u).|| * ||.du.||) <= (1 / 2) by A3, XCMPLX_1: 87;

      then ||.s.|| <= (1 / 2) by A29, XXREAL_0: 2;

      then (1 - (1 / 2)) <= (1 - ||.s.||) by XREAL_1: 10;

      then (1 / (1 - ||.s.||)) <= (1 / (1 / 2)) by XREAL_1: 118;

      then ||.( Inv (I + s)).|| <= 2 by A11, XXREAL_0: 2;

      then ( ||.( Inv (I + s)).|| * (( ||.( Inv u).|| * ||.du.||) * (( ||.( Inv u).|| * ||.du.||) * ||.( Inv u).||))) <= (2 * (( ||.( Inv u).|| * ||.du.||) * (( ||.( Inv u).|| * ||.du.||) * ||.( Inv u).||))) by XREAL_1: 64;

      hence ||.((( Inv (u + du)) - ( Inv u)) - ( - ((( Inv u) * du) * ( Inv u)))).|| <= (K * ( ||.du.|| * ||.du.||)) by A28, XXREAL_0: 2;

    end;

    theorem :: NDIFF_9:17

    

     LM80: for I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,X)) st ( dom I) = ( InvertibleOperators (X,Y)) & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u) holds for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds I is_differentiable_in u & for du be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (( diff (I,u)) . du) = ( - ((( Inv u) * du) * ( Inv u)))

    proof

      let I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,X));

      assume

       A1: ( dom I) = ( InvertibleOperators (X,Y)) & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u);

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

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

      set N = ( InvertibleOperators (X,Y));

      set P = ( InvertibleOperators (Y,X));

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A2: u in N;

      deffunc FL( Point of S) = ( - ((( Inv u) * $1) * ( Inv u)));

      consider L be Function of the carrier of S, the carrier of W such that

       A3: for x be Point of S holds (L . x) = FL(x) from FUNCT_2:sch 4;

      

       A6: for s,t be Element of S holds (L . (s + t)) = ((L . s) + (L . t))

      proof

        let s,t be Element of S;

        

        thus (L . (s + t)) = ( - ((( Inv u) * (s + t)) * ( Inv u))) by A3

        .= ( - (((( Inv u) * s) + (( Inv u) * t)) * ( Inv u))) by LOPBAN13: 19

        .= ( - (((( Inv u) * s) * ( Inv u)) + ((( Inv u) * t) * ( Inv u)))) by LOPBAN13: 20

        .= (( - ((( Inv u) * s) * ( Inv u))) - ((( Inv u) * t) * ( Inv u))) by RLVECT_1: 31

        .= ((L . s) + ( - ((( Inv u) * t) * ( Inv u)))) by A3

        .= ((L . s) + (L . t)) by A3;

      end;

      for s be Element of S holds for r be Real holds (L . (r * s)) = (r * (L . s))

      proof

        let s be Element of S, r be Real;

        

        thus (L . (r * s)) = ( - ((( Inv u) * (r * s)) * ( Inv u))) by A3

        .= ( - (((r * ( Inv u)) * s) * ( Inv u))) by LOPBAN13: 28

        .= ( - ((r * (( Inv u) * s)) * ( Inv u))) by LOPBAN13: 28

        .= ( - (r * ((( Inv u) * s) * ( Inv u)))) by LOPBAN13: 28

        .= (r * ( - ((( Inv u) * s) * ( Inv u)))) by RLVECT_1: 25

        .= (r * (L . s)) by A3;

      end;

      then

      reconsider L as LinearOperator of S, W by A6, LOPBAN_1:def 5, VECTSP_1:def 20;

      now

        let x be VECTOR of S;

        (L . x) = ( - ((( Inv u) * x) * ( Inv u))) by A3;

        then

         A8: ||.(L . x).|| = ||.((( Inv u) * x) * ( Inv u)).|| by NORMSP_1: 2;

        

         A9: ||.((( Inv u) * x) * ( Inv u)).|| <= ( ||.(( Inv u) * x).|| * ||.( Inv u).||) by LOPBAN13: 18;

        ( ||.(( Inv u) * x).|| * ||.( Inv u).||) <= (( ||.( Inv u).|| * ||.x.||) * ||.( Inv u).||) by LOPBAN13: 18, XREAL_1: 64;

        hence ||.(L . x).|| <= (( ||.( Inv u).|| * ||.( Inv u).||) * ||.x.||) by A8, A9, XXREAL_0: 2;

      end;

      then

      reconsider L as Lipschitzian LinearOperator of S, W by LOPBAN_1:def 8;

      deffunc FR( Point of S) = ((( Inv (u + $1)) - ( Inv u)) - (L . $1));

      consider R be Function of the carrier of S, the carrier of W such that

       A11: for x be Point of S holds (R . x) = FR(x) from FUNCT_2:sch 4;

      

       A12: ( dom R) = the carrier of S by FUNCT_2:def 1;

      

       A13: for x be Point of S holds (R . x) = ((( Inv (u + x)) - ( Inv u)) - ( - ((( Inv u) * x) * ( Inv u))))

      proof

        let x be Point of S;

        

        thus (R . x) = ((( Inv (u + x)) - ( Inv u)) - (L . x)) by A11

        .= ((( Inv (u + x)) - ( Inv u)) - ( - ((( Inv u) * x) * ( Inv u)))) by A3;

      end;

      reconsider L0 = L as Point of ( R_NormSpace_of_BoundedLinearOperators (S,W)) by LOPBAN_1:def 9;

      for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Point of S st z <> ( 0. S) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r

      proof

        let r0 be Real;

        assume

         A15: r0 > 0 ;

        set r = (r0 / 2);

        

         A16: 0 < r & r < r0 by A15, XREAL_1: 215, XREAL_1: 216;

        ex v be Point of S st u = v & v is invertible by A2;

        then

        consider K,s be Real such that

         A17: 0 <= K & 0 < s & for du be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds (u + du) is invertible & ||.((( Inv (u + du)) - ( Inv u)) - ( - ((( Inv u) * du) * ( Inv u)))).|| <= (K * ( ||.du.|| * ||.du.||)) by LMTh3;

        set s1 = (r / (K + 1));

        

         A18: (K + 0 ) < (K + 1) by XREAL_1: 8;

        

         A20: 0 < s1 by A16, A17, XREAL_1: 139;

        set s2 = ( min (s1,1));

        

         A21: 0 < s2 & s2 <= s1 & s2 <= 1 by A20, XXREAL_0: 15, XXREAL_0: 17;

        set d = ( min (s,s2));

        

         A22: 0 < d & d <= s & d <= s2 by A17, A21, XXREAL_0: 15, XXREAL_0: 17;

        then

         A23: d <= s & d <= s1 & d <= 1 by A21, XXREAL_0: 2;

        take d;

        thus d > 0 by A17, A21, XXREAL_0: 15;

        let z be Point of S;

        assume

         A24: z <> ( 0. S) & ||.z.|| < d;

        then

         A25: ||.z.|| < s by A22, XXREAL_0: 2;

         ||.(R /. z).|| = ||.((( Inv (u + z)) - ( Inv u)) - ( - ((( Inv u) * z) * ( Inv u)))).|| by A13;

        then ||.(R /. z).|| <= (K * ( ||.z.|| * ||.z.||)) by A17, A25;

        then ( ||.(R /. z).|| / ||.z.||) <= (((K * ||.z.||) * ||.z.||) / ||.z.||) by XREAL_1: 72;

        then

         A27: ( ||.(R /. z).|| / ||.z.||) <= (K * ||.z.||) by A24, NORMSP_0:def 5, XCMPLX_1: 89;

         ||.z.|| <= s1 by A23, A24, XXREAL_0: 2;

        then

         A28: (K * ||.z.||) <= (K * (r / (K + 1))) by A17, XREAL_1: 64;

        (K / (K + 1)) <= 1 by A17, A18, XREAL_1: 183;

        then (r * (K / (K + 1))) <= (1 * r) by A15, XREAL_1: 64;

        then (K * ||.z.||) <= r by A28, XXREAL_0: 2;

        then ( ||.(R /. z).|| / ||.z.||) <= r by A27, XXREAL_0: 2;

        hence (( ||.z.|| " ) * ||.(R /. z).||) < r0 by A16, XXREAL_0: 2;

      end;

      then

      reconsider R0 = R as RestFunc of S, W by NDIFF_1: 23;

      ex g be Real st 0 < g & { y where y be Point of S : ||.(y - u).|| < g } c= N by A2, NDIFF_1: 3;

      then

       A29: N is Neighbourhood of u by NFCONT_1:def 1;

      

       A30: for v be Point of S st v in N holds ((I /. v) - (I /. u)) = ((L0 . (v - u)) + (R0 /. (v - u)))

      proof

        let v be Point of S;

        assume

         A31: v in N;

        

        then

         A32: (I /. v) = (I . v) by A1, PARTFUN1:def 6

        .= ( Inv v) by A1, A31;

        (I /. u) = (I . u) by A1, A2, PARTFUN1:def 6

        .= ( Inv u) by A1, A2;

        

        hence ((I /. v) - (I /. u)) = (( Inv (u + (v - u))) - ( Inv u)) by A32, RLVECT_4: 1

        .= ((L0 . (v - u)) + ((( Inv (u + (v - u))) - ( Inv u)) - (L . (v - u)))) by RLVECT_4: 1

        .= ((L0 . (v - u)) + ((( Inv (u + (v - u))) - ( Inv u)) - ( - ((( Inv u) * (v - u)) * ( Inv u))))) by A3

        .= ((L0 . (v - u)) + (R . (v - u))) by A13

        .= ((L0 . (v - u)) + (R0 /. (v - u))) by A12, PARTFUN1:def 6;

      end;

      hence

       A34: I is_differentiable_in u by A1, A29, NDIFF_1:def 6;

      let du be Point of S;

      

      thus (( diff (I,u)) . du) = (L0 . du) by A1, A29, A30, A34, NDIFF_1:def 7

      .= ( - ((( Inv u) * du) * ( Inv u))) by A3;

    end;

    theorem :: NDIFF_9:18

    ex I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,X)) st ( dom I) = ( InvertibleOperators (X,Y)) & ( rng I) = ( InvertibleOperators (Y,X)) & I is one-to-one & I is_differentiable_on ( InvertibleOperators (X,Y)) & (ex J be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (Y,X)), ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st J = (I " ) & J is one-to-one & ( dom J) = ( InvertibleOperators (Y,X)) & ( rng J) = ( InvertibleOperators (X,Y)) & J is_differentiable_on ( InvertibleOperators (Y,X))) & (for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u)) & for u,du be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (( diff (I,u)) . du) = ( - ((( Inv u) * du) * ( Inv u)))

    proof

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

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

      consider I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,X)) such that

       A1: ( dom I) = ( InvertibleOperators (X,Y)) & ( rng I) = ( InvertibleOperators (Y,X)) & I is one-to-one & I is_continuous_on ( InvertibleOperators (X,Y)) & (ex J be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (Y,X)), ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st J = (I " ) & J is one-to-one & ( dom J) = ( InvertibleOperators (Y,X)) & ( rng J) = ( InvertibleOperators (X,Y)) & J is_continuous_on ( InvertibleOperators (Y,X))) & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u) by LOPBAN13: 25;

      consider J be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (Y,X)), ( R_NormSpace_of_BoundedLinearOperators (X,Y)) such that

       A2: J = (I " ) & J is one-to-one & ( dom J) = ( InvertibleOperators (Y,X)) & ( rng J) = ( InvertibleOperators (X,Y)) & J is_continuous_on ( InvertibleOperators (Y,X)) by A1;

      take I;

      

       A4: for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds I is_differentiable_in u by A1, LM80;

      for v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in ( InvertibleOperators (Y,X)) holds (J . v) = ( Inv v)

      proof

        let v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X));

        assume v in ( InvertibleOperators (Y,X));

        then

        consider u be object such that

         A5: u in ( dom I) & v = (I . u) by A1, FUNCT_1:def 3;

        reconsider u as Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by A5;

        

         A7: ex u0 be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u = u0 & u0 is invertible by A1, A5;

        

        thus (J . v) = u by A1, A2, A5, FUNCT_1: 34

        .= ( Inv ( Inv u)) by A7, LOPBAN13: 15

        .= ( Inv v) by A1, A5;

      end;

      then for v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in ( InvertibleOperators (Y,X)) holds J is_differentiable_in v by A2, LM80;

      then J is_differentiable_on ( InvertibleOperators (Y,X)) by A2, NDIFF_1: 31;

      hence thesis by A1, A2, A4, LM80, NDIFF_1: 31;

    end;

    theorem :: NDIFF_9:19

    

     Th45: for E,G,F be RealNormSpace, 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:], A be Subset of E, B be Subset of F, g be PartFunc of E, F st Z is open & ( dom f) = Z & A is open & B is open & [:A, B:] c= Z & z = [a, b] & (f . (a,b)) = c & f is_differentiable_in z & ( dom g) = A & ( rng g) c= B & a in A & (g . a) = b & g is_continuous_in a & (for x be Point of E st x in A holds (f . (x,(g . x))) = c) & ( partdiff`2 (f,z)) is invertible holds g is_differentiable_in a & ( diff (g,a)) = ( - (( Inv ( partdiff`2 (f,z))) * ( partdiff`1 (f,z))))

    proof

      let E,G,F be RealNormSpace, 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:], A be Subset of E, B be Subset of F, g be PartFunc of E, F;

      assume

       A1: Z is open & ( dom f) = Z & A is open & B is open & [:A, B:] c= Z & z = [a, b] & (f . (a,b)) = c & f is_differentiable_in z & ( dom g) = A & ( rng g) c= B & a in A & (g . a) = b & g is_continuous_in a & (for x be Point of E st x in A holds (f . (x,(g . x))) = c) & ( partdiff`2 (f,z)) is invertible;

      then b in ( rng g) by FUNCT_1:def 3;

      then

      consider r2 be Real such that

       A3: 0 < r2 & ( Ball (b,r2)) c= B by A1, NDIFF_8: 20;

      consider r3 be Real such that

       A4: 0 < r3 & for x1 be Point of E st x1 in ( dom g) & ||.(x1 - a).|| < r3 holds ||.((g /. x1) - (g /. a)).|| < r2 by A1, A3, NFCONT_1: 7;

      consider r4 be Real such that

       A5: 0 < r4 & ( Ball (a,r4)) c= A by A1, NDIFF_8: 20;

      set r1 = ( min (r3,r4));

      

       A6: 0 < r1 & r1 <= r3 & r1 <= r4 by A4, A5, XXREAL_0: 17, XXREAL_0: 21;

      set g1 = (g | ( Ball (a,r1)));

      

       B6: ( Ball (a,r1)) c= ( Ball (a,r4)) by A6, NDIFF_8: 15;

      then

       A7: ( Ball (a,r1)) c= A by A5, XBOOLE_1: 1;

      

       A8: ( dom g1) = ( Ball (a,r1)) by A1, A5, B6, RELAT_1: 62, XBOOLE_1: 1;

       B8:

      now

        let y be object;

        assume

         A9: y in ( rng g1);

        then

        consider x be object such that

         A10: x in ( dom g1) & y = (g1 . x) by FUNCT_1:def 3;

        reconsider xp = x as Point of E by A10;

        

         A12: x in ( Ball (a,r4)) by A6, A8, A10, NDIFF_8: 15, TARSKI:def 3;

        reconsider yp = y as Point of F by A9;

        xp in { xx where xx be Point of E : ||.(xx - a).|| < r1 } by A8, A10, NDIFF_8: 17;

        then ex z be Point of E st z = xp & ||.(z - a).|| < r1;

        then ||.(xp - a).|| < r3 by A6, XXREAL_0: 2;

        then

         A13: ||.((g /. xp) - (g /. a)).|| < r2 by A1, A4, A5, A12;

        

         A14: y = (g . xp) by A8, A10, FUNCT_1: 49

        .= (g /. xp) by A1, A5, A12, PARTFUN1:def 6;

        b = (g /. a) by A1, PARTFUN1:def 6;

        then yp in { z where z be Point of F : ||.(z - b).|| < r2 } by A13, A14;

        hence y in ( Ball (b,r2)) by NDIFF_8: 17;

      end;

      

       A17: a in ( Ball (a,r1)) by A6, NDIFF_8: 13;

      

       A26: for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Point of E st x1 in ( dom g1) & ||.(x1 - a).|| < s holds ||.((g1 /. x1) - (g1 /. a)).|| < r

      proof

        let r be Real;

        assume 0 < r;

        then

        consider s be Real such that

         A20: 0 < s & for x1 be Point of E st x1 in ( dom g) & ||.(x1 - a).|| < s holds ||.((g /. x1) - (g /. a)).|| < r by A1, NFCONT_1: 7;

        take s;

        thus 0 < s by A20;

        let x1 be Point of E;

        assume

         A21: x1 in ( dom g1) & ||.(x1 - a).|| < s;

        

        then

         A25: (g /. x1) = (g . x1) by A1, A7, A8, PARTFUN1:def 6

        .= (g1 . x1) by A8, A21, FUNCT_1: 49

        .= (g1 /. x1) by A21, PARTFUN1:def 6;

        (g /. a) = (g . a) by A1, PARTFUN1:def 6

        .= (g1 . a) by A6, FUNCT_1: 49, NDIFF_8: 13

        .= (g1 /. a) by A6, A8, NDIFF_8: 13, PARTFUN1:def 6;

        hence ||.((g1 /. x1) - (g1 /. a)).|| < r by A1, A7, A8, A20, A21, A25;

      end;

      

       A28: for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g1 . x))) = c

      proof

        let x be Point of E;

        assume

         A29: x in ( Ball (a,r1));

        then (f . (x,(g . x))) = c by A1, A7;

        hence thesis by A29, FUNCT_1: 49;

      end;

      b in ( Ball (b,r2)) by A3, NDIFF_8: 13;

      then

       A31: [a, b] in [:( Ball (a,r1)), ( Ball (b,r2)):] by A17, ZFMISC_1: 87;

      

       A32: [:( Ball (a,r1)), ( Ball (b,r2)):] c= [:A, B:] by A3, A7, ZFMISC_1: 96;

      reconsider Q = (( partdiff`2 (f,z)) " ) as Lipschitzian LinearOperator of G, F by A1, LOPBAN_1:def 9;

      reconsider P = ( partdiff`1 (f,z)) as Lipschitzian LinearOperator of E, G by LOPBAN_1:def 9;

      Z is open & ( dom f) = Z & z = [a, b] & z in Z & (f . (a,b)) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & ( dom g1) = ( Ball (a,r1)) & ( rng g1) c= ( Ball (b,r2)) & (g1 . a) = b & g1 is_continuous_in a & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g1 . x))) = c) & ( partdiff`2 (f,z)) is one-to-one & Q = (( partdiff`2 (f,z)) " ) & P = ( partdiff`1 (f,z)) by A1, A3, A6, A8, B8, A26, A28, A31, A32, FUNCT_1: 49, NDIFF_8: 13, NFCONT_1: 7, TARSKI:def 3;

      then

       A33: g1 is_differentiable_in a & ( diff (g1,a)) = ( - (Q * P)) by Th5;

      then

      consider N be Neighbourhood of a such that

       A34: N c= ( dom g1) & ex R be RestFunc of E, F st for x be Point of E st x in N holds ((g1 /. x) - (g1 /. a)) = ((( diff (g1,a)) . (x - a)) + (R /. (x - a))) by NDIFF_1:def 7;

      consider R be RestFunc of E, F such that

       A35: for x be Point of E st x in N holds ((g1 /. x) - (g1 /. a)) = ((( diff (g1,a)) . (x - a)) + (R /. (x - a))) by A34;

      

       A37: N c= A by A7, A8, A34, XBOOLE_1: 1;

      

       A38: N c= ( dom g) by A1, A7, A8, A34, XBOOLE_1: 1;

      

       A39: for x be Point of E st x in N holds ((g /. x) - (g /. a)) = ((( diff (g1,a)) . (x - a)) + (R /. (x - a)))

      proof

        let x be Point of E;

        assume

         A40: x in N;

        

        then

         A46: (g /. x) = (g . x) by A1, A37, PARTFUN1:def 6

        .= (g1 . x) by A8, A34, A40, FUNCT_1: 49

        .= (g1 /. x) by A34, A40, PARTFUN1:def 6;

        (g /. a) = (g . a) by A1, PARTFUN1:def 6

        .= (g1 . a) by A6, FUNCT_1: 49, NDIFF_8: 13

        .= (g1 /. a) by A6, A8, NDIFF_8: 13, PARTFUN1:def 6;

        hence ((g /. x) - (g /. a)) = ((( diff (g1,a)) . (x - a)) + (R /. (x - a))) by A35, A40, A46;

      end;

      hence g is_differentiable_in a by A1, A7, A8, A34, NDIFF_1:def 6, XBOOLE_1: 1;

      then

       A48: ( diff (g,a)) = ( diff (g1,a)) by A38, A39, NDIFF_1:def 7;

      Q = ( Inv ( partdiff`2 (f,z))) by A1, LOPBAN13:def 2;

      then ( modetrans (( Inv ( partdiff`2 (f,z))),G,F)) = Q by LOPBAN_1:def 11;

      then

       A51: (( Inv ( partdiff`2 (f,z))) * ( partdiff`1 (f,z))) = (Q * P) by LOPBAN_1:def 11;

      then (Q * P) is Lipschitzian LinearOperator of E, F by LOPBAN_1:def 9;

      hence thesis by A33, A48, A51, LOPBAN13: 31;

    end;

    theorem :: NDIFF_9:20

    

     Th47: for E be RealNormSpace, G,F be non trivial RealBanachSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, c be Point of G, A be Subset of E, B be Subset of F, g be PartFunc of E, F st Z is open & ( dom f) = Z & A is open & B is open & [:A, B:] c= Z & f is_differentiable_on Z & (f `| Z) is_continuous_on Z & ( dom g) = A & ( rng g) c= B & g is_continuous_on A & (for x be Point of E st x in A holds (f . (x,(g . x))) = c) & (for x be Point of E, z be Point of [:E, F:] st x in A & z = [x, (g . x)] holds ( partdiff`2 (f,z)) is invertible) holds g is_differentiable_on A & (g `| A) is_continuous_on A & for x be Point of E, z be Point of [:E, F:] st x in A & z = [x, (g . x)] holds ( diff (g,x)) = ( - (( Inv ( partdiff`2 (f,z))) * ( partdiff`1 (f,z))))

    proof

      let E be RealNormSpace, G,F be non trivial RealBanachSpace, Z be Subset of [:E, F:], f be PartFunc of [:E, F:], G, c be Point of G, A be Subset of E, B be Subset of F, g be PartFunc of E, F;

      assume

       A1: Z is open & ( dom f) = Z & A is open & B is open & [:A, B:] c= Z & f is_differentiable_on Z & (f `| Z) is_continuous_on Z & ( dom g) = A & ( rng g) c= B & g is_continuous_on A & (for x be Point of E st x in A holds (f . (x,(g . x))) = c) & (for x be Point of E, z be Point of [:E, F:] st x in A & z = [x, (g . x)] holds ( partdiff`2 (f,z)) is invertible);

      then

       A2: f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & (f `partial`1| Z) is_continuous_on Z & (f `partial`2| Z) is_continuous_on Z by NDIFF_7: 52;

      

       A3: for x be Point of E, z be Point of [:E, F:] st x in A & z = [x, (g . x)] holds g is_differentiable_in x & ( diff (g,x)) = ( - (( Inv ( partdiff`2 (f,z))) * ( partdiff`1 (f,z))))

      proof

        let a be Point of E, z be Point of [:E, F:];

        assume

         A4: a in A & z = [a, (g . a)];

        then

         A5: (g . a) in ( rng g) by A1, FUNCT_1:def 3;

        then

        reconsider b = (g . a) as Point of F;

        

         A6: (f . (a,b)) = c by A1, A4;

        z in [:A, B:] by A1, A4, A5, ZFMISC_1: 87;

        then

         A9: f is_differentiable_in z by A1, NDIFF_1: 31;

        

         A10: (g | A) is_continuous_in a by A1, A4, NFCONT_1:def 7;

        

         A11: (g | A) = g by A1, RELAT_1: 68;

        ( partdiff`2 (f,z)) is invertible by A1, A4;

        hence g is_differentiable_in a & ( diff (g,a)) = ( - (( Inv ( partdiff`2 (f,z))) * ( partdiff`1 (f,z)))) by A1, A4, A6, A9, A10, A11, Th45;

      end;

      for x be Point of E st x in A holds g is_differentiable_in x

      proof

        let x be Point of E;

        assume

         A13: x in A;

        then (g . x) in ( rng g) by A1, FUNCT_1:def 3;

        then

        reconsider y = (g . x) as Point of F;

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

        then

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

        z = [x, (g . x)];

        hence thesis by A3, A13;

      end;

      hence

       A15: g is_differentiable_on A by A1, NDIFF_1: 31;

      then

       A16: ( dom (g `| A)) = A by NDIFF_1:def 9;

      consider xg be PartFunc of E, [:E, F:] such that

       A17: ( dom xg) = A & for x be Point of E st x in A holds (xg . x) = [x, (g . x)] and

       A18: xg is_continuous_on A by A1, LmTh471;

      consider BL be BilinearOperator of ( R_NormSpace_of_BoundedLinearOperators (E,G)), ( R_NormSpace_of_BoundedLinearOperators (G,F)), ( R_NormSpace_of_BoundedLinearOperators (E,F)) such that

       A19: BL is_continuous_on the carrier of [:( R_NormSpace_of_BoundedLinearOperators (E,G)), ( R_NormSpace_of_BoundedLinearOperators (G,F)):] & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)), v be Point of ( R_NormSpace_of_BoundedLinearOperators (G,F)) holds (BL . (u,v)) = (v * u) by LOPBAN13: 29;

      consider I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (F,G)), ( R_NormSpace_of_BoundedLinearOperators (G,F)) such that

       A20: ( dom I) = ( InvertibleOperators (F,G)) & ( rng I) = ( InvertibleOperators (G,F)) & I is one-to-one & I is_continuous_on ( InvertibleOperators (F,G)) & (ex J be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (G,F)), ( R_NormSpace_of_BoundedLinearOperators (F,G)) st J = (I " ) & J is one-to-one & ( dom J) = ( InvertibleOperators (G,F)) & ( rng J) = ( InvertibleOperators (F,G)) & J is_continuous_on ( InvertibleOperators (G,F))) & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) st u in ( InvertibleOperators (F,G)) holds (I . u) = ( Inv u) by LOPBAN13: 25;

      

       A21: ( dom (f `partial`1| Z)) = Z by A2, NDIFF_7:def 10;

      

       A22: ( dom (f `partial`2| Z)) = Z by A2, NDIFF_7:def 11;

      

       A23: for x be Point of E st x in A holds ((g `| A) /. x) = ( - (BL /. [(((f `partial`1| Z) * xg) . x), (((I * (f `partial`2| Z)) * xg) . x)]))

      proof

        let x be Point of E;

        assume

         A24: x in A;

        then

         A25: ((g `| A) /. x) = ( diff (g,x)) by A15, NDIFF_1:def 9;

        (xg /. x) = (xg . x) by A17, A24, PARTFUN1:def 6

        .= [x, (g . x)] by A17, A24;

        then ( partdiff`2 (f,(xg /. x))) is invertible by A1, A24;

        then ( partdiff`2 (f,(xg /. x))) in ( InvertibleOperators (F,G));

        then

         A27: (I . ( partdiff`2 (f,(xg /. x)))) = ( Inv ( partdiff`2 (f,(xg /. x)))) by A20;

         [( partdiff`1 (f,(xg /. x))), (I . ( partdiff`2 (f,(xg /. x))))] is set by TARSKI: 1;

        then [( partdiff`1 (f,(xg /. x))), (I . ( partdiff`2 (f,(xg /. x))))] is Point of [:( R_NormSpace_of_BoundedLinearOperators (E,G)), ( R_NormSpace_of_BoundedLinearOperators (G,F)):] by A27, PRVECT_3: 18;

        then [( partdiff`1 (f,(xg /. x))), (I . ( partdiff`2 (f,(xg /. x))))] in the carrier of [:( R_NormSpace_of_BoundedLinearOperators (E,G)), ( R_NormSpace_of_BoundedLinearOperators (G,F)):];

        then

         A28: [( partdiff`1 (f,(xg /. x))), (I . ( partdiff`2 (f,(xg /. x))))] in ( dom BL) by FUNCT_2:def 1;

        

         A29: (( Inv ( partdiff`2 (f,(xg /. x)))) * ( partdiff`1 (f,(xg /. x)))) = (BL . (( partdiff`1 (f,(xg /. x))),(I . ( partdiff`2 (f,(xg /. x)))))) by A19, A27

        .= (BL /. [( partdiff`1 (f,(xg /. x))), (I . ( partdiff`2 (f,(xg /. x))))]) by A28, PARTFUN1:def 6;

        

         A30: (g . x) in ( rng g) by A1, A24, FUNCT_1:def 3;

        then

        reconsider y = (g . x) as Point of F;

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

        then

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

        

         A33: z = (xg . x) & (xg . x) = (xg /. x) by A17, A24, PARTFUN1:def 6;

        

         A34: z in [:A, B:] by A1, A24, A30, ZFMISC_1: 87;

        

         A35: (((f `partial`1| Z) * xg) . x) = ((f `partial`1| Z) . (xg . x)) by A17, A24, FUNCT_1: 13

        .= ((f `partial`1| Z) /. (xg . x)) by A1, A21, A33, A34, PARTFUN1:def 6

        .= ( partdiff`1 (f,(xg /. x))) by A1, A2, A33, A34, NDIFF_7:def 10;

        (((I * (f `partial`2| Z)) * xg) . x) = ((I * (f `partial`2| Z)) . (xg . x)) by A17, A24, FUNCT_1: 13

        .= (I . ((f `partial`2| Z) . (xg . x))) by A1, A22, A33, A34, FUNCT_1: 13

        .= (I . ((f `partial`2| Z) /. (xg . x))) by A1, A22, A33, A34, PARTFUN1:def 6

        .= (I . ( partdiff`2 (f,(xg /. x)))) by A1, A2, A33, A34, NDIFF_7:def 11;

        hence thesis by A3, A24, A25, A29, A33, A35;

      end;

      

       A39: for x be Point of E st x in A holds x in ( dom ((f `partial`1| Z) * xg)) & ((f `partial`1| Z) * xg) is_continuous_in x

      proof

        let x be Point of E;

        assume

         A40: x in A;

        then

         A41: (g . x) in ( rng g) by A1, FUNCT_1:def 3;

         [x, (g . x)] is set by TARSKI: 1;

        then

        reconsider z = [x, (g . x)] as Point of [:E, F:] by A41, PRVECT_3: 18;

        

         A44: z in [:A, B:] by A1, A40, A41, ZFMISC_1: 87;

        

         A46: (xg . x) = [x, (g . x)] & (xg . x) = (xg /. x) by A17, A40, PARTFUN1:def 6;

        hence

         A47: x in ( dom ((f `partial`1| Z) * xg)) by A1, A17, A40, A21, A44, FUNCT_1: 11;

        (xg | A) is_continuous_in x by A18, A40, NFCONT_1:def 7;

        then

         A48: xg is_continuous_in x by A17, RELAT_1: 69;

        ((f `partial`1| Z) | Z) is_continuous_in (xg /. x) by A1, A2, A44, A46, NFCONT_1:def 7;

        then (f `partial`1| Z) is_continuous_in (xg /. x) by A21, RELAT_1: 69;

        hence thesis by A47, A48, NFCONT112;

      end;

      

       A49: for x be Point of E st x in A holds x in ( dom ((I * (f `partial`2| Z)) * xg)) & ((I * (f `partial`2| Z)) * xg) is_continuous_in x

      proof

        let x be Point of E;

        assume

         A50: x in A;

        then

         A51: (g . x) in ( rng g) by A1, FUNCT_1:def 3;

         [x, (g . x)] is set by TARSKI: 1;

        then

        reconsider z = [x, (g . x)] as Point of [:E, F:] by A51, PRVECT_3: 18;

        

         A54: z in [:A, B:] by A1, A50, A51, ZFMISC_1: 87;

        

         A56: (xg . x) = [x, (g . x)] & (xg . x) = (xg /. x) by A17, A50, PARTFUN1:def 6;

        (xg | A) is_continuous_in x by A18, A50, NFCONT_1:def 7;

        then

         A58: xg is_continuous_in x by A17, RELAT_1: 69;

        ((f `partial`2| Z) | Z) is_continuous_in (xg /. x) by A1, A2, A54, A56, NFCONT_1:def 7;

        then

         A61: (f `partial`2| Z) is_continuous_in (xg /. x) by A22, RELAT_1: 69;

        

         A62: ( partdiff`2 (f,(xg /. x))) is invertible by A1, A50, A56;

        then

         A63: ( partdiff`2 (f,(xg /. x))) in ( InvertibleOperators (F,G));

        

         A64: ( partdiff`2 (f,(xg /. x))) in ( dom I) by A20, A62;

        

         A65: ((f `partial`2| Z) /. (xg /. x)) = ( partdiff`2 (f,(xg /. x))) by A1, A2, A54, A56, NDIFF_7:def 11;

        then ((f `partial`2| Z) . (xg /. x)) in ( dom I) by A1, A22, A54, A56, A64, PARTFUN1:def 6;

        then

         A68: (xg /. x) in ( dom (I * (f `partial`2| Z))) by A1, A22, A54, A56, FUNCT_1: 11;

        hence

         A70: x in ( dom ((I * (f `partial`2| Z)) * xg)) by A17, A50, A56, FUNCT_1: 11;

        (I | ( InvertibleOperators (F,G))) is_continuous_in ((f `partial`2| Z) /. (xg /. x)) by A20, A63, A65, NFCONT_1:def 7;

        then I is_continuous_in ((f `partial`2| Z) /. (xg /. x)) by A20, RELAT_1: 69;

        then (I * (f `partial`2| Z)) is_continuous_in (xg /. x) by A61, A68, NFCONT112;

        hence thesis by A58, A70, NFCONT112;

      end;

      for x be object st x in A holds x in ( dom ((f `partial`1| Z) * xg)) by A39;

      then

       A72: A c= ( dom ((f `partial`1| Z) * xg)) by TARSKI:def 3;

      for x be object st x in A holds x in ( dom ((I * (f `partial`2| Z)) * xg)) by A49;

      then

       A74: A c= ( dom ((I * (f `partial`2| Z)) * xg)) by TARSKI:def 3;

      

       A75: for x be Point of E st x in A holds ((f `partial`1| Z) * xg) is_continuous_in x by A39;

      for x be Point of E st x in A holds ((I * (f `partial`2| Z)) * xg) is_continuous_in x by A49;

      then

      consider H be PartFunc of E, ( R_NormSpace_of_BoundedLinearOperators (E,F)) such that

       A77: ( dom H) = A & (for x be Point of E st x in A holds (H . x) = (BL . ((((f `partial`1| Z) * xg) . x),(((I * (f `partial`2| Z)) * xg) . x)))) & H is_continuous_on A by A19, A72, A74, A75, LmTh47;

      

       A78: for x0 be Point of E st x0 in A holds (BL . [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)]) = (BL /. [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)])

      proof

        let x0 be Point of E;

        assume x0 in A;

        then

         A82: (((f `partial`1| Z) * xg) . x0) in ( rng ((f `partial`1| Z) * xg)) & (((I * (f `partial`2| Z)) * xg) . x0) in ( rng ((I * (f `partial`2| Z)) * xg)) by A39, A49, FUNCT_1: 3;

         [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)] is set by TARSKI: 1;

        then [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)] is Point of [:( R_NormSpace_of_BoundedLinearOperators (E,G)), ( R_NormSpace_of_BoundedLinearOperators (G,F)):] by A82, PRVECT_3: 18;

        then [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)] in the carrier of [:( R_NormSpace_of_BoundedLinearOperators (E,G)), ( R_NormSpace_of_BoundedLinearOperators (G,F)):];

        then [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)] in ( dom BL) by FUNCT_2:def 1;

        hence (BL . [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)]) = (BL /. [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)]) by PARTFUN1:def 6;

      end;

      for x0 be Point of E st x0 in A holds ((g `| A) | A) is_continuous_in x0

      proof

        let x0 be Point of E;

        assume

         A83: x0 in A;

        then

         A85: x0 in ( dom ((g `| A) | A)) by A16, RELAT_1: 69;

        set F = ((g `| A) | A);

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Point of E st x1 in ( dom F) & ||.(x1 - x0).|| < s holds ||.((F /. x1) - (F /. x0)).|| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider s be Real such that

           A88: 0 < s & for x1 be Point of E st x1 in A & ||.(x1 - x0).|| < s holds ||.((H /. x1) - (H /. x0)).|| < r by A77, A83, NFCONT_1: 19;

          take s;

          thus 0 < s by A88;

          let x1 be Point of E;

          assume

           A89: x1 in ( dom F) & ||.(x1 - x0).|| < s;

          then

           A90: x1 in A by A16, RELAT_1: 69;

          then

           A91: ||.((H /. x1) - (H /. x0)).|| < r by A88, A89;

          

           A92: (H /. x1) = (H . x1) by A77, A90, PARTFUN1:def 6

          .= (BL . ((((f `partial`1| Z) * xg) . x1),(((I * (f `partial`2| Z)) * xg) . x1))) by A77, A90

          .= (BL /. [(((f `partial`1| Z) * xg) . x1), (((I * (f `partial`2| Z)) * xg) . x1)]) by A78, A90;

          

           A93: (F /. x1) = ((g `| A) /. x1) by A16, RELAT_1: 69

          .= ( - (H /. x1)) by A23, A90, A92;

          

           A94: (H /. x0) = (H . x0) by A77, A83, PARTFUN1:def 6

          .= (BL . ((((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0))) by A77, A83

          .= (BL /. [(((f `partial`1| Z) * xg) . x0), (((I * (f `partial`2| Z)) * xg) . x0)]) by A78, A83;

          (F /. x0) = ((g `| A) /. x0) by A16, RELAT_1: 69

          .= ( - (H /. x0)) by A23, A83, A94;

          

          then ((F /. x1) - (F /. x0)) = (( - (H /. x1)) + (H /. x0)) by A93, RLVECT_1: 17

          .= ( - ((H /. x1) - (H /. x0))) by RLVECT_1: 33;

          hence ||.((F /. x1) - (F /. x0)).|| < r by A91, NORMSP_1: 2;

        end;

        hence thesis by A85, NFCONT_1: 7;

      end;

      hence (g `| A) is_continuous_on A by A16, NFCONT_1:def 7;

      thus for x be Point of E, z be Point of [:E, F:] st x in A & z = [x, (g . x)] holds ( diff (g,x)) = ( - (( Inv ( partdiff`2 (f,z))) * ( partdiff`1 (f,z)))) by A3;

    end;

    theorem :: NDIFF_9:21

    for E be RealNormSpace, G,F be non trivial 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_differentiable_on Z & (f `| Z) is_continuous_on Z & [a, b] in Z & (f . (a,b)) = c & z = [a, b] & ( partdiff`2 (f,z)) is invertible 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 ( dom g) = ( Ball (a,r1)) & ( rng g) c= ( Ball (b,r2)) & g is_continuous_on ( Ball (a,r1)) & (g . a) = b & (for x be Point of E st x in ( Ball (a,r1)) holds (f . (x,(g . x))) = c) & g is_differentiable_on ( Ball (a,r1)) & (g `| ( Ball (a,r1))) is_continuous_on ( Ball (a,r1)) & (for x be Point of E, z be Point of [:E, F:] st x in ( Ball (a,r1)) & z = [x, (g . x)] holds ( diff (g,x)) = ( - (( Inv ( partdiff`2 (f,z))) * ( partdiff`1 (f,z))))) & (for x be Point of E, z be Point of [:E, F:] st x in ( Ball (a,r1)) & z = [x, (g . x)] holds ( partdiff`2 (f,z)) is invertible)) & (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 be RealNormSpace, G,F be non trivial RealBanachSpace, Z0 be Subset of [:E, F:], f0 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:];

      assume

       A1: Z0 is open & ( dom f0) = Z0 & f0 is_differentiable_on Z0 & (f0 `| Z0) is_continuous_on Z0 & [a, b] in Z0 & (f0 . (a,b)) = c & z = [a, b] & ( partdiff`2 (f0,z)) is invertible;

      then

       A2: f0 is_partial_differentiable_on`1 Z0 & f0 is_partial_differentiable_on`2 Z0 & (f0 `partial`1| Z0) is_continuous_on Z0 & (f0 `partial`2| Z0) is_continuous_on Z0 by NDIFF_7: 52;

      set DF0 = (f0 `| Z0);

      set PDF2 = (f0 `partial`2| Z0);

      

       A3: ( dom PDF2) = Z0 by A2, NDIFF_7:def 11;

      

       A4: ( partdiff`2 (f0,z)) in ( InvertibleOperators (F,G)) by A1;

      

       A5: (PDF2 . z) = (PDF2 /. z) by A1, A3, PARTFUN1:def 6;

      then (PDF2 . z) = ( partdiff`2 (f0,z)) by A1, A2, NDIFF_7:def 11;

      then

      consider p1 be Real such that

       A8: 0 < p1 & ( Ball ((PDF2 /. z),p1)) c= ( InvertibleOperators (F,G)) by A4, A5, NDIFF_8: 20;

      consider s1 be Real such that

       A9: 0 < s1 & for z1 be Point of [:E, F:] st z1 in Z0 & ||.(z1 - z).|| < s1 holds ||.((PDF2 /. z1) - (PDF2 /. z)).|| < p1 by A1, A2, A8, NFCONT_1: 19;

      consider s2 be Real such that

       A10: 0 < s2 & ( Ball (z,s2)) c= Z0 by A1, NDIFF_8: 20;

      set s = ( min (s1,s2));

      

       A11: 0 < s & s <= s1 & s <= s2 by A9, A10, XXREAL_0: 17, XXREAL_0: 21;

      set Z = ( Ball (z,s));

      set f = (f0 | Z);

      

       A12: z in Z by A11, NDIFF_8: 13;

      

       A15: (f . (a,b)) = c by A1, A11, FUNCT_1: 49, NDIFF_8: 13;

      

       A16: Z c= ( Ball (z,s2)) by A11, NDIFF_8: 15;

      then

       A18: Z c= Z0 by A10, XBOOLE_1: 1;

      

       A19: ( dom f) = Z by A1, A10, A16, RELAT_1: 62, XBOOLE_1: 1;

      f0 is_differentiable_on Z by A1, A10, A16, XBOOLE_1: 1, NDIFF_1: 46;

      then

       A20: for x be Point of [:E, F:] st x in Z holds (f0 | Z) is_differentiable_in x by NDIFF_1:def 8;

      

       A21: (f | Z) = (f0 | Z) by RELAT_1: 72;

      then

       A22: f is_differentiable_on Z by A19, A20, NDIFF_1:def 8;

      set DF = (f `| Z);

      

       A23: ( dom DF) = Z by A22, NDIFF_1:def 9;

      

       A24: for z be Point of [:E, F:] st z in Z holds ( diff (f0,z)) = ( diff (f,z))

      proof

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

        assume

         A25: z in Z;

        then f0 is_differentiable_in z by A1, A18, NDIFF_1: 31;

        hence ( diff (f0,z)) = ( diff (f,z)) by A1, A18, A25, LMDIFF;

      end;

      for x0 be Point of [:E, F:] holds for r be Real st x0 in Z & 0 < r holds ex s be Real st 0 < s & for x1 be Point of [:E, F:] st x1 in Z & ||.(x1 - x0).|| < s holds ||.((DF /. x1) - (DF /. x0)).|| < r

      proof

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

        let r be Real;

        assume

         A26: x0 in Z & 0 < r;

        then

        consider s be Real such that

         A28: 0 < s & for x1 be Point of [:E, F:] st x1 in Z0 & ||.(x1 - x0).|| < s holds ||.((DF0 /. x1) - (DF0 /. x0)).|| < r by A1, A18, NFCONT_1: 19;

        take s;

        thus 0 < s by A28;

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

        assume

         A29: x1 in Z & ||.(x1 - x0).|| < s;

        

        then

         A32: (DF /. x1) = ( diff (f,x1)) by A22, NDIFF_1:def 9

        .= ( diff (f0,x1)) by A24, A29

        .= (DF0 /. x1) by A1, A18, A29, NDIFF_1:def 9;

        (DF /. x0) = ( diff (f,x0)) by A22, A26, NDIFF_1:def 9

        .= ( diff (f0,x0)) by A24, A26

        .= (DF0 /. x0) by A1, A18, A26, NDIFF_1:def 9;

        hence ||.((DF /. x1) - (DF /. x0)).|| < r by A18, A28, A29, A32;

      end;

      then

       A34: (f `| Z) is_continuous_on Z by A23, NFCONT_1: 19;

      

       A35: f is_continuous_on Z by A19, A20, A21, NDIFF_1: 45, NDIFF_1:def 8;

      

       A36: f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & (f `partial`1| Z) is_continuous_on Z & (f `partial`2| Z) is_continuous_on Z by A22, A34, NDIFF_7: 52;

      

       A37: for z be Point of [:E, F:] st z in Z holds ( partdiff`1 (f0,z)) = ( partdiff`1 (f,z)) & ( partdiff`2 (f0,z)) = ( partdiff`2 (f,z))

      proof

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

        assume

         A38: z in Z;

        then (f0 | Z0) is_partial_differentiable_in`1 z by A2, A18;

        then f0 is_partial_differentiable_in`1 z by A1, RELAT_1: 69;

        hence ( partdiff`1 (f0,z)) = ( partdiff`1 (f,z)) by A1, A18, A38, LMPDIFF;

        (f0 | Z0) is_partial_differentiable_in`2 z by A2, A18, A38;

        then f0 is_partial_differentiable_in`2 z by A1, RELAT_1: 69;

        hence ( partdiff`2 (f0,z)) = ( partdiff`2 (f,z)) by A1, A18, A38, LMPDIFF;

      end;

      then ( partdiff`2 (f,z)) in { v where v be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) : v is invertible } by A4, A12;

      then

       A44: ex v be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) st ( partdiff`2 (f,z)) = v & v is invertible;

      then (( partdiff`2 (f,z)) " ) is Lipschitzian LinearOperator of G, F by LOPBAN_1:def 9;

      then

      consider r1,r2 be Real such that

       A47: 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) by A1, A11, A15, A19, A35, A36, A44, NDIFF_8: 13, NDIFF_8: 36;

      ( Ball (b,r2)) c= ( cl_Ball (b,r2)) by NDIFF_8: 15;

      then [:( Ball (a,r1)), ( Ball (b,r2)):] c= [:( Ball (a,r1)), ( cl_Ball (b,r2)):] by ZFMISC_1: 95;

      then

       A48: [:( Ball (a,r1)), ( Ball (b,r2)):] c= Z by A47, XBOOLE_1: 1;

      

       A49: for x be Point of E, y be Point of F st x in ( Ball (a,r1)) & y in ( Ball (b,r2)) holds (f0 . (x,y)) = (f . (x,y))

      proof

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

        assume x in ( Ball (a,r1)) & y in ( Ball (b,r2));

        then [x, y] in [:( Ball (a,r1)), ( Ball (b,r2)):] by ZFMISC_1: 87;

        hence thesis by A48, FUNCT_1: 49;

      end;

      take r1, r2;

      thus 0 < r1 & 0 < r2 by A47;

      thus [:( Ball (a,r1)), ( cl_Ball (b,r2)):] c= Z0 by A18, A47, XBOOLE_1: 1;

      thus 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)) & (f0 . (x,y)) = c

      proof

        let x be Point of E;

        assume

         A52: x in ( Ball (a,r1));

        then

        consider y be Point of F such that

         A53: y in ( Ball (b,r2)) & (f . (x,y)) = c by A47;

        take y;

        thus y in ( Ball (b,r2)) by A53;

        thus (f0 . (x,y)) = c by A49, A52, A53;

      end;

      thus 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)) & (f0 . (x,y1)) = c & (f0 . (x,y2)) = c holds y1 = y2

      proof

        let x be Point of E;

        assume

         A54: x in ( Ball (a,r1));

        let y1,y2 be Point of F such that

         A55: y1 in ( Ball (b,r2)) & y2 in ( Ball (b,r2)) & (f0 . (x,y1)) = c & (f0 . (x,y2)) = c;

        

         A56: (f . (x,y1)) = c by A49, A54, A55;

        (f . (x,y2)) = c by A49, A54, A55;

        hence y1 = y2 by A47, A54, A55, A56;

      end;

      consider g be PartFunc of E, F such that

       A57: 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 by A47;

      

       A58: for x be Point of E, w be Point of [:E, F:] st x in ( Ball (a,r1)) & w = [x, (g . x)] holds ( partdiff`2 (f0,w)) is invertible

      proof

        let x be Point of E, w be Point of [:E, F:];

        assume

         A59: x in ( Ball (a,r1)) & w = [x, (g . x)];

        then (g . x) in ( rng g) by A57, FUNCT_1: 3;

        then w in [:( Ball (a,r1)), ( Ball (b,r2)):] by A57, A59, ZFMISC_1: 87;

        then

         A60: w in Z by A48;

        then w in { y where y be Point of [:E, F:] : ||.(y - z).|| < s } by NDIFF_8: 17;

        then ex y be Point of [:E, F:] st w = y & ||.(y - z).|| < s;

        then ||.(w - z).|| < s1 by A11, XXREAL_0: 2;

        then ||.((PDF2 /. w) - (PDF2 /. z)).|| < p1 by A9, A18, A60;

        then (PDF2 /. w) in { y where y be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) : ||.(y - (PDF2 /. z)).|| < p1 };

        then (PDF2 /. w) in ( Ball ((PDF2 /. z),p1)) by NDIFF_8: 17;

        then (PDF2 /. w) in ( InvertibleOperators (F,G)) by A8;

        then ( partdiff`2 (f0,w)) in ( InvertibleOperators (F,G)) by A2, A18, A60, NDIFF_7:def 11;

        then ex v be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) st ( partdiff`2 (f0,w)) = v & v is invertible;

        hence ( partdiff`2 (f0,w)) is invertible;

      end;

      

       A63: for x be Point of E, w be Point of [:E, F:] st x in ( Ball (a,r1)) & w = [x, (g . x)] holds ( partdiff`2 (f,w)) is invertible

      proof

        let x be Point of E, w be Point of [:E, F:];

        assume

         A64: x in ( Ball (a,r1)) & w = [x, (g . x)];

        then (g . x) in ( rng g) by A57, FUNCT_1: 3;

        then w in [:( Ball (a,r1)), ( Ball (b,r2)):] by A57, A64, ZFMISC_1: 87;

        then ( partdiff`2 (f,w)) = ( partdiff`2 (f0,w)) & ( partdiff`1 (f,w)) = ( partdiff`1 (f0,w)) by A37, A48;

        hence thesis by A58, A64;

      end;

      

       A68: for x be Point of E st x in ( Ball (a,r1)) holds (f0 . (x,(g . x))) = c

      proof

        let x be Point of E;

        assume

         A69: x in ( Ball (a,r1));

        then (g . x) in ( rng g) by A57, FUNCT_1: 3;

        then (f0 . (x,(g . x))) = (f . (x,(g . x))) by A49, A57, A69;

        hence (f0 . (x,(g . x))) = c by A57, A69;

      end;

      

       A70: g is_differentiable_on ( Ball (a,r1)) & (g `| ( Ball (a,r1))) is_continuous_on ( Ball (a,r1)) & for x be Point of E, z be Point of [:E, F:] st x in ( Ball (a,r1)) & z = [x, (g . x)] holds ( diff (g,x)) = ( - (( Inv ( partdiff`2 (f0,z))) * ( partdiff`1 (f0,z))))

      proof

        for x be Point of E, z be Point of [:E, F:] st x in ( Ball (a,r1)) & z = [x, (g . x)] holds ( diff (g,x)) = ( - (( Inv ( partdiff`2 (f0,z))) * ( partdiff`1 (f0,z))))

        proof

          let x be Point of E, z be Point of [:E, F:];

          assume

           A73: x in ( Ball (a,r1)) & z = [x, (g . x)];

          then (g . x) in ( rng g) by A57, FUNCT_1: 3;

          then z in [:( Ball (a,r1)), ( Ball (b,r2)):] by A57, A73, ZFMISC_1: 87;

          then ( partdiff`2 (f,z)) = ( partdiff`2 (f0,z)) & ( partdiff`1 (f,z)) = ( partdiff`1 (f0,z)) by A37, A48;

          hence thesis by A19, A22, A34, A48, A57, A63, A73, Th47;

        end;

        hence thesis by A19, A22, A34, A48, A57, A63, Th47;

      end;

      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 (f0 . (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 (f0 . (x,(g2 . x))) = c) holds g1 = g2

      proof

        let g1,g2 be PartFunc of E, F;

        assume

         A75: ( dom g1) = ( Ball (a,r1)) & ( rng g1) c= ( Ball (b,r2)) & (for x be Point of E st x in ( Ball (a,r1)) holds (f0 . (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 (f0 . (x,(g2 . x))) = c);

         A76:

        now

          let x be Point of E;

          assume

           A77: x in ( Ball (a,r1));

          then (g1 . x) in ( rng g1) by A75, FUNCT_1: 3;

          then (f0 . (x,(g1 . x))) = (f . (x,(g1 . x))) by A49, A75, A77;

          hence (f . (x,(g1 . x))) = c by A75, A77;

        end;

        now

          let x be Point of E;

          assume

           A78: x in ( Ball (a,r1));

          then (g2 . x) in ( rng g2) by A75, FUNCT_1: 3;

          then (f0 . (x,(g2 . x))) = (f . (x,(g2 . x))) by A49, A75, A78;

          hence (f . (x,(g2 . x))) = c by A75, A78;

        end;

        hence g1 = g2 by A47, A75, A76;

      end;

      hence thesis by A57, A58, A68, A70;

    end;