ndiff_7.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;

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

    theorem :: NDIFF_7:1

    

     FX1: for X be set, I,f be Function holds ((f | X) * I) = ((f * I) | (I " X))

    proof

      let X be set, I,f be Function;

      

       P1: ( dom ((f | X) * I)) = (I " ( dom (f | X))) by RELAT_1: 147;

      

       P2: (I " ( dom (f | X))) = (I " (( dom f) /\ X)) by RELAT_1: 61

      .= ((I " ( dom f)) /\ (I " X)) by FUNCT_1: 68

      .= (( dom (f * I)) /\ (I " X)) by RELAT_1: 147

      .= ( dom ((f * I) | (I " X))) by RELAT_1: 61;

      now

        let x be object;

        assume

         Q1: x in ( dom ((f | X) * I));

        then x in (I " ( dom (f | X))) by RELAT_1: 147;

        then

         Q3: x in ( dom I) & (I . x) in ( dom (f | X)) by FUNCT_1:def 7;

        

        thus (((f | X) * I) . x) = ((f | X) . (I . x)) by FUNCT_1: 12, Q1

        .= (f . (I . x)) by FUNCT_1: 47, Q3

        .= ((f * I) . x) by FUNCT_1: 13, Q3

        .= (((f * I) | (I " X)) . x) by FUNCT_1: 47, Q1, P1, P2;

      end;

      hence thesis by P2, FUNCT_1: 2, RELAT_1: 147;

    end;

    theorem :: NDIFF_7:2

    

     LM001: for S,T be RealNormSpace, L be LinearOperator of S, T, x,y be Point of S holds ((L . x) - (L . y)) = (L . (x - y))

    proof

      let S,T be RealNormSpace, L be LinearOperator of S, T, x,x0 be Point of S;

      

      thus ((L . x) - (L . x0)) = ((L . x) + (( - 1) * (L . x0))) by RLVECT_1: 16

      .= ((L . x) + (L . (( - 1) * x0))) by LOPBAN_1:def 5

      .= (L . (x + (( - 1) * x0))) by VECTSP_1:def 20

      .= (L . (x - x0)) by RLVECT_1: 16;

    end;

    theorem :: NDIFF_7:3

    

     Th26: for X,Y,W be RealNormSpace, I be Function of X, Y, f1,f2 be PartFunc of Y, W holds ((f1 + f2) * I) = ((f1 * I) + (f2 * I)) & ((f1 - f2) * I) = ((f1 * I) - (f2 * I))

    proof

      let X,Y,W be RealNormSpace, I be Function of X, Y, f1,f2 be PartFunc of Y, W;

      set DI = the carrier of X;

      

       A1: ( dom I) = DI by FUNCT_2:def 1;

      

       A2: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 1;

      

       A3b: for s be Element of DI holds s in ( dom ((f1 + f2) * I)) iff s in ( dom ((f1 * I) + (f2 * I)))

      proof

        let s be Element of DI;

        s in ( dom ((f1 + f2) * I)) iff (I . s) in (( dom f1) /\ ( dom f2)) by A2, A1, FUNCT_1: 11;

        then s in ( dom ((f1 + f2) * I)) iff (I . s) in ( dom f1) & (I . s) in ( dom f2) by XBOOLE_0:def 4;

        then s in ( dom ((f1 + f2) * I)) iff s in ( dom (f1 * I)) & s in ( dom (f2 * I)) by A1, FUNCT_1: 11;

        then s in ( dom ((f1 + f2) * I)) iff s in (( dom (f1 * I)) /\ ( dom (f2 * I))) by XBOOLE_0:def 4;

        hence thesis by VFUNCT_1:def 1;

      end;

      then

       A3: for s be object holds s in ( dom ((f1 + f2) * I)) iff s in ( dom ((f1 * I) + (f2 * I)));

      then

       A3a: ( dom ((f1 + f2) * I)) = ( dom ((f1 * I) + (f2 * I))) by TARSKI: 2;

      

       A4: for z be Element of DI st z in ( dom ((f1 + f2) * I)) holds (((f1 + f2) * I) . z) = (((f1 * I) + (f2 * I)) . z)

      proof

        let z be Element of DI;

        assume

         A5: z in ( dom ((f1 + f2) * I));

        then

         A6: (I . z) in ( dom (f1 + f2)) by FUNCT_1: 11;

        z in (( dom (f1 * I)) /\ ( dom (f2 * I))) by A3a, A5, VFUNCT_1:def 1;

        then

         A7: z in ( dom (f1 * I)) & z in ( dom (f2 * I)) by XBOOLE_0:def 4;

        

         A8: (I . z) in (( dom f1) /\ ( dom f2)) by A2, A5, FUNCT_1: 11;

        then (I . z) in ( dom f1) by XBOOLE_0:def 4;

        

        then

         A9: (f1 /. (I . z)) = (f1 . (I . z)) by PARTFUN1:def 6

        .= ((f1 * I) . z) by A7, FUNCT_1: 12

        .= ((f1 * I) /. z) by A7, PARTFUN1:def 6;

        (I . z) in ( dom f2) by A8, XBOOLE_0:def 4;

        

        then

         A10: (f2 /. (I . z)) = (f2 . (I . z)) by PARTFUN1:def 6

        .= ((f2 * I) . z) by A7, FUNCT_1: 12

        .= ((f2 * I) /. z) by A7, PARTFUN1:def 6;

        (((f1 + f2) * I) . z) = ((f1 + f2) . (I . z)) by A5, FUNCT_1: 12

        .= ((f1 + f2) /. (I . z)) by A6, PARTFUN1:def 6

        .= ((f1 /. (I . z)) + (f2 /. (I . z))) by A6, VFUNCT_1:def 1

        .= (((f1 * I) + (f2 * I)) /. z) by A3b, A5, A9, A10, VFUNCT_1:def 1;

        hence thesis by A3b, A5, PARTFUN1:def 6;

      end;

      

       A11: ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 2;

      

       A12b: for s be Element of DI holds s in ( dom ((f1 - f2) * I)) iff s in ( dom ((f1 * I) - (f2 * I)))

      proof

        let s be Element of DI;

        s in ( dom ((f1 - f2) * I)) iff (I . s) in (( dom f1) /\ ( dom f2)) by A11, A1, FUNCT_1: 11;

        then s in ( dom ((f1 - f2) * I)) iff (I . s) in ( dom f1) & (I . s) in ( dom f2) by XBOOLE_0:def 4;

        then s in ( dom ((f1 - f2) * I)) iff s in ( dom (f1 * I)) & s in ( dom (f2 * I)) by A1, FUNCT_1: 11;

        then s in ( dom ((f1 - f2) * I)) iff s in (( dom (f1 * I)) /\ ( dom (f2 * I))) by XBOOLE_0:def 4;

        hence thesis by VFUNCT_1:def 2;

      end;

      then

       A12: for s be object holds s in ( dom ((f1 - f2) * I)) iff s in ( dom ((f1 * I) - (f2 * I)));

      then

       A12a: ( dom ((f1 - f2) * I)) = ( dom ((f1 * I) - (f2 * I))) by TARSKI: 2;

      for z be Element of DI st z in ( dom ((f1 - f2) * I)) holds (((f1 - f2) * I) . z) = (((f1 * I) - (f2 * I)) . z)

      proof

        let z be Element of DI;

        assume

         A13: z in ( dom ((f1 - f2) * I));

        then

         A14: (I . z) in ( dom (f1 - f2)) by FUNCT_1: 11;

        z in (( dom (f1 * I)) /\ ( dom (f2 * I))) by A12a, A13, VFUNCT_1:def 2;

        then

         A15: z in ( dom (f1 * I)) & z in ( dom (f2 * I)) by XBOOLE_0:def 4;

        

         A16: (I . z) in (( dom f1) /\ ( dom f2)) by A11, A13, FUNCT_1: 11;

        then (I . z) in ( dom f1) by XBOOLE_0:def 4;

        

        then

         A17: (f1 /. (I . z)) = (f1 . (I . z)) by PARTFUN1:def 6

        .= ((f1 * I) . z) by A15, FUNCT_1: 12

        .= ((f1 * I) /. z) by A15, PARTFUN1:def 6;

        (I . z) in ( dom f2) by A16, XBOOLE_0:def 4;

        

        then

         A18: (f2 /. (I . z)) = (f2 . (I . z)) by PARTFUN1:def 6

        .= ((f2 * I) . z) by A15, FUNCT_1: 12

        .= ((f2 * I) /. z) by A15, PARTFUN1:def 6;

        

        thus (((f1 - f2) * I) . z) = ((f1 - f2) . (I . z)) by A13, FUNCT_1: 12

        .= ((f1 - f2) /. (I . z)) by A14, PARTFUN1:def 6

        .= ((f1 /. (I . z)) - (f2 /. (I . z))) by A14, VFUNCT_1:def 2

        .= (((f1 * I) - (f2 * I)) /. z) by A12b, A13, A17, A18, VFUNCT_1:def 2

        .= (((f1 * I) - (f2 * I)) . z) by A12b, A13, PARTFUN1:def 6;

      end;

      hence thesis by A3, A12, A4, TARSKI: 2, PARTFUN1: 5;

    end;

    theorem :: NDIFF_7:4

    

     Th27: for X,Y,W be RealNormSpace, I be Function of X, Y, f be PartFunc of Y, W, r be Real holds (r (#) (f * I)) = ((r (#) f) * I)

    proof

      let X,Y,W be RealNormSpace, I be Function of X, Y, f be PartFunc of Y, W, r be Real;

      set DI = the carrier of X;

      

       A1: ( dom (r (#) f)) = ( dom f) by VFUNCT_1:def 4;

      

       A2: ( dom (r (#) (f * I))) = ( dom (f * I)) by VFUNCT_1:def 4;

      

       A3: ( dom I) = DI by FUNCT_2:def 1;

      

       A4b: for s be Element of DI holds s in ( dom ((r (#) f) * I)) iff s in ( dom (f * I))

      proof

        let s be Element of DI;

        s in ( dom ((r (#) f) * I)) iff (I . s) in ( dom (r (#) f)) by A3, FUNCT_1: 11;

        hence thesis by A1, A3, FUNCT_1: 11;

      end;

      then

       A4: for s be object holds s in ( dom (r (#) (f * I))) iff s in ( dom ((r (#) f) * I)) by A2;

      then

       A4a: ( dom (r (#) (f * I))) = ( dom ((r (#) f) * I)) by TARSKI: 2;

      

       A5: for s be Element of DI holds s in ( dom ((r (#) f) * I)) iff (I . s) in ( dom (r (#) f))

      proof

        let s be Element of DI;

        ( dom I) = DI by FUNCT_2:def 1;

        hence thesis by FUNCT_1: 11;

      end;

      for z be Element of DI st z in ( dom (r (#) (f * I))) holds ((r (#) (f * I)) . z) = (((r (#) f) * I) . z)

      proof

        let z be Element of DI;

        assume

         A6: z in ( dom (r (#) (f * I)));

        then

         A7: z in ( dom (f * I)) by VFUNCT_1:def 4;

        

         A9: (f /. (I . z)) = (f . (I . z)) by A1, A5, A4a, A6, PARTFUN1:def 6

        .= ((f * I) . z) by A7, FUNCT_1: 12

        .= ((f * I) /. z) by A7, PARTFUN1:def 6;

        

         A10: ((r (#) (f * I)) . z) = ((r (#) (f * I)) /. z) by A6, PARTFUN1:def 6

        .= (r * (f /. (I . z))) by A6, A9, VFUNCT_1:def 4;

        (((r (#) f) * I) . z) = ((r (#) f) . (I . z)) by A2, A4b, A6, FUNCT_1: 12

        .= ((r (#) f) /. (I . z)) by A5, A4a, A6, PARTFUN1:def 6

        .= (r * (f /. (I . z))) by A5, A4a, A6, VFUNCT_1:def 4;

        hence thesis by A10;

      end;

      hence thesis by A4, TARSKI: 2, PARTFUN1: 5;

    end;

    theorem :: NDIFF_7:5

    

     LM030: for f be PartFunc of T, W, g be Function of S, T, x be Point of S st x in ( dom g) & (g /. x) in ( dom f) & g is_continuous_in x & f is_continuous_in (g /. x) holds (f * g) is_continuous_in x

    proof

      let f be PartFunc of T, W, g be Function of S, T, x be Point of S;

      assume that

       AS1: x in ( dom g) and

       AS2: (g /. x) in ( dom f) and

       AS3: g is_continuous_in x and

       AS4: f is_continuous_in (g /. x);

      set h = (f * g);

      

       P1: x in ( dom h) by AS1, AS2, PARTFUN2: 3;

      for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Point of S st x1 in ( dom h) & ||.(x1 - x).|| < s holds ||.((h /. x1) - (h /. x)).|| < r

      proof

        let r be Real;

        assume 0 < r;

        then

        consider t be Real such that

         P2: 0 < t & for y1 be Point of T st y1 in ( dom f) & ||.(y1 - (g /. x)).|| < t holds ||.((f /. y1) - (f /. (g /. x))).|| < r by AS4, NFCONT_1: 7;

        consider s be Real such that

         P3: 0 < s & for x1 be Point of S st x1 in ( dom g) & ||.(x1 - x).|| < s holds ||.((g /. x1) - (g /. x)).|| < t by P2, AS3, NFCONT_1: 7;

        take s;

        thus 0 < s by P3;

        let x1 be Point of S;

        assume

         P4: x1 in ( dom h) & ||.(x1 - x).|| < s;

        then

         P7: x1 in ( dom g) & (g /. x1) in ( dom f) by PARTFUN2: 3;

        then

         P5: ||.((g /. x1) - (g /. x)).|| < t by P3, P4;

        (h /. x1) = (f /. (g /. x1)) & (h /. x) = (f /. (g /. x)) by P4, AS1, AS2, PARTFUN2: 3, PARTFUN2: 4;

        hence ||.((h /. x1) - (h /. x)).|| < r by P2, P5, P7;

      end;

      hence h is_continuous_in x by NFCONT_1: 7, P1;

    end;

    definition

      let X,Y be RealNormSpace;

      let x be Element of [:X, Y:];

      :: NDIFF_7:def1

      func reproj1 (x) -> Function of X, [:X, Y:] means

      : Defrep1: for r be Element of X holds (it . r) = [r, (x `2 )];

      existence

      proof

        reconsider x1 = x as Element of [:the carrier of X, the carrier of Y:];

        defpred S1[ Element of X, Element of the carrier of [:X, Y:]] means $2 = [$1, (x1 `2 )];

        

         A1: for r be Element of X holds ex y be Element of the carrier of [:X, Y:] st S1[r, y]

        proof

          let r be Element of X;

          consider p1 be Point of X, p2 be Point of Y such that

           X1: x = [p1, p2] by PRVECT_3: 18;

           [r, (x1 `2 )] in [:the carrier of X, the carrier of Y:] by X1, ZFMISC_1:def 2;

          hence ex y be Element of the carrier of [:X, Y:] st S1[r, y];

        end;

        ex f be Function of the carrier of X, the carrier of [:X, Y:] st for r be Element of X holds S1[r, (f . r)] from FUNCT_2:sch 3( A1);

        hence ex b1 be Function of X, [:X, Y:] st for r be Element of X holds (b1 . r) = [r, (x `2 )];

      end;

      uniqueness

      proof

        let f,g be Function of the carrier of X, the carrier of [:X, Y:];

        assume that

         A2: for r be Element of X holds (f . r) = [r, (x `2 )] and

         A3: for r be Element of X holds (g . r) = [r, (x `2 )];

        now

          let r be Element of X;

          (f . r) = [r, (x `2 )] by A2;

          hence (f . r) = (g . r) by A3;

        end;

        hence f = g;

      end;

      :: NDIFF_7:def2

      func reproj2 (x) -> Function of Y, [:X, Y:] means

      : Defrep2: for r be Element of Y holds (it . r) = [(x `1 ), r];

      existence

      proof

        reconsider x1 = x as Element of [:the carrier of X, the carrier of Y:];

        defpred S1[ Element of Y, Element of the carrier of [:X, Y:]] means $2 = [(x1 `1 ), $1];

        

         A1: for r be Element of Y holds ex y be Element of the carrier of [:X, Y:] st S1[r, y]

        proof

          let r be Element of Y;

          consider p1 be Point of X, p2 be Point of Y such that

           X1: x = [p1, p2] by PRVECT_3: 18;

           [(x1 `1 ), r] in [:the carrier of X, the carrier of Y:] by X1, ZFMISC_1:def 2;

          hence ex y be Element of the carrier of [:X, Y:] st S1[r, y];

        end;

        ex f be Function of the carrier of Y, the carrier of [:X, Y:] st for r be Element of Y holds S1[r, (f . r)] from FUNCT_2:sch 3( A1);

        hence ex b1 be Function of Y, [:X, Y:] st for r be Element of Y holds (b1 . r) = [(x `1 ), r];

      end;

      uniqueness

      proof

        let f,g be Function of the carrier of Y, the carrier of [:X, Y:];

        assume that

         A2: for r be Element of Y holds (f . r) = [(x `1 ), r] and

         A3: for r be Element of Y holds (g . r) = [(x `1 ), r];

        now

          let r be Element of Y;

          (f . r) = [(x `1 ), r] by A2;

          hence (f . r) = (g . r) by A3;

        end;

        hence f = g;

      end;

    end

    begin

    theorem :: NDIFF_7:6

    

     LM010: for I be LinearOperator of S, T, x be Point of S st I is isometric holds I is_continuous_in x

    proof

      let I be LinearOperator of S, T, x0 be Point of S;

      assume

       AS1: I is isometric;

      

       P1: ( dom I) = the carrier of S by FUNCT_2:def 1;

      for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Point of S st x1 in ( dom I) & ||.(x1 - x0).|| < s holds ||.((I /. x1) - (I /. x0)).|| < r

      proof

        let r be Real;

        assume

         P2: 0 < r;

        take s = r;

        thus 0 < s by P2;

        let x1 be Point of S;

        assume

         P3: x1 in ( dom I) & ||.(x1 - x0).|| < s;

        thus thesis by AS1, P3;

      end;

      hence thesis by NFCONT_1: 7, P1;

    end;

    theorem :: NDIFF_7:7

    

     LMMAZU: for S,T be RealNormSpace, f be LinearOperator of S, T holds f is isometric iff for x be Element of S holds ||.(f . x).|| = ||.x.||

    proof

      let S,T be RealNormSpace, f be LinearOperator of S, T;

      hereby

        assume

         A1: f is isometric;

        thus for x be Element of S holds ||.(f . x).|| = ||.x.||

        proof

          let x be Element of S;

          

          thus ||.(f . x).|| = ||.(f . (x - ( 0. S))).|| by RLVECT_1: 13

          .= ||.((f . x) - (f . ( 0. S))).|| by LM001

          .= ||.(x - ( 0. S)).|| by A1

          .= ||.x.|| by RLVECT_1: 13;

        end;

      end;

      assume

       A2: for x be Element of S holds ||.(f . x).|| = ||.x.||;

      for a,b be Point of S holds ||.((f . a) - (f . b)).|| = ||.(a - b).||

      proof

        let a,b be Point of S;

        

        thus ||.((f . a) - (f . b)).|| = ||.(f . (a - b)).|| by LM001

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

      end;

      hence thesis;

    end;

    theorem :: NDIFF_7:8

    

     LM015: for I be LinearOperator of S, T, Z be Subset of S st I is isometric holds I is_continuous_on Z

    proof

      let I be LinearOperator of S, T, Z be Subset of S;

      assume

       AS: I is isometric;

      

       P1: ( dom I) = the carrier of S by FUNCT_2:def 1;

      for x be Point of S st x in ( dom I) holds (I | ( dom I)) is_continuous_in x by AS, LM010;

      hence thesis by P1, NFCONT_1: 23, NFCONT_1:def 7;

    end;

    theorem :: NDIFF_7:9

    

     LM020: for I be LinearOperator of S, T st I is one-to-one onto isometric holds ex J be LinearOperator of T, S st J = (I " ) & J is one-to-one onto isometric

    proof

      let I be LinearOperator of S, T;

      assume that

       AS0: I is one-to-one onto and

       AS1: I is isometric;

      

       P0: ( rng I) = the carrier of T & ( dom I) = the carrier of S by AS0, FUNCT_2:def 1;

      

       P1: ( rng I) = ( dom (I " )) & ( dom I) = ( rng (I " )) by AS0, FUNCT_1: 33;

      then

      reconsider J = (I " ) as Function of T, S by P0, FUNCT_2: 1;

      

       X1: for v,w be Point of T holds (J . (v + w)) = ((J . v) + (J . w))

      proof

        let v,w be Point of T;

        consider t be Point of S such that

         X1: v = (I . t) by AS0, FUNCT_2: 113;

        consider s be Point of S such that

         X2: w = (I . s) by AS0, FUNCT_2: 113;

        

         X3: (J . (v + w)) = (J . (I . (t + s))) by X1, X2, VECTSP_1:def 20

        .= (t + s) by FUNCT_1: 34, AS0, P0;

        (J . w) = s by X2, FUNCT_1: 34, AS0, P0;

        hence thesis by AS0, P0, X1, X3, FUNCT_1: 34;

      end;

      

       X2: for v be Point of T, r be Real holds (J . (r * v)) = (r * (J . v))

      proof

        let v be Point of T, r be Real;

        consider t be Point of S such that

         X1: v = (I . t) by AS0, FUNCT_2: 113;

        (J . (r * v)) = (J . (I . (r * t))) by X1, LOPBAN_1:def 5

        .= (r * t) by FUNCT_1: 34, AS0, P0;

        hence thesis by AS0, P0, X1, FUNCT_1: 34;

      end;

      reconsider J as LinearOperator of T, S by X1, X2, LOPBAN_1:def 5, VECTSP_1:def 20;

      take J;

      thus J = (I " );

      thus J is one-to-one onto by AS0, P1, FUNCT_2:def 1;

      for v be Point of T holds ||.(J . v).|| = ||.v.||

      proof

        let v be Point of T;

        consider t be Point of S such that

         X1: v = (I . t) by AS0, FUNCT_2: 113;

        

        thus ||.(J . v).|| = ||.t.|| by X1, FUNCT_1: 34, AS0, P0

        .= ||.v.|| by X1, AS1, LMMAZU;

      end;

      hence thesis by LMMAZU;

    end;

    theorem :: NDIFF_7:10

    

     LM021: for I be LinearOperator of S, T, s1 be sequence of S st I is isometric & s1 is convergent holds (I * s1) is convergent & ( lim (I * s1)) = (I . ( lim s1))

    proof

      let I be LinearOperator of S, T, s1 be sequence of S;

      assume

       AS: I is isometric & s1 is convergent;

      

       P1: ( dom I) = the carrier of S by FUNCT_2:def 1;

      

       P22: ( rng s1) c= ( dom I) by P1;

      I is_continuous_in ( lim s1) by AS, LM010;

      then (I /* s1) is convergent & (I /. ( lim s1)) = ( lim (I /* s1)) by NFCONT_1:def 5, AS, P22;

      hence thesis by P22, FUNCT_2:def 11;

    end;

    theorem :: NDIFF_7:11

    

     LM022: for I be LinearOperator of S, T, s1 be sequence of S st I is one-to-one onto isometric holds (s1 is convergent iff (I * s1) is convergent)

    proof

      let I be LinearOperator of S, T, s1 be sequence of S;

      assume

       AS: I is one-to-one onto isometric;

      consider J be LinearOperator of T, S such that

       P2: J = (I " ) & J is one-to-one onto isometric by AS, LM020;

      thus s1 is convergent implies (I * s1) is convergent by LM021, AS;

      assume

       P4: (I * s1) is convergent;

      

       P6: ( rng s1) c= the carrier of S;

      (J * (I * s1)) = ((J * I) * s1) by RELAT_1: 36

      .= (( id the carrier of S) * s1) by AS, P2, FUNCT_2: 29

      .= s1 by RELAT_1: 53, P6;

      hence s1 is convergent by P2, P4, LM021;

    end;

    

     LM023: for I be LinearOperator of S, T, Z be Subset of S st I is one-to-one onto isometric & Z is closed holds (I .: Z) is closed

    proof

      let I be LinearOperator of S, T, Z be Subset of S;

      assume that

       A1: I is one-to-one onto and

       A2: I is isometric and

       A3: Z is closed;

      

       P1: ( dom I) = the carrier of S by FUNCT_2:def 1;

      consider J be LinearOperator of T, S such that

       P2: J = (I " ) & J is one-to-one onto & J is isometric by A1, A2, LM020;

      now

        let t1 be sequence of T;

        assume

         A4: ( rng t1) c= (I .: Z) & t1 is convergent;

        then

         A5: (J * t1) is convergent by P2, LM022;

        

         A6: ( rng (J * t1)) = (J .: ( rng t1)) by RELAT_1: 127;

        (J .: (I .: Z)) = (I " (I .: Z)) by A1, P2, FUNCT_1: 85

        .= Z by FUNCT_1: 94, P1, A1;

        then ( lim (J * t1)) in Z by A3, A4, A5, A6, NFCONT_1:def 3, RELAT_1: 123;

        then (J . ( lim t1)) in Z by A4, P2, LM021;

        then (I . (J . ( lim t1))) in (I .: Z) by FUNCT_2: 35;

        hence ( lim t1) in (I .: Z) by A1, P2, FUNCT_1: 35;

      end;

      hence (I .: Z) is closed by NFCONT_1:def 3;

    end;

    theorem :: NDIFF_7:12

    

     LM024: for I be LinearOperator of S, T, Z be Subset of S st I is one-to-one onto isometric holds (Z is closed iff (I .: Z) is closed)

    proof

      let I be LinearOperator of S, T, Z be Subset of S;

      assume that

       A1: I is one-to-one onto and

       A2: I is isometric;

      

       P1: ( dom I) = the carrier of S by FUNCT_2:def 1;

      consider J be LinearOperator of T, S such that

       P2: J = (I " ) & J is one-to-one onto isometric by A1, A2, LM020;

      thus Z is closed iff (I .: Z) is closed

      proof

        thus Z is closed implies (I .: Z) is closed by A1, A2, LM023;

        assume

         P3: (I .: Z) is closed;

        (J .: (I .: Z)) = (I " (I .: Z)) by A1, P2, FUNCT_1: 85

        .= Z by FUNCT_1: 94, P1, A1;

        hence Z is closed by P2, P3, LM023;

      end;

    end;

    theorem :: NDIFF_7:13

    

     LM025: for I be LinearOperator of S, T, Z be Subset of S st I is one-to-one onto isometric holds (Z is open iff (I .: Z) is open)

    proof

      let I be LinearOperator of S, T, Z be Subset of S;

      assume that

       A1: I is one-to-one onto and

       A2: I is isometric;

      consider J be LinearOperator of T, S such that

       P2: J = (I " ) & J is one-to-one onto isometric by A1, A2, LM020;

      

       Q2: I = (J " ) by P2, A1, FUNCT_1: 43;

      

       Q3: (J " Z) = ((J " ) .: Z) by P2, FUNCT_1: 85

      .= (I .: Z) by A1, P2, FUNCT_1: 43;

      

       A3: (I .: (Z ` )) = (J " (Z ` )) by Q2, P2, FUNCT_1: 85

      .= ((I .: Z) ` ) by Q3, FUNCT_2: 100;

      thus Z is open iff (I .: Z) is open

      proof

        hereby

          assume Z is open;

          then (Z ` ) is closed by NFCONT_1:def 4;

          then ((I .: Z) ` ) is closed by A1, A2, A3, LM024;

          hence (I .: Z) is open by NFCONT_1:def 4;

        end;

        assume (I .: Z) is open;

        then (I .: (Z ` )) is closed by A3, NFCONT_1:def 4;

        then (Z ` ) is closed by A1, A2, LM024;

        hence Z is open by NFCONT_1:def 4;

      end;

    end;

    

     LM026: for I be LinearOperator of S, T, Z be Subset of S st I is isometric & Z is compact holds (I .: Z) is compact

    proof

      let I be LinearOperator of S, T, Z be Subset of S;

      assume

       AS: I is isometric & Z is compact;

      ( dom I) = the carrier of S by FUNCT_2:def 1;

      hence (I .: Z) is compact by AS, LM015, NFCONT_1: 32;

    end;

    theorem :: NDIFF_7:14

    for I be LinearOperator of S, T, Z be Subset of S st I is one-to-one onto isometric holds (Z is compact iff (I .: Z) is compact)

    proof

      let I be LinearOperator of S, T, Z be Subset of S;

      assume that

       A1: I is one-to-one onto and

       A2: I is isometric;

      consider J be LinearOperator of T, S such that

       P2: J = (I " ) & J is one-to-one onto isometric by A1, A2, LM020;

      

       P1: ( dom I) = the carrier of S by FUNCT_2:def 1;

      thus Z is compact implies (I .: Z) is compact by LM026, A2;

      thus (I .: Z) is compact implies Z is compact

      proof

        assume

         X2: (I .: Z) is compact;

        (J .: (I .: Z)) = (I " (I .: Z)) by A1, P2, FUNCT_1: 85

        .= Z by FUNCT_1: 94, P1, A1;

        hence Z is compact by P2, X2, LM026;

      end;

    end;

    theorem :: NDIFF_7:15

    

     LM040: for f be PartFunc of T, W, I be LinearOperator of S, T st I is one-to-one onto isometric holds for x be Point of S st (I . x) in ( dom f) holds (f * I) is_continuous_in x iff f is_continuous_in (I . x)

    proof

      let f be PartFunc of T, W, I be LinearOperator of S, T;

      assume that

       AS2: I is one-to-one onto and

       AS3: I is isometric;

      set g = (f * I);

      let x be Point of S;

      assume

       AS6: (I . x) in ( dom f);

      

       P0: ( dom I) = the carrier of S by FUNCT_2:def 1;

      hereby

        assume

         P1: g is_continuous_in x;

        consider J be LinearOperator of T, S such that

         P2: J = (I " ) & J is one-to-one onto isometric by LM020, AS2, AS3;

        

         Q4: J is_continuous_in (I . x) by LM010, P2;

        

         P3: (J . (I . x)) = x by AS2, P2, P0, FUNCT_1: 34;

        

         Q0: ( dom J) = the carrier of T by FUNCT_2:def 1;

        

         Q1: (J . (I . x)) in ( dom g) by P1, P3, NFCONT_1: 7;

        

         Q3: (g * J) = (f * (I * (I " ))) by P2, RELAT_1: 36

        .= (f * ( id the carrier of T)) by AS2, FUNCT_2: 29

        .= f by FUNCT_2: 17;

        (J . (I . x)) = (J /. (I . x)) & (I . x) = (I /. x);

        hence f is_continuous_in (I . x) by Q3, LM030, P3, P1, Q0, Q1, Q4;

      end;

      assume

       P2: f is_continuous_in (I . x);

      (I . x) = (I /. x);

      hence g is_continuous_in x by P0, AS3, AS6, P2, LM010, LM030;

    end;

    theorem :: NDIFF_7:16

    

     LM045: for f be PartFunc of T, W, I be LinearOperator of S, T, X be set st X c= the carrier of T & I is one-to-one onto isometric holds f is_continuous_on X iff (f * I) is_continuous_on (I " X)

    proof

      let f be PartFunc of T, W, I be LinearOperator of S, T, X be set;

      assume that

       AS1: X c= the carrier of T and

       AS2: I is one-to-one onto and

       AS3: I is isometric;

      hereby

        assume

         P2: f is_continuous_on X;

        then (I " X) c= (I " ( dom f)) by NFCONT_1:def 7, RELAT_1: 143;

        then

         P3: (I " X) c= ( dom (f * I)) by RELAT_1: 147;

        for x be Point of S st x in (I " X) holds ((f * I) | (I " X)) is_continuous_in x

        proof

          let x be Point of S;

          assume x in (I " X);

          then

           P5: x in ( dom I) & (I . x) in X by FUNCT_1:def 7;

          then

           P6: (f | X) is_continuous_in (I . x) by P2, NFCONT_1:def 7;

          X c= ( dom f) & for y be Point of T st y in X holds (f | X) is_continuous_in y by P2, NFCONT_1:def 7;

          then (I . x) in (( dom f) /\ X) by P5, XBOOLE_0:def 4;

          then (I . x) in ( dom (f | X)) by RELAT_1: 61;

          then ((f | X) * I) is_continuous_in x by AS2, AS3, P6, LM040;

          hence ((f * I) | (I " X)) is_continuous_in x by FX1;

        end;

        hence (f * I) is_continuous_on (I " X) by P3, NFCONT_1:def 7;

      end;

      assume

       P2: (f * I) is_continuous_on (I " X);

      then (I " X) c= ( dom (f * I)) & for x be Point of S st x in (I " X) holds ((f * I) | (I " X)) is_continuous_in x by NFCONT_1:def 7;

      then

       K1: (I " X) c= (I " ( dom f)) by RELAT_1: 147;

      

       P3: X c= ( dom f) by AS1, AS2, FUNCT_1: 88, K1;

      for y be Point of T st y in X holds (f | X) is_continuous_in y

      proof

        let y be Point of T;

        assume

         P4: y in X;

        consider x be Point of S such that

         P5: y = (I . x) by AS2, FUNCT_2: 113;

        ( dom I) = the carrier of S by FUNCT_2:def 1;

        then x in (I " X) by P4, P5, FUNCT_1:def 7;

        then ((f * I) | (I " X)) is_continuous_in x by P2, NFCONT_1:def 7;

        then

         P7: ((f | X) * I) is_continuous_in x by FX1;

        (I . x) in ( dom (f | X)) by P3, P4, P5, RELAT_1: 57;

        hence (f | X) is_continuous_in y by AS2, AS3, P5, P7, LM040;

      end;

      hence f is_continuous_on X by AS1, AS2, K1, FUNCT_1: 88, NFCONT_1:def 7;

    end;

    definition

      let X,Y be RealNormSpace;

      :: NDIFF_7:def3

      func IsoCPNrSP (X,Y) -> LinearOperator of [:X, Y:], ( product <*X, Y*>) means

      : defISO: for x be Point of X, y be Point of Y holds (it . (x,y)) = <*x, y*>;

      existence

      proof

        consider I be Function of [:X, Y:], ( product <*X, Y*>) such that I is one-to-one onto and

         A2: for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*> and

         A3: for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w)) and

         A4: for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v)) and ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) and for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.|| by PRVECT_3: 15;

        reconsider I as LinearOperator of [:X, Y:], ( product <*X, Y*>) by A3, A4, VECTSP_1:def 20, LOPBAN_1:def 5;

        take I;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let I1,I2 be LinearOperator of [:X, Y:], ( product <*X, Y*>);

        assume that

         A1: for x be Point of X, y be Point of Y holds (I1 . (x,y)) = <*x, y*> and

         A2: for x be Point of X, y be Point of Y holds (I2 . (x,y)) = <*x, y*>;

        for x,y be set st x in the carrier of X & y in the carrier of Y holds (I1 . (x,y)) = (I2 . (x,y))

        proof

          let x,y be set;

          assume

           P2: x in the carrier of X & y in the carrier of Y;

          then

          reconsider x1 = x as Point of X;

          reconsider y1 = y as Point of Y by P2;

          

          thus (I1 . (x,y)) = <*x1, y1*> by A1

          .= (I2 . (x,y)) by A2;

        end;

        hence I1 = I2 by BINOP_1:def 21;

      end;

    end

    theorem :: NDIFF_7:17

    

     ZeZe: for X,Y be RealNormSpace holds ( 0. ( product <*X, Y*>)) = (( IsoCPNrSP (X,Y)) . ( 0. [:X, Y:]))

    proof

      let X,Y be RealNormSpace;

      consider I be Function of [:X, Y:], ( product <*X, Y*>) such that I is one-to-one onto and

       A2: for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*> and

       A3: for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w)) and

       A4: for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v)) and

       A5: ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) and for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.|| by PRVECT_3: 15;

      reconsider I as LinearOperator of [:X, Y:], ( product <*X, Y*>) by A3, A4, VECTSP_1:def 20, LOPBAN_1:def 5;

      for a be Element of X, b be Element of Y holds (I . (a,b)) = (( IsoCPNrSP (X,Y)) . (a,b)) by defISO, A2;

      hence thesis by A5, BINOP_1: 2;

    end;

    registration

      let X,Y be RealNormSpace;

      cluster ( IsoCPNrSP (X,Y)) -> one-to-one onto isometric;

      correctness

      proof

        consider I be Function of [:X, Y:], ( product <*X, Y*>) such that

         A1: I is one-to-one onto and

         A2: for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*> and

         A3: for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w)) and

         A4: for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v)) and ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) and

         A6: for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.|| by PRVECT_3: 15;

        reconsider I as LinearOperator of [:X, Y:], ( product <*X, Y*>) by A3, A4, VECTSP_1:def 20, LOPBAN_1:def 5;

        for a be Element of X, b be Element of Y holds (I . (a,b)) = (( IsoCPNrSP (X,Y)) . (a,b)) by defISO, A2;

        then I = ( IsoCPNrSP (X,Y)) by BINOP_1: 2;

        hence thesis by A1, A6, LMMAZU;

      end;

    end

    registration

      let X,Y be RealNormSpace;

      cluster one-to-one onto isometric for LinearOperator of [:X, Y:], ( product <*X, Y*>);

      correctness

      proof

        take ( IsoCPNrSP (X,Y));

        thus thesis;

      end;

    end

    definition

      let X,Y be RealNormSpace;

      let f be one-to-one onto isometric LinearOperator of [:X, Y:], ( product <*X, Y*>);

      :: original: "

      redefine

      func f " -> LinearOperator of ( product <*X, Y*>), [:X, Y:] ;

      correctness

      proof

        consider J be LinearOperator of ( product <*X, Y*>), [:X, Y:] such that

         P3: J = (f " ) and J is one-to-one onto isometric by LM020;

        thus thesis by P3;

      end;

    end

    registration

      let X,Y be RealNormSpace;

      let f be one-to-one onto isometric LinearOperator of [:X, Y:], ( product <*X, Y*>);

      cluster (f " ) -> one-to-one onto isometric;

      correctness

      proof

        consider J be LinearOperator of ( product <*X, Y*>), [:X, Y:] such that

         P3: J = (f " ) and

         P4: J is one-to-one onto and

         P5: J is isometric by LM020;

        thus thesis by P3, P4, P5;

      end;

    end

    registration

      let X,Y be RealNormSpace;

      cluster one-to-one onto isometric for LinearOperator of ( product <*X, Y*>), [:X, Y:];

      correctness

      proof

        set J = (( IsoCPNrSP (X,Y)) " );

        take J;

        thus thesis;

      end;

    end

    theorem :: NDIFF_7:18

    

     defISOA1: for X,Y be RealNormSpace, x be Point of X, y be Point of Y holds ((( IsoCPNrSP (X,Y)) " ) . <*x, y*>) = [x, y]

    proof

      let X,Y be RealNormSpace;

      set I = ( IsoCPNrSP (X,Y));

      set J = (I " );

      

       P0: ( dom I) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      for x be Point of X, y be Point of Y holds (J . <*x, y*>) = [x, y]

      proof

        let x be Point of X, y be Point of Y;

        

         Q1: (I . (x,y)) = <*x, y*> by defISO;

        reconsider z = [x, y] as Point of [:X, Y:] by ZFMISC_1:def 2;

        (J . (I . z)) = z by P0, FUNCT_1: 34;

        hence thesis by Q1;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_7:19

    

     defISOA2: for X,Y be RealNormSpace holds ((( IsoCPNrSP (X,Y)) " ) . ( 0. ( product <*X, Y*>))) = ( 0. [:X, Y:])

    proof

      let X,Y be RealNormSpace;

      set I = ( IsoCPNrSP (X,Y));

      set J = (I " );

      

       P0: ( dom I) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      (J . ( 0. ( product <*X, Y*>))) = (J . (I . ( 0. [:X, Y:]))) by ZeZe;

      hence thesis by P0, FUNCT_1: 34;

    end;

    theorem :: NDIFF_7:20

    for X,Y be RealNormSpace, Z be Subset of [:X, Y:] holds ( IsoCPNrSP (X,Y)) is_continuous_on Z by LM015;

    theorem :: NDIFF_7:21

    for X,Y be RealNormSpace, Z be Subset of ( product <*X, Y*>) holds (( IsoCPNrSP (X,Y)) " ) is_continuous_on Z by LM015;

    theorem :: NDIFF_7:22

    

     LMX00: for S,T,W be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (S,W)), g be Point of ( R_NormSpace_of_BoundedLinearOperators (T,W)), I be LinearOperator of S, T st I is one-to-one onto isometric & f = (g * I) holds ||.f.|| = ||.g.||

    proof

      let S,T,W be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (S,W)), g be Point of ( R_NormSpace_of_BoundedLinearOperators (T,W)), I be LinearOperator of S, T;

      assume

       AS: I is one-to-one onto isometric & f = (g * I);

      

       P1: ( dom I) = the carrier of S by FUNCT_2:def 1;

      consider J be LinearOperator of T, S such that

       P2: J = (I " ) & J is one-to-one onto isometric by AS, LM020;

      reconsider f0 = f as Lipschitzian LinearOperator of S, W by LOPBAN_1:def 9;

      reconsider g0 = g as Lipschitzian LinearOperator of T, W by LOPBAN_1:def 9;

      reconsider gI = (g * I) as Lipschitzian LinearOperator of S, W by LOPBAN_1:def 9, AS;

      

       Y1: for x be object holds x in { ||.(g0 . t).|| where t be VECTOR of T : ||.t.|| <= 1 } iff x in { ||.(gI . w).|| where w be VECTOR of S : ||.w.|| <= 1 }

      proof

        let x be object;

        hereby

          assume x in { ||.(g0 . t).|| where t be VECTOR of T : ||.t.|| <= 1 };

          then

          consider t be VECTOR of T such that

           B1: x = ||.(g0 . t).|| & ||.t.|| <= 1;

          set s = (J . t);

          

           B2: (gI . s) = (g0 . (I . (J . t))) by P1, FUNCT_1: 13

          .= (g0 . t) by FUNCT_1: 35, AS, P2;

           ||.s.|| <= 1 by B1, P2, LMMAZU;

          hence x in { ||.(gI . w).|| where w be VECTOR of S : ||.w.|| <= 1 } by B1, B2;

        end;

        assume x in { ||.(gI . w).|| where w be VECTOR of S : ||.w.|| <= 1 };

        then

        consider w be VECTOR of S such that

         B1: x = ||.(gI . w).|| & ||.w.|| <= 1;

        set t = (I . w);

        

         B2: (gI . w) = (g0 . t) by P1, FUNCT_1: 13;

         ||.t.|| <= 1 by B1, AS, LMMAZU;

        hence x in { ||.(g0 . t).|| where t be VECTOR of T : ||.t.|| <= 1 } by B1, B2;

      end;

      

       X0: ( PreNorms f0) = ( PreNorms g0) by AS, Y1, TARSKI: 2;

      

       X1: ( PreNorms ( modetrans (f,S,W))) = ( PreNorms f0) by LOPBAN_1: 29

      .= ( PreNorms ( modetrans (g,T,W))) by X0, LOPBAN_1: 29;

      

      thus ||.f.|| = ( upper_bound ( PreNorms ( modetrans (f,S,W)))) by LOPBAN_1:def 13

      .= ||.g.|| by X1, LOPBAN_1:def 13;

    end;

    registration

      let S, T;

      cluster isometric -> Lipschitzian for LinearOperator of S, T;

      coherence

      proof

        let g be LinearOperator of S, T;

        assume

         A1: g is isometric;

        reconsider K = 1 as Real;

        for x be VECTOR of S holds ||.(g . x).|| <= (K * ||.x.||) by A1, LMMAZU;

        hence thesis;

      end;

    end

    begin

    theorem :: NDIFF_7:23

    for G be RealNormSpace-Sequence, F be RealNormSpace, i be set, f,g be PartFunc of ( product G), F, X be Subset of ( product G) st X is open & i in ( dom G) & f is_partial_differentiable_on (X,i) & g is_partial_differentiable_on (X,i) holds (f + g) is_partial_differentiable_on (X,i) & ((f + g) `partial| (X,i)) = ((f `partial| (X,i)) + (g `partial| (X,i)))

    proof

      let G be RealNormSpace-Sequence;

      let F be RealNormSpace;

      let i be set;

      let f,g be PartFunc of ( product G), F;

      let X be Subset of ( product G);

      assume that

       O1: X is open and

       A0: i in ( dom G) and

       A1: f is_partial_differentiable_on (X,i) and

       A2: g is_partial_differentiable_on (X,i);

      set h = (f + g);

      ( dom h) = (( dom f) /\ ( dom g)) by VFUNCT_1:def 1;

      then

       D1: X c= ( dom h) by A1, A2, XBOOLE_1: 19;

      

       X1: for x be Point of ( product G) st x in X holds h is_partial_differentiable_in (x,i) & ( partdiff (h,x,i)) = (( partdiff (f,x,i)) + ( partdiff (g,x,i)))

      proof

        let x be Point of ( product G);

        assume

         P5: x in X;

        then

         P6: f is_partial_differentiable_in (x,i) by A1, O1, NDIFF_5: 24;

        g is_partial_differentiable_in (x,i) by A2, O1, P5, NDIFF_5: 24;

        hence h is_partial_differentiable_in (x,i) & ( partdiff (h,x,i)) = (( partdiff (f,x,i)) + ( partdiff (g,x,i))) by A0, NDIFF_5: 28, P6;

      end;

      then for x be Point of ( product G) st x in X holds h is_partial_differentiable_in (x,i);

      hence

       P7: h is_partial_differentiable_on (X,i) by NDIFF_5: 24, D1, O1;

      set fp = (f `partial| (X,i));

      set gp = (g `partial| (X,i));

      

       P8: ( dom fp) = X & for x be Point of ( product G) st x in X holds (fp /. x) = ( partdiff (f,x,i)) by A1, NDIFF_5:def 9;

      

       P9: ( dom gp) = X & for x be Point of ( product G) st x in X holds (gp /. x) = ( partdiff (g,x,i)) by A2, NDIFF_5:def 9;

      

       P10: ( dom (fp + gp)) = (X /\ X) by P8, P9, VFUNCT_1:def 1

      .= X;

      for x be Point of ( product G) st x in X holds ((fp + gp) /. x) = ( partdiff (h,x,i))

      proof

        let x be Point of ( product G);

        assume

         P11: x in X;

        

         Z1: (fp /. x) = ( partdiff (f,x,i)) by A1, P11, NDIFF_5:def 9;

        

        thus ((fp + gp) /. x) = ((fp /. x) + (gp /. x)) by P11, P10, VFUNCT_1:def 1

        .= (( partdiff (f,x,i)) + ( partdiff (g,x,i))) by Z1, A2, P11, NDIFF_5:def 9

        .= ( partdiff ((f + g),x,i)) by P11, X1;

      end;

      hence thesis by P7, P10, NDIFF_5:def 9;

    end;

    theorem :: NDIFF_7:24

    for G be RealNormSpace-Sequence, F be RealNormSpace, i be set, f,g be PartFunc of ( product G), F, X be Subset of ( product G) st X is open & i in ( dom G) & f is_partial_differentiable_on (X,i) & g is_partial_differentiable_on (X,i) holds (f - g) is_partial_differentiable_on (X,i) & ((f - g) `partial| (X,i)) = ((f `partial| (X,i)) - (g `partial| (X,i)))

    proof

      let G be RealNormSpace-Sequence;

      let F be RealNormSpace;

      let i be set;

      let f,g be PartFunc of ( product G), F;

      let X be Subset of ( product G);

      assume that

       O1: X is open and

       A0: i in ( dom G) and

       A1: f is_partial_differentiable_on (X,i) and

       A2: g is_partial_differentiable_on (X,i);

      set h = (f - g);

      ( dom h) = (( dom f) /\ ( dom g)) by VFUNCT_1:def 2;

      then

       D1: X c= ( dom h) by A1, A2, XBOOLE_1: 19;

      

       X1: for x be Point of ( product G) st x in X holds h is_partial_differentiable_in (x,i) & ( partdiff (h,x,i)) = (( partdiff (f,x,i)) - ( partdiff (g,x,i)))

      proof

        let x be Point of ( product G);

        assume

         P5: x in X;

        then

         P6: f is_partial_differentiable_in (x,i) by A1, O1, NDIFF_5: 24;

        g is_partial_differentiable_in (x,i) by A2, O1, P5, NDIFF_5: 24;

        hence thesis by A0, NDIFF_5: 29, P6;

      end;

      then for x be Point of ( product G) st x in X holds h is_partial_differentiable_in (x,i);

      hence

       P7: h is_partial_differentiable_on (X,i) by NDIFF_5: 24, D1, O1;

      set fp = (f `partial| (X,i));

      set gp = (g `partial| (X,i));

      

       P8: ( dom fp) = X & for x be Point of ( product G) st x in X holds (fp /. x) = ( partdiff (f,x,i)) by A1, NDIFF_5:def 9;

      

       P9: ( dom gp) = X & for x be Point of ( product G) st x in X holds (gp /. x) = ( partdiff (g,x,i)) by A2, NDIFF_5:def 9;

      

       P10: ( dom (fp - gp)) = (X /\ X) by P8, P9, VFUNCT_1:def 2

      .= X;

      for x be Point of ( product G) st x in X holds ((fp - gp) /. x) = ( partdiff (h,x,i))

      proof

        let x be Point of ( product G);

        assume

         P11: x in X;

        

         Z1: (fp /. x) = ( partdiff (f,x,i)) by A1, P11, NDIFF_5:def 9;

        

        thus ((fp - gp) /. x) = ((fp /. x) - (gp /. x)) by P11, P10, VFUNCT_1:def 2

        .= (( partdiff (f,x,i)) - ( partdiff (g,x,i))) by Z1, A2, P11, NDIFF_5:def 9

        .= ( partdiff ((f - g),x,i)) by P11, X1;

      end;

      hence thesis by P7, P10, NDIFF_5:def 9;

    end;

    theorem :: NDIFF_7:25

    for G be RealNormSpace-Sequence, F be RealNormSpace, i be set, f be PartFunc of ( product G), F, r be Real, X be Subset of ( product G) st X is open & i in ( dom G) & f is_partial_differentiable_on (X,i) holds (r (#) f) is_partial_differentiable_on (X,i) & ((r (#) f) `partial| (X,i)) = (r (#) (f `partial| (X,i)))

    proof

      let G be RealNormSpace-Sequence;

      let F be RealNormSpace;

      let i be set;

      let f be PartFunc of ( product G), F;

      let r be Real;

      let X be Subset of ( product G);

      assume that

       O1: X is open and

       A0: i in ( dom G) and

       A1: f is_partial_differentiable_on (X,i);

      set h = (r (#) f);

      

       D1: X c= ( dom h) by A1, VFUNCT_1:def 4;

      

       X1: for x be Point of ( product G) st x in X holds h is_partial_differentiable_in (x,i) & ( partdiff (h,x,i)) = (r * ( partdiff (f,x,i)))

      proof

        let x be Point of ( product G);

        assume x in X;

        then f is_partial_differentiable_in (x,i) by A1, O1, NDIFF_5: 24;

        hence thesis by A0, NDIFF_5: 30;

      end;

      then for x be Point of ( product G) st x in X holds h is_partial_differentiable_in (x,i);

      hence

       P7: h is_partial_differentiable_on (X,i) by NDIFF_5: 24, D1, O1;

      set fp = (f `partial| (X,i));

      

       P8: ( dom fp) = X & for x be Point of ( product G) st x in X holds (fp /. x) = ( partdiff (f,x,i)) by A1, NDIFF_5:def 9;

      

       P10: ( dom (r (#) fp)) = X by P8, VFUNCT_1:def 4;

      for x be Point of ( product G) st x in X holds ((r (#) fp) /. x) = ( partdiff (h,x,i))

      proof

        let x be Point of ( product G);

        assume

         P11: x in X;

        

        thus ((r (#) fp) /. x) = (r * (fp /. x)) by P11, P10, VFUNCT_1:def 4

        .= (r * ( partdiff (f,x,i))) by A1, P11, NDIFF_5:def 9

        .= ( partdiff ((r (#) f),x,i)) by P11, X1;

      end;

      hence (h `partial| (X,i)) = (r (#) fp) by P7, P10, NDIFF_5:def 9;

    end;

    theorem :: NDIFF_7:26

    

     LM090: for S,T be RealNormSpace, L be Lipschitzian LinearOperator of S, T, x0 be Point of S holds L is_differentiable_in x0 & ( diff (L,x0)) = L

    proof

      let S,T be RealNormSpace, L0 be Lipschitzian LinearOperator of S, T, x0 be Point of S;

      the carrier of S c= the carrier of S;

      then

      reconsider Z = the carrier of S as Subset of S;

      reconsider E = {} as Subset of S by XBOOLE_1: 2;

      reconsider L = L0 as Point of ( R_NormSpace_of_BoundedLinearOperators (S,T)) by LOPBAN_1:def 9;

      reconsider R = (the carrier of S --> ( 0. T)) as PartFunc of S, T;

      

       A6: ( dom R) = the carrier of S;

      now

        let h be ( 0. S) -convergent sequence of S;

        assume h is non-zero;

         A7:

        now

          let n be Nat;

          

           A8: (R /. (h . n)) = (R . (h . n)) by A6, PARTFUN1:def 6

          .= ( 0. T);

          

           A9: ( rng h) c= ( dom R);

          

           A10: n in NAT by ORDINAL1:def 12;

          

          thus ((( ||.h.|| " ) (#) (R /* h)) . n) = ((( ||.h.|| " ) . n) * ((R /* h) . n)) by NDIFF_1:def 2

          .= ( 0. T) by A8, A9, A10, FUNCT_2: 109, RLVECT_1: 10;

        end;

        then

         A11: (( ||.h.|| " ) (#) (R /* h)) is constant by VALUED_0:def 18;

        hence (( ||.h.|| " ) (#) (R /* h)) is convergent by NDIFF_1: 18;

        ((( ||.h.|| " ) (#) (R /* h)) . 0 ) = ( 0. T) by A7;

        hence ( lim (( ||.h.|| " ) (#) (R /* h))) = ( 0. T) by A11, NDIFF_1: 18;

      end;

      then

      reconsider R as RestFunc of S, T by NDIFF_1:def 5;

      set N = the Neighbourhood of x0;

      

       A15: for x be Point of S st x in N holds ((L0 /. x) - (L0 /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

      proof

        let x be Point of S;

        

         A16: (R /. (x - x0)) = (R . (x - x0)) by A6, PARTFUN1:def 6

        .= ( 0. T);

        assume x in N;

        

        thus ((L0 /. x) - (L0 /. x0)) = (L . (x - x0)) by LM001

        .= ((L . (x - x0)) + (R /. (x - x0))) by A16, RLVECT_1: 4;

      end;

      

       A17: ( dom L0) = the carrier of S by FUNCT_2:def 1;

      hence L0 is_differentiable_in x0 by A15;

      hence thesis by A17, A15, NDIFF_1:def 7;

    end;

    theorem :: NDIFF_7:27

    

     LM120: for f be PartFunc of T, W, I be Lipschitzian LinearOperator of S, T, I0 be Point of ( R_NormSpace_of_BoundedLinearOperators (S,T)) st I0 = I holds for x be Point of S st f is_differentiable_in (I . x) holds (f * I) is_differentiable_in x & ( diff ((f * I),x)) = (( diff (f,(I . x))) * I0)

    proof

      let f be PartFunc of T, W, I be Lipschitzian LinearOperator of S, T, I0 be Point of ( R_NormSpace_of_BoundedLinearOperators (S,T));

      assume

       AS0: I0 = I;

      let x be Point of S;

      assume

       AS4: f is_differentiable_in (I . x);

      

       X1: I is_differentiable_in x & ( diff (I,x)) = I by LM090;

      thus (f * I) is_differentiable_in x by X1, AS4, NDIFF_2: 13;

      thus thesis by AS0, AS4, X1, NDIFF_2: 13;

    end;

    theorem :: NDIFF_7:28

    

     LM150: for f be PartFunc of T, W, I be LinearOperator of S, T st I is one-to-one onto & I is isometric holds for x be Point of S holds (f * I) is_differentiable_in x iff f is_differentiable_in (I . x)

    proof

      let f be PartFunc of T, W, I be LinearOperator of S, T;

      assume that

       AS2: I is one-to-one onto and

       AS3: I is isometric;

      

       P0: ( dom I) = the carrier of S by FUNCT_2:def 1;

      set g = (f * I);

      let x be Point of S;

      hereby

        assume

         P1: g is_differentiable_in x;

        consider J be LinearOperator of T, S such that

         P2: J = (I " ) & J is one-to-one onto isometric by LM020, AS2, AS3;

        

         Q4: J is_differentiable_in (I . x) by LM090, P2;

        

         P3: (J . (I . x)) = x by AS2, P2, P0, FUNCT_1: 34;

        (g * J) = (f * (I * (I " ))) by P2, RELAT_1: 36

        .= (f * ( id the carrier of T)) by AS2, FUNCT_2: 29

        .= f by FUNCT_2: 17;

        hence f is_differentiable_in (I . x) by NDIFF_2: 13, P3, P1, Q4;

      end;

      assume

       P2: f is_differentiable_in (I . x);

      I is Lipschitzian LinearOperator of S, T by AS3;

      then

      reconsider I0 = I as Point of ( R_NormSpace_of_BoundedLinearOperators (S,T)) by LOPBAN_1:def 9;

      I0 = I;

      hence thesis by P2, LM120, AS3;

    end;

    theorem :: NDIFF_7:29

    

     LM155: for f be PartFunc of T, W, I be LinearOperator of S, T, X be set st X c= the carrier of T & I is one-to-one onto & I is isometric holds f is_differentiable_on X iff (f * I) is_differentiable_on (I " X)

    proof

      let f be PartFunc of T, W, I be LinearOperator of S, T, X be set;

      assume that

       AS1: X c= the carrier of T and

       AS2: I is one-to-one onto and

       AS3: I is isometric;

      hereby

        assume

         P2: f is_differentiable_on X;

        

         P3: (I " X) c= (I " ( dom f)) by P2, RELAT_1: 143;

        for x be Point of S st x in (I " X) holds ((f * I) | (I " X)) is_differentiable_in x

        proof

          let x be Point of S;

          assume x in (I " X);

          then x in ( dom I) & (I . x) in X by FUNCT_1:def 7;

          then

           P6: (f | X) is_differentiable_in (I . x) by P2;

          ((f | X) * I) is_differentiable_in x by AS2, AS3, P6, LM150;

          hence ((f * I) | (I " X)) is_differentiable_in x by FX1;

        end;

        hence (f * I) is_differentiable_on (I " X) by P3, RELAT_1: 147;

      end;

      assume

       P2: (f * I) is_differentiable_on (I " X);

      then

       K1: (I " X) c= (I " ( dom f)) by RELAT_1: 147;

      for y be Point of T st y in X holds (f | X) is_differentiable_in y

      proof

        let y be Point of T;

        assume

         P4: y in X;

        consider x be Point of S such that

         P5: y = (I . x) by AS2, FUNCT_2: 113;

        ( dom I) = the carrier of S by FUNCT_2:def 1;

        then x in (I " X) by P4, P5, FUNCT_1:def 7;

        then ((f * I) | (I " X)) is_differentiable_in x by P2;

        then ((f | X) * I) is_differentiable_in x by FX1;

        hence (f | X) is_differentiable_in y by AS2, AS3, P5, LM150;

      end;

      hence thesis by AS1, AS2, K1, FUNCT_1: 88;

    end;

    theorem :: NDIFF_7:30

    for X,Y be RealNormSpace, f be PartFunc of ( product <*X, Y*>), W, D be Subset of ( product <*X, Y*>) st f is_differentiable_on D holds for z be Point of ( product <*X, Y*>) st z in ( dom (f `| D)) holds ((f `| D) . z) = ((((f * ( IsoCPNrSP (X,Y))) `| (( IsoCPNrSP (X,Y)) " D)) /. ((( IsoCPNrSP (X,Y)) " ) . z)) * (( IsoCPNrSP (X,Y)) " ))

    proof

      let X,Y be RealNormSpace, f be PartFunc of ( product <*X, Y*>), W, D be Subset of ( product <*X, Y*>);

      assume

       AS2: f is_differentiable_on D;

      then

       OP1: D is open by NDIFF_1: 32;

      set I = ( IsoCPNrSP (X,Y));

      

       X1: I is one-to-one onto & (for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*>) & ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) & I is isometric by defISO, ZeZe;

      set J = (( IsoCPNrSP (X,Y)) " );

      

       P1: ( dom (f `| D)) = D & for x be Point of ( product <*X, Y*>) st x in D holds ((f `| D) /. x) = ( diff (f,x)) by NDIFF_1:def 9, AS2;

      set g = (f * I);

      set E = (I " D);

      

       P3: g is_differentiable_on E by LM155, AS2;

      for z be Point of ( product <*X, Y*>) st z in ( dom (f `| D)) holds ((f `| D) . z) = (((g `| E) /. (J . z)) * (I " ))

      proof

        let z be Point of ( product <*X, Y*>);

        assume

         F1: z in ( dom (f `| D));

        

        then

         F2: ((f `| D) . z) = ((f `| D) /. z) by PARTFUN1:def 6

        .= ( diff (f,z)) by F1, P1;

        

         F3: f is_differentiable_in z by F1, OP1, P1, AS2, NDIFF_1: 31;

        consider w be Point of [:X, Y:] such that

         F4: z = (( IsoCPNrSP (X,Y)) . w) by X1, FUNCT_2: 113;

        reconsider I0 = I as Point of ( R_NormSpace_of_BoundedLinearOperators ( [:X, Y:],( product <*X, Y*>))) by LOPBAN_1:def 9;

        

         F11: ((( diff (f,z)) * I0) * (I0 " )) = (( modetrans (( diff (f,z)),( product <*X, Y*>),W)) * (( modetrans (I0, [:X, Y:],( product <*X, Y*>))) * (I0 " ))) by RELAT_1: 36

        .= (( modetrans (( diff (f,z)),( product <*X, Y*>),W)) * (I * (I " ))) by LOPBAN_1:def 11

        .= (( modetrans (( diff (f,z)),( product <*X, Y*>),W)) * ( id ( rng I0))) by FUNCT_1: 39

        .= ( modetrans (( diff (f,z)),( product <*X, Y*>),W)) by X1, FUNCT_2: 17

        .= ((f `| D) . z) by F2, LOPBAN_1:def 11;

        w in E by F1, F4, P1, FUNCT_2: 38;

        then

         F12: (((g `| E) /. w) * (I0 " )) = (( diff (g,w)) * (I0 " )) by P3, NDIFF_1:def 9;

        

         F13: w = (J . z) by F4, FUNCT_2: 26;

        thus ((f `| D) . z) = (((g `| E) /. (J . z)) * (I " )) by F3, F4, F11, F12, F13, LM120;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_7:31

    

     LM166: for X,Y be RealNormSpace, f be PartFunc of [:X, Y:], W, D be Subset of [:X, Y:] st f is_differentiable_on D holds for z be Point of [:X, Y:] st z in ( dom (f `| D)) holds ((f `| D) . z) = ((((f * (( IsoCPNrSP (X,Y)) " )) `| ((( IsoCPNrSP (X,Y)) " ) " D)) /. (( IsoCPNrSP (X,Y)) . z)) * ((( IsoCPNrSP (X,Y)) " ) " ))

    proof

      let X,Y be RealNormSpace, f be PartFunc of [:X, Y:], W, D be Subset of [:X, Y:];

      assume

       AS2: f is_differentiable_on D;

      then

       OP1: D is open by NDIFF_1: 32;

      set I = (( IsoCPNrSP (X,Y)) " );

      

       X1: I = (( IsoCPNrSP (X,Y)) " ) & I is one-to-one onto & (for x be Point of X, y be Point of Y holds (I . <*x, y*>) = [x, y]) & ( 0. [:X, Y:]) = (I . ( 0. ( product <*X, Y*>))) & I is isometric by defISOA1, defISOA2;

      set J = ( IsoCPNrSP (X,Y));

      

       X2: J is one-to-one onto & (for x be Point of X, y be Point of Y holds (J . (x,y)) = <*x, y*>) & ( 0. ( product <*X, Y*>)) = (J . ( 0. [:X, Y:])) & J is isometric by defISO, ZeZe;

      

       P1: ( dom (f `| D)) = D & for x be Point of [:X, Y:] st x in D holds ((f `| D) /. x) = ( diff (f,x)) by NDIFF_1:def 9, AS2;

      set g = (f * I);

      set E = (I " D);

      

       P3: g is_differentiable_on E by LM155, AS2;

      for z be Point of [:X, Y:] st z in ( dom (f `| D)) holds ((f `| D) . z) = (((g `| E) /. (J . z)) * (I " ))

      proof

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

        assume

         F1X: z in ( dom (f `| D));

        then

         F1: z in D by AS2, NDIFF_1:def 9;

        

         F2: ((f `| D) . z) = ((f `| D) /. z) by F1X, PARTFUN1:def 6

        .= ( diff (f,z)) by F1X, P1;

        

         F3: f is_differentiable_in z by F1, OP1, AS2, NDIFF_1: 31;

        consider w be Point of ( product <*X, Y*>) such that

         F4: z = ((( IsoCPNrSP (X,Y)) " ) . w) by X1, FUNCT_2: 113;

        reconsider I0 = I as Point of ( R_NormSpace_of_BoundedLinearOperators (( product <*X, Y*>), [:X, Y:])) by LOPBAN_1:def 9;

        

         F9: ((( diff (f,z)) * I0) * (I0 " )) = (( diff (g,w)) * (I0 " )) by F3, F4, LM120;

        

         F11: ((( diff (f,z)) * I0) * (I0 " )) = (( modetrans (( diff (f,z)), [:X, Y:],W)) * (( modetrans (I0,( product <*X, Y*>), [:X, Y:])) * (I0 " ))) by RELAT_1: 36

        .= (( modetrans (( diff (f,z)), [:X, Y:],W)) * (I * (I " ))) by LOPBAN_1:def 11

        .= (( modetrans (( diff (f,z)), [:X, Y:],W)) * ( id ( rng I0))) by FUNCT_1: 39

        .= ( modetrans (( diff (f,z)), [:X, Y:],W)) by X1, FUNCT_2: 17

        .= ((f `| D) . z) by F2, LOPBAN_1:def 11;

        w in E by F4, F1, FUNCT_2: 38;

        then (((g `| E) /. w) * (I0 " )) = (( diff (g,w)) * (I0 " )) by P3, NDIFF_1:def 9;

        hence thesis by F4, F9, F11, X2, FUNCT_1: 35;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_7:32

    

     LM180: for X,Y be RealNormSpace, z be Point of [:X, Y:] holds ( reproj1 z) = ((( IsoCPNrSP (X,Y)) " ) * ( reproj (( In (1,( dom <*X, Y*>))),(( IsoCPNrSP (X,Y)) . z)))) & ( reproj2 z) = ((( IsoCPNrSP (X,Y)) " ) * ( reproj (( In (2,( dom <*X, Y*>))),(( IsoCPNrSP (X,Y)) . z))))

    proof

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

      set i1 = ( In (1,( dom <*X, Y*>)));

      set i2 = ( In (2,( dom <*X, Y*>)));

      

       D1: ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      then 1 in ( dom <*X, Y*>);

      then

       AS1: i1 = 1 by SUBSET_1:def 8;

      2 in ( dom <*X, Y*>) by D1;

      then

       AS2: i2 = 2 by SUBSET_1:def 8;

      set I = (( IsoCPNrSP (X,Y)) " );

      set J = ( IsoCPNrSP (X,Y));

      set f1 = ( reproj1 z);

      ( <*X, Y*> . i1) = X by AS1, FINSEQ_1: 44;

      then

      reconsider R = ( reproj (i1,(( IsoCPNrSP (X,Y)) . z))) as Function of X, ( product <*X, Y*>);

      reconsider g1 = ((( IsoCPNrSP (X,Y)) " ) * R) as Function of X, [:X, Y:];

      consider x be Point of X, y be Point of Y such that

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

      

       P3: (z `2 ) = y by P1;

      

       P4: (( IsoCPNrSP (X,Y)) . z) = (( IsoCPNrSP (X,Y)) . (x,y)) by P1

      .= <*x, y*> by defISO;

      now

        let r be Element of X;

        reconsider r0 = r as Element of ( <*X, Y*> . i1) by AS1, FINSEQ_1: 44;

        i1 in ( Seg 2) by AS1;

        then i1 in ( Seg ( len <*x, y*>)) by FINSEQ_1: 44;

        then

         X0: i1 in ( dom <*x, y*>) by FINSEQ_1:def 3;

        

         X1: (R . r) = ( <*x, y*> +* (i1,r0)) by P4, NDIFF_5:def 4;

        

         X3: ( <*x, y*> +* (i1,r0)) = ( <*x, y*> +* (i1 .--> r0)) by FUNCT_7:def 3, X0;

        

         X2: ( <*x, y*> +* (i1 .--> r0)) = <*r, y*>

        proof

          set q = ( <*x, y*> +* (1 .--> r0));

          

           X5: q = ( <*x, y*> +* (1,r0)) by AS1, X0, FUNCT_7:def 3;

          then

          reconsider q as FinSequence;

          

           K1: ( len q) = ( len <*x, y*>) by X5, FUNCT_7: 97

          .= 2 by FINSEQ_1: 44;

          1 in ( dom (1 .--> r0)) by FUNCOP_1: 74;

          

          then

           K3: (q . 1) = ((1 .--> r0) . 1) by FUNCT_4: 13

          .= r by FUNCOP_1: 72;

           not 2 in ( dom (1 .--> r0)) by FUNCOP_1: 75;

          

          then (q . 2) = ( <*x, y*> . 2) by FUNCT_4: 11

          .= y by FINSEQ_1: 44;

          hence thesis by AS1, K1, K3, FINSEQ_1: 44;

        end;

        (g1 . r) = (I . (R . r)) by FUNCT_2: 15

        .= [r, y] by X1, X2, X3, defISOA1;

        hence (f1 . r) = (g1 . r) by P3, Defrep1;

      end;

      

      hence f1 = g1

      .= ((( IsoCPNrSP (X,Y)) " ) * ( reproj (i1,(( IsoCPNrSP (X,Y)) . z))));

      set f2 = ( reproj2 z);

      ( <*X, Y*> . i2) = Y by AS2, FINSEQ_1: 44;

      then

      reconsider L = ( reproj (i2,(( IsoCPNrSP (X,Y)) . z))) as Function of Y, ( product <*X, Y*>);

      reconsider g2 = ((( IsoCPNrSP (X,Y)) " ) * L) as Function of Y, [:X, Y:];

      consider x be Point of X, y be Point of Y such that

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

      

       P2: (z `1 ) = x by P1;

      

       P4: (( IsoCPNrSP (X,Y)) . z) = (( IsoCPNrSP (X,Y)) . (x,y)) by P1

      .= <*x, y*> by defISO;

      now

        let r be Element of Y;

        reconsider r0 = r as Element of ( <*X, Y*> . i2) by AS2, FINSEQ_1: 44;

        i2 in ( Seg 2) by AS2;

        then i2 in ( Seg ( len <*x, y*>)) by FINSEQ_1: 44;

        then

         X0: i2 in ( dom <*x, y*>) by FINSEQ_1:def 3;

        

         X1: (L . r) = ( <*x, y*> +* (i2,r0)) by P4, NDIFF_5:def 4;

        

         X3: ( <*x, y*> +* (i2,r0)) = ( <*x, y*> +* (i2 .--> r0)) by FUNCT_7:def 3, X0;

        

         X2: ( <*x, y*> +* (i2 .--> r0)) = <*x, r*>

        proof

          set q = ( <*x, y*> +* (2 .--> r0));

          

           X5: q = ( <*x, y*> +* (2,r0)) by AS2, X0, FUNCT_7:def 3;

          then

          reconsider q as FinSequence;

          

           K1: ( len q) = ( len <*x, y*>) by X5, FUNCT_7: 97

          .= 2 by FINSEQ_1: 44;

          2 in ( dom (2 .--> r0)) by FUNCOP_1: 74;

          

          then

           K3: (q . 2) = ((2 .--> r0) . 2) by FUNCT_4: 13

          .= r by FUNCOP_1: 72;

           not 1 in ( dom (2 .--> r0)) by FUNCOP_1: 75;

          

          then (q . 1) = ( <*x, y*> . 1) by FUNCT_4: 11

          .= x by FINSEQ_1: 44;

          hence thesis by AS2, K1, K3, FINSEQ_1: 44;

        end;

        (g2 . r) = (I . (L . r)) by FUNCT_2: 15

        .= [x, r] by X1, X2, X3, defISOA1;

        hence (f2 . r) = (g2 . r) by P2, Defrep2;

      end;

      

      hence f2 = g2

      .= ((( IsoCPNrSP (X,Y)) " ) * ( reproj (i2,(( IsoCPNrSP (X,Y)) . z))));

    end;

    definition

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

      :: original: `1

      redefine

      func z `1 -> Point of X ;

      correctness

      proof

        consider x be Point of X, y be Point of Y such that

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

        thus thesis by P1;

      end;

      :: original: `2

      redefine

      func z `2 -> Point of Y ;

      correctness

      proof

        consider x be Point of X, y be Point of Y such that

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

        thus thesis by P1;

      end;

    end

    definition

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], f be PartFunc of [:X, Y:], W;

      :: NDIFF_7:def4

      pred f is_partial_differentiable_in`1 z means (f * ( reproj1 z)) is_differentiable_in (z `1 );

      :: NDIFF_7:def5

      pred f is_partial_differentiable_in`2 z means (f * ( reproj2 z)) is_differentiable_in (z `2 );

    end

    theorem :: NDIFF_7:33

    

     LM190: for X,Y be RealNormSpace, z be Point of [:X, Y:] holds (z `1 ) = (( proj ( In (1,( dom <*X, Y*>)))) . (( IsoCPNrSP (X,Y)) . z)) & (z `2 ) = (( proj ( In (2,( dom <*X, Y*>)))) . (( IsoCPNrSP (X,Y)) . z))

    proof

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

      set i1 = ( In (1,( dom <*X, Y*>)));

      set i2 = ( In (2,( dom <*X, Y*>)));

      

       D1: ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      then 1 in ( dom <*X, Y*>);

      then

       AS1: i1 = 1 by SUBSET_1:def 8;

      2 in ( dom <*X, Y*>) by D1;

      then

       AS2: i2 = 2 by SUBSET_1:def 8;

      set G = <*X, Y*>;

      

       AS3: ( product G) = NORMSTR (# ( product ( carr G)), ( zeros G), [:( addop G):], [:( multop G):], ( productnorm G) #) by PRVECT_2: 6;

      consider x be Point of X, y be Point of Y such that

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

      

       P4: (( IsoCPNrSP (X,Y)) . z) = (( IsoCPNrSP (X,Y)) . (x,y)) by P1

      .= <*x, y*> by defISO;

      reconsider w = (( IsoCPNrSP (X,Y)) . z) as Element of ( product ( carr G)) by AS3;

      

       P5: (( proj ( In (1,( dom <*X, Y*>)))) . w) = ( <*x, y*> . 1) by P4, AS1, NDIFF_5:def 3

      .= (z `1 ) by P1, FINSEQ_1: 44;

      (( proj ( In (2,( dom <*X, Y*>)))) . w) = ( <*x, y*> . 2) by P4, AS2, NDIFF_5:def 3

      .= (z `2 ) by P1, FINSEQ_1: 44;

      hence thesis by P5;

    end;

    theorem :: NDIFF_7:34

    

     LM200: for X,Y,W be RealNormSpace, z be Point of [:X, Y:], f be PartFunc of [:X, Y:], W holds (f is_partial_differentiable_in`1 z iff (f * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),1)) & (f is_partial_differentiable_in`2 z iff (f * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),2))

    proof

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], f be PartFunc of [:X, Y:], W;

      reconsider g = (f * (( IsoCPNrSP (X,Y)) " )) as PartFunc of ( product <*X, Y*>), W;

      reconsider w = (( IsoCPNrSP (X,Y)) . z) as Element of ( product <*X, Y*>);

      

       D1: ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      then 1 in ( dom <*X, Y*>);

      then

       AS1: ( In (1,( dom <*X, Y*>))) = 1 by SUBSET_1:def 8;

      2 in ( dom <*X, Y*>) by D1;

      then

       AS2: ( In (2,( dom <*X, Y*>))) = 2 by SUBSET_1:def 8;

      

       X1: (f * ( reproj1 z)) = (f * ((( IsoCPNrSP (X,Y)) " ) * ( reproj (( In (1,( dom <*X, Y*>))),(( IsoCPNrSP (X,Y)) . z))))) by LM180

      .= (g * ( reproj (( In (1,( dom <*X, Y*>))),w))) by RELAT_1: 36;

      

       X3: X = ( <*X, Y*> . ( In (1,( dom <*X, Y*>)))) by AS1, FINSEQ_1: 44;

      

       Y1: (f * ( reproj2 z)) = (f * ((( IsoCPNrSP (X,Y)) " ) * ( reproj (( In (2,( dom <*X, Y*>))),(( IsoCPNrSP (X,Y)) . z))))) by LM180

      .= (g * ( reproj (( In (2,( dom <*X, Y*>))),w))) by RELAT_1: 36;

      

       Y3: Y = ( <*X, Y*> . ( In (2,( dom <*X, Y*>)))) by AS2, FINSEQ_1: 44;

      thus f is_partial_differentiable_in`1 z iff (f * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),1) by X1, X3, LM190;

      thus thesis by Y1, Y3, LM190;

    end;

    definition

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], f be PartFunc of [:X, Y:], W;

      :: NDIFF_7:def6

      func partdiff`1 (f,z) -> Point of ( R_NormSpace_of_BoundedLinearOperators (X,W)) equals ( diff ((f * ( reproj1 z)),(z `1 )));

      coherence ;

      :: NDIFF_7:def7

      func partdiff`2 (f,z) -> Point of ( R_NormSpace_of_BoundedLinearOperators (Y,W)) equals ( diff ((f * ( reproj2 z)),(z `2 )));

      coherence ;

    end

    theorem :: NDIFF_7:35

    

     LM210: for X,Y,W be RealNormSpace, z be Point of [:X, Y:], f be PartFunc of [:X, Y:], W holds ( partdiff`1 (f,z)) = ( partdiff ((f * (( IsoCPNrSP (X,Y)) " )),(( IsoCPNrSP (X,Y)) . z),1)) & ( partdiff`2 (f,z)) = ( partdiff ((f * (( IsoCPNrSP (X,Y)) " )),(( IsoCPNrSP (X,Y)) . z),2))

    proof

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], f be PartFunc of [:X, Y:], W;

      reconsider g = (f * (( IsoCPNrSP (X,Y)) " )) as PartFunc of ( product <*X, Y*>), W;

      reconsider w = (( IsoCPNrSP (X,Y)) . z) as Element of ( product <*X, Y*>);

      

       D1: ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      then 1 in ( dom <*X, Y*>);

      then

       AS1: ( In (1,( dom <*X, Y*>))) = 1 by SUBSET_1:def 8;

      2 in ( dom <*X, Y*>) by D1;

      then

       AS2: ( In (2,( dom <*X, Y*>))) = 2 by SUBSET_1:def 8;

      

       X1: (f * ( reproj1 z)) = (f * ((( IsoCPNrSP (X,Y)) " ) * ( reproj (( In (1,( dom <*X, Y*>))),(( IsoCPNrSP (X,Y)) . z))))) by LM180

      .= (g * ( reproj (( In (1,( dom <*X, Y*>))),w))) by RELAT_1: 36;

      

       X3: X = ( <*X, Y*> . ( In (1,( dom <*X, Y*>)))) by AS1, FINSEQ_1: 44;

      

       Y1: (f * ( reproj2 z)) = (f * ((( IsoCPNrSP (X,Y)) " ) * ( reproj (( In (2,( dom <*X, Y*>))),(( IsoCPNrSP (X,Y)) . z))))) by LM180

      .= (g * ( reproj (( In (2,( dom <*X, Y*>))),w))) by RELAT_1: 36;

      

       Y3: Y = ( <*X, Y*> . ( In (2,( dom <*X, Y*>)))) by AS2, FINSEQ_1: 44;

      thus ( partdiff`1 (f,z)) = ( partdiff ((f * (( IsoCPNrSP (X,Y)) " )),(( IsoCPNrSP (X,Y)) . z),1)) by X1, X3, LM190;

      thus thesis by Y1, Y3, LM190;

    end;

    theorem :: NDIFF_7:36

    

     LM215: for X,Y,W be RealNormSpace, z be Point of [:X, Y:], f1,f2 be PartFunc of [:X, Y:], W st f1 is_partial_differentiable_in`1 z & f2 is_partial_differentiable_in`1 z holds (f1 + f2) is_partial_differentiable_in`1 z & ( partdiff`1 ((f1 + f2),z)) = (( partdiff`1 (f1,z)) + ( partdiff`1 (f2,z))) & (f1 - f2) is_partial_differentiable_in`1 z & ( partdiff`1 ((f1 - f2),z)) = (( partdiff`1 (f1,z)) - ( partdiff`1 (f2,z)))

    proof

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], f1,f2 be PartFunc of [:X, Y:], W;

      assume

       A1: f1 is_partial_differentiable_in`1 z & f2 is_partial_differentiable_in`1 z;

      ((f1 * ( reproj1 z)) + (f2 * ( reproj1 z))) is_differentiable_in (z `1 ) by NDIFF_1: 35, A1;

      hence (f1 + f2) is_partial_differentiable_in`1 z by Th26;

      

      thus ( partdiff`1 ((f1 + f2),z)) = ( diff (((f1 * ( reproj1 z)) + (f2 * ( reproj1 z))),(z `1 ))) by Th26

      .= (( partdiff`1 (f1,z)) + ( partdiff`1 (f2,z))) by NDIFF_1: 35, A1;

      ((f1 * ( reproj1 z)) - (f2 * ( reproj1 z))) is_differentiable_in (z `1 ) by NDIFF_1: 36, A1;

      hence (f1 - f2) is_partial_differentiable_in`1 z by Th26;

      

      thus ( partdiff`1 ((f1 - f2),z)) = ( diff (((f1 * ( reproj1 z)) - (f2 * ( reproj1 z))),(z `1 ))) by Th26

      .= (( partdiff`1 (f1,z)) - ( partdiff`1 (f2,z))) by NDIFF_1: 36, A1;

    end;

    theorem :: NDIFF_7:37

    

     LM216: for X,Y,W be RealNormSpace, z be Point of [:X, Y:], f1,f2 be PartFunc of [:X, Y:], W st f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z holds (f1 + f2) is_partial_differentiable_in`2 z & ( partdiff`2 ((f1 + f2),z)) = (( partdiff`2 (f1,z)) + ( partdiff`2 (f2,z))) & (f1 - f2) is_partial_differentiable_in`2 z & ( partdiff`2 ((f1 - f2),z)) = (( partdiff`2 (f1,z)) - ( partdiff`2 (f2,z)))

    proof

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], f1,f2 be PartFunc of [:X, Y:], W;

      assume

       A1: f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z;

      ((f1 * ( reproj2 z)) + (f2 * ( reproj2 z))) is_differentiable_in (z `2 ) by NDIFF_1: 35, A1;

      hence (f1 + f2) is_partial_differentiable_in`2 z by Th26;

      

      thus ( partdiff`2 ((f1 + f2),z)) = ( diff (((f1 * ( reproj2 z)) + (f2 * ( reproj2 z))),(z `2 ))) by Th26

      .= (( partdiff`2 (f1,z)) + ( partdiff`2 (f2,z))) by NDIFF_1: 35, A1;

      ((f1 * ( reproj2 z)) - (f2 * ( reproj2 z))) is_differentiable_in (z `2 ) by NDIFF_1: 36, A1;

      hence (f1 - f2) is_partial_differentiable_in`2 z by Th26;

      

      thus ( partdiff`2 ((f1 - f2),z)) = ( diff (((f1 * ( reproj2 z)) - (f2 * ( reproj2 z))),(z `2 ))) by Th26

      .= (( partdiff`2 (f1,z)) - ( partdiff`2 (f2,z))) by NDIFF_1: 36, A1;

    end;

    theorem :: NDIFF_7:38

    

     LM217: for X,Y,W be RealNormSpace, z be Point of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W st f is_partial_differentiable_in`1 z holds (r (#) f) is_partial_differentiable_in`1 z & ( partdiff`1 ((r (#) f),z)) = (r * ( partdiff`1 (f,z)))

    proof

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W;

      assume

       A1: f is_partial_differentiable_in`1 z;

      ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      then

       D2: 1 in ( dom <*X, Y*>);

      then ( In (1,( dom <*X, Y*>))) = 1 by SUBSET_1:def 8;

      then

       BX1: ( <*X, Y*> . ( In (1,( dom <*X, Y*>)))) = X by FINSEQ_1: 44;

      

       P1: (f * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),1) by LM200, A1;

      

       P3: ( partdiff`1 ((r (#) f),z)) = ( partdiff (((r (#) f) * (( IsoCPNrSP (X,Y)) " )),(( IsoCPNrSP (X,Y)) . z),1)) by LM210;

      

       P4: ( partdiff`1 (f,z)) = ( partdiff ((f * (( IsoCPNrSP (X,Y)) " )),(( IsoCPNrSP (X,Y)) . z),1)) by LM210;

      

       P6: ((r (#) f) * (( IsoCPNrSP (X,Y)) " )) = (r (#) (f * (( IsoCPNrSP (X,Y)) " ))) by Th27;

      hence (r (#) f) is_partial_differentiable_in`1 z by D2, P1, LM200, NDIFF_5: 30;

      thus thesis by BX1, D2, P1, P3, P4, P6, NDIFF_5: 30;

    end;

    theorem :: NDIFF_7:39

    

     LM218: for X,Y,W be RealNormSpace, z be Point of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W st f is_partial_differentiable_in`2 z holds (r (#) f) is_partial_differentiable_in`2 z & ( partdiff`2 ((r (#) f),z)) = (r * ( partdiff`2 (f,z)))

    proof

      let X,Y,W be RealNormSpace, z be Point of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W;

      assume

       A1: f is_partial_differentiable_in`2 z;

      

       D1: ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      

       D3: 2 in ( dom <*X, Y*>) by D1;

      then ( In (2,( dom <*X, Y*>))) = 2 by SUBSET_1:def 8;

      then

       BX2: ( <*X, Y*> . ( In (2,( dom <*X, Y*>)))) = Y by FINSEQ_1: 44;

      

       P1: (f * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),2) by LM200, A1;

      

       P3: ( partdiff`2 ((r (#) f),z)) = ( partdiff (((r (#) f) * (( IsoCPNrSP (X,Y)) " )),(( IsoCPNrSP (X,Y)) . z),2)) by LM210;

      

       P4: ( partdiff`2 (f,z)) = ( partdiff ((f * (( IsoCPNrSP (X,Y)) " )),(( IsoCPNrSP (X,Y)) . z),2)) by LM210;

      

       P6: ((r (#) f) * (( IsoCPNrSP (X,Y)) " )) = (r (#) (f * (( IsoCPNrSP (X,Y)) " ))) by Th27;

      (r (#) (f * (( IsoCPNrSP (X,Y)) " ))) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),2) by NDIFF_5: 30, P1, D3;

      then ((r (#) f) * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),2) by Th27;

      hence (r (#) f) is_partial_differentiable_in`2 z by LM200;

      thus thesis by BX2, D3, P1, P3, P4, P6, NDIFF_5: 30;

    end;

    definition

      let X,Y,W be RealNormSpace, Z be set, f be PartFunc of [:X, Y:], W;

      :: NDIFF_7:def8

      pred f is_partial_differentiable_on`1 Z means Z c= ( dom f) & for z be Point of [:X, Y:] st z in Z holds (f | Z) is_partial_differentiable_in`1 z;

      :: NDIFF_7:def9

      pred f is_partial_differentiable_on`2 Z means Z c= ( dom f) & for z be Point of [:X, Y:] st z in Z holds (f | Z) is_partial_differentiable_in`2 z;

    end

    theorem :: NDIFF_7:40

    

     LM300: for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W holds (f is_partial_differentiable_on`1 Z iff (f * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_on (((( IsoCPNrSP (X,Y)) " ) " Z),1)) & (f is_partial_differentiable_on`2 Z iff (f * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_on (((( IsoCPNrSP (X,Y)) " ) " Z),2))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W;

      set I = (( IsoCPNrSP (X,Y)) " );

      set J = ( IsoCPNrSP (X,Y));

      set g = (f * I);

      set E = (I " Z);

      

       X1: I = (( IsoCPNrSP (X,Y)) " ) & I is one-to-one onto & (for x be Point of X, y be Point of Y holds (I . <*x, y*>) = [x, y]) & ( 0. [:X, Y:]) = (I . ( 0. ( product <*X, Y*>))) & I is isometric by defISOA1, defISOA2;

      

       X2: J is one-to-one onto & (for x be Point of X, y be Point of Y holds (J . (x,y)) = <*x, y*>) & ( 0. ( product <*X, Y*>)) = (J . ( 0. [:X, Y:])) & J is isometric by defISO, ZeZe;

      

       A1: ( dom (f * I)) = (I " ( dom f)) by RELAT_1: 147;

      

       A2: ( dom J) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      thus f is_partial_differentiable_on`1 Z iff g is_partial_differentiable_on (E,1)

      proof

        hereby

          assume

           P2: f is_partial_differentiable_on`1 Z;

          for w be Point of ( product <*X, Y*>) st w in E holds (g | E) is_partial_differentiable_in (w,1)

          proof

            let w be Point of ( product <*X, Y*>);

            assume

             A4: w in E;

            consider z be Point of [:X, Y:] such that

             F4: w = (( IsoCPNrSP (X,Y)) . z) by X2, FUNCT_2: 113;

            (I . w) = z by A2, F4, FUNCT_1: 34;

            then z in Z by A4, FUNCT_2: 38;

            then ((f | Z) * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),1) by P2, LM200;

            hence thesis by F4, FX1;

          end;

          hence g is_partial_differentiable_on (E,1) by A1, P2, RELAT_1: 143;

        end;

        assume

         P2: g is_partial_differentiable_on (E,1);

        then

         P3: (I " Z) c= (I " ( dom f)) by RELAT_1: 147;

        for z be Point of [:X, Y:] st z in Z holds (f | Z) is_partial_differentiable_in`1 z

        proof

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

          assume

           A4: z in Z;

          set w = (( IsoCPNrSP (X,Y)) . z);

          (I . w) = z by A2, FUNCT_1: 34;

          then

           F4: w in E by FUNCT_2: 38, A4;

          ((f | Z) * I) = (g | E) by FX1;

          hence thesis by F4, P2, LM200;

        end;

        hence f is_partial_differentiable_on`1 Z by P3, X1, FUNCT_1: 88;

      end;

      thus f is_partial_differentiable_on`2 Z iff g is_partial_differentiable_on (E,2)

      proof

        hereby

          assume

           P2: f is_partial_differentiable_on`2 Z;

          for w be Point of ( product <*X, Y*>) st w in E holds (g | E) is_partial_differentiable_in (w,2)

          proof

            let w be Point of ( product <*X, Y*>);

            assume

             A4: w in E;

            consider z be Point of [:X, Y:] such that

             F4: w = (( IsoCPNrSP (X,Y)) . z) by X2, FUNCT_2: 113;

            

             F8: (I . w) = z by A2, F4, FUNCT_1: 34;

            (I . w) in Z by FUNCT_2: 38, A4;

            then ((f | Z) * (( IsoCPNrSP (X,Y)) " )) is_partial_differentiable_in ((( IsoCPNrSP (X,Y)) . z),2) by F8, P2, LM200;

            hence thesis by F4, FX1;

          end;

          hence g is_partial_differentiable_on (E,2) by A1, P2, RELAT_1: 143;

        end;

        assume

         P2: g is_partial_differentiable_on (E,2);

        

         P3: (I " Z) c= (I " ( dom f)) by P2, RELAT_1: 147;

        for z be Point of [:X, Y:] st z in Z holds (f | Z) is_partial_differentiable_in`2 z

        proof

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

          assume

           A4: z in Z;

          set w = (( IsoCPNrSP (X,Y)) . z);

          (I . w) = z by A2, FUNCT_1: 34;

          then

           F4: w in E by FUNCT_2: 38, A4;

          ((f | Z) * I) = (g | E) by FX1;

          hence thesis by F4, P2, LM200;

        end;

        hence f is_partial_differentiable_on`2 Z by P3, X1, FUNCT_1: 88;

      end;

    end;

    definition

      let X,Y,W be RealNormSpace, Z be set, f be PartFunc of [:X, Y:], W;

      assume

       A2: f is_partial_differentiable_on`1 Z;

      :: NDIFF_7:def10

      func f `partial`1| Z -> PartFunc of [:X, Y:], ( R_NormSpace_of_BoundedLinearOperators (X,W)) means

      : Def91: ( dom it ) = Z & for z be Point of [:X, Y:] st z in Z holds (it /. z) = ( partdiff`1 (f,z));

      existence

      proof

        deffunc F( Element of [:X, Y:]) = ( partdiff`1 (f,$1));

        defpred P[ set] means $1 in Z;

        consider F be PartFunc of [:X, Y:], ( R_NormSpace_of_BoundedLinearOperators (X,W)) such that

         A3: (for z be Point of [:X, Y:] holds z in ( dom F) iff P[z]) & for z be Point of [:X, Y:] st z in ( dom F) holds (F . z) = F(z) from SEQ_1:sch 3;

        take F;

        now

          

           A4: Z is Subset of [:X, Y:] by A2, XBOOLE_1: 1;

          let y be object;

          assume y in Z;

          hence y in ( dom F) by A3, A4;

        end;

        then

         A5: Z c= ( dom F);

        ( dom F) c= Z by A3;

        hence ( dom F) = Z by A5, XBOOLE_0:def 10;

        hereby

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

          assume

           A6: x in Z;

          then (F . x) = ( partdiff`1 (f,x)) by A3;

          hence (F /. x) = ( partdiff`1 (f,x)) by A3, A6, PARTFUN1:def 6;

        end;

      end;

      uniqueness

      proof

        let F,H be PartFunc of [:X, Y:], ( R_NormSpace_of_BoundedLinearOperators (X,W));

        assume that

         A7: ( dom F) = Z and

         A8: for x be Point of [:X, Y:] st x in Z holds (F /. x) = ( partdiff`1 (f,x)) and

         A9: ( dom H) = Z and

         A10: for x be Point of [:X, Y:] st x in Z holds (H /. x) = ( partdiff`1 (f,x));

        now

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

          assume

           A11: x in ( dom F);

          then (F /. x) = ( partdiff`1 (f,x)) by A7, A8;

          hence (F /. x) = (H /. x) by A7, A10, A11;

        end;

        hence thesis by A7, A9, PARTFUN2: 1;

      end;

    end

    definition

      let X,Y,W be RealNormSpace, Z be set, f be PartFunc of [:X, Y:], W;

      assume

       A2: f is_partial_differentiable_on`2 Z;

      :: NDIFF_7:def11

      func f `partial`2| Z -> PartFunc of [:X, Y:], ( R_NormSpace_of_BoundedLinearOperators (Y,W)) means

      : Def92: ( dom it ) = Z & for z be Point of [:X, Y:] st z in Z holds (it /. z) = ( partdiff`2 (f,z));

      existence

      proof

        deffunc F( Element of [:X, Y:]) = ( partdiff`2 (f,$1));

        defpred P[ Element of [:X, Y:]] means $1 in Z;

        consider F be PartFunc of [:X, Y:], ( R_NormSpace_of_BoundedLinearOperators (Y,W)) such that

         A3: (for z be Point of [:X, Y:] holds z in ( dom F) iff P[z]) & for z be Point of [:X, Y:] st z in ( dom F) holds (F . z) = F(z) from SEQ_1:sch 3;

        take F;

        now

          

           A4: Z is Subset of [:X, Y:] by A2, XBOOLE_1: 1;

          let y be object;

          assume y in Z;

          hence y in ( dom F) by A3, A4;

        end;

        then

         A5: Z c= ( dom F);

        ( dom F) c= Z by A3;

        hence ( dom F) = Z by A5, XBOOLE_0:def 10;

        hereby

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

          assume

           A6: x in Z;

          then (F . x) = ( partdiff`2 (f,x)) by A3;

          hence (F /. x) = ( partdiff`2 (f,x)) by A3, A6, PARTFUN1:def 6;

        end;

      end;

      uniqueness

      proof

        let F,H be PartFunc of [:X, Y:], ( R_NormSpace_of_BoundedLinearOperators (Y,W));

        assume that

         A7: ( dom F) = Z and

         A8: for x be Point of [:X, Y:] st x in Z holds (F /. x) = ( partdiff`2 (f,x)) and

         A9: ( dom H) = Z and

         A10: for x be Point of [:X, Y:] st x in Z holds (H /. x) = ( partdiff`2 (f,x));

        now

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

          assume

           A11: x in ( dom F);

          then (F /. x) = ( partdiff`2 (f,x)) by A7, A8;

          hence (F /. x) = (H /. x) by A7, A10, A11;

        end;

        hence thesis by A7, A9, PARTFUN2: 1;

      end;

    end

    theorem :: NDIFF_7:41

    

     LM400: for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W st f is_partial_differentiable_on`1 Z holds (f `partial`1| Z) = (((f * (( IsoCPNrSP (X,Y)) " )) `partial| (((( IsoCPNrSP (X,Y)) " ) " Z),1)) * ( IsoCPNrSP (X,Y)))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W;

      assume

       AS0: f is_partial_differentiable_on`1 Z;

      set I = (( IsoCPNrSP (X,Y)) " );

      set J = ( IsoCPNrSP (X,Y));

      set g = (f * I);

      set E = (I " Z);

      

       A2: ( dom J) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      set fpz = (f `partial`1| Z);

      

       P1: ( dom fpz) = Z & for z be Point of [:X, Y:] st z in Z holds (fpz /. z) = ( partdiff`1 (f,z)) by Def91, AS0;

      set gpe = (g `partial| (E,1));

      

       P3X: g is_partial_differentiable_on (E,1) by LM300, AS0;

      then

       P3: ( dom gpe) = E & for x be Point of ( product <*X, Y*>) st x in E holds (gpe /. x) = ( partdiff (g,x,1)) by NDIFF_5:def 9;

      

       P4: ( dom (gpe * J)) = (J " E) by P3, RELAT_1: 147

      .= (J " (J .: Z)) by FUNCT_1: 84

      .= Z by A2, FUNCT_1: 94;

      now

        let x be object;

        assume

         P40: x in ( dom fpz);

        then

        reconsider z = x as Point of [:X, Y:];

        

         P44: (J . z) in (J .: Z) by P1, P40, FUNCT_2: 35;

        (I " ) = J by FUNCT_1: 43;

        then

         P42: (J . z) in E by P44, FUNCT_1: 85;

        

        thus (fpz . x) = (fpz /. z) by PARTFUN1:def 6, P40

        .= ( partdiff`1 (f,z)) by P1, P40

        .= ( partdiff (g,(J . z),1)) by LM210

        .= (gpe /. (J . z)) by P3X, P42, NDIFF_5:def 9

        .= (gpe . (J . z)) by P42, PARTFUN1:def 6, P3

        .= ((gpe * J) . x) by A2, FUNCT_1: 13;

      end;

      hence thesis by P1, P4, FUNCT_1: 2;

    end;

    theorem :: NDIFF_7:42

    

     LM401: for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W st f is_partial_differentiable_on`2 Z holds (f `partial`2| Z) = (((f * (( IsoCPNrSP (X,Y)) " )) `partial| (((( IsoCPNrSP (X,Y)) " ) " Z),2)) * ( IsoCPNrSP (X,Y)))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W;

      assume

       AS0: f is_partial_differentiable_on`2 Z;

      set I = (( IsoCPNrSP (X,Y)) " );

      set J = ( IsoCPNrSP (X,Y));

      set g = (f * I);

      set E = (I " Z);

      

       A2: ( dom J) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      set fpz = (f `partial`2| Z);

      

       P1: ( dom fpz) = Z & for z be Point of [:X, Y:] st z in Z holds (fpz /. z) = ( partdiff`2 (f,z)) by Def92, AS0;

      set gpe = (g `partial| (E,2));

      

       P3X: g is_partial_differentiable_on (E,2) by LM300, AS0;

      then

       P3: ( dom gpe) = E & for x be Point of ( product <*X, Y*>) st x in E holds (gpe /. x) = ( partdiff (g,x,2)) by NDIFF_5:def 9;

      

       P4: ( dom (gpe * J)) = (J " E) by P3, RELAT_1: 147

      .= (J " (J .: Z)) by FUNCT_1: 84

      .= Z by A2, FUNCT_1: 94;

      now

        let x be object;

        assume

         P40: x in ( dom fpz);

        then

        reconsider z = x as Point of [:X, Y:];

        

         P44: (J . z) in (J .: Z) by P1, P40, FUNCT_2: 35;

        (I " ) = J by FUNCT_1: 43;

        then

         P42: (J . z) in E by P44, FUNCT_1: 85;

        

        thus (fpz . x) = (fpz /. z) by PARTFUN1:def 6, P40

        .= ( partdiff`2 (f,z)) by P1, P40

        .= ( partdiff (g,(J . z),2)) by LM210

        .= (gpe /. (J . z)) by P3X, P42, NDIFF_5:def 9

        .= (gpe . (J . z)) by P3, P42, PARTFUN1:def 6

        .= ((gpe * J) . x) by A2, FUNCT_1: 13;

      end;

      hence thesis by P1, P4, FUNCT_1: 2;

    end;

    theorem :: NDIFF_7:43

    

     NDIFF5241: for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W st Z is open holds f is_partial_differentiable_on`1 Z iff Z c= ( dom f) & for x be Point of [:X, Y:] st x in Z holds f is_partial_differentiable_in`1 x

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W;

      assume

       AS: Z is open;

      set I = (( IsoCPNrSP (X,Y)) " );

      set J = ( IsoCPNrSP (X,Y));

      set g = (f * I);

      set E = (I " Z);

      

       X1: I = (( IsoCPNrSP (X,Y)) " ) & I is one-to-one onto & (for x be Point of X, y be Point of Y holds (I . <*x, y*>) = [x, y]) & ( 0. [:X, Y:]) = (I . ( 0. ( product <*X, Y*>))) & I is isometric by defISOA1, defISOA2;

      

       X2: J is one-to-one onto & (for x be Point of X, y be Point of Y holds (J . (x,y)) = <*x, y*>) & ( 0. ( product <*X, Y*>)) = (J . ( 0. [:X, Y:])) & J is isometric by defISO, ZeZe;

      

       A2: ( dom J) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      (I " Z) = (J .: Z) by FUNCT_1: 84;

      then

       OP1: E is open by AS, LM025;

      hereby

        assume f is_partial_differentiable_on`1 Z;

        then

         P2: g is_partial_differentiable_on (E,1) by LM300;

        then (I " Z) c= (I " ( dom f)) by RELAT_1: 147;

        hence Z c= ( dom f) by X1, FUNCT_1: 88;

        thus for x be Point of [:X, Y:] st x in Z holds f is_partial_differentiable_in`1 x

        proof

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

          assume

           A4: z in Z;

          set w = (( IsoCPNrSP (X,Y)) . z);

          (I . w) = z by A2, FUNCT_1: 34;

          then w in E by FUNCT_2: 38, A4;

          then g is_partial_differentiable_in (w,1) by OP1, P2, NDIFF_5: 24;

          hence f is_partial_differentiable_in`1 z by LM200;

        end;

      end;

      assume

       P1: Z c= ( dom f) & for x be Point of [:X, Y:] st x in Z holds f is_partial_differentiable_in`1 x;

      then (I " Z) c= (I " ( dom f)) by RELAT_1: 143;

      then

       P3: E c= ( dom g) by RELAT_1: 147;

      for w be Point of ( product <*X, Y*>) st w in E holds g is_partial_differentiable_in (w,1)

      proof

        let w be Point of ( product <*X, Y*>);

        assume

         A4: w in E;

        consider z be Point of [:X, Y:] such that

         F4: w = (( IsoCPNrSP (X,Y)) . z) by X2, FUNCT_2: 113;

        

         F8: (I . w) = z by A2, F4, FUNCT_1: 34;

        z in Z by A4, F8, FUNCT_2: 38;

        hence g is_partial_differentiable_in (w,1) by F4, P1, LM200;

      end;

      then g is_partial_differentiable_on (E,1) by NDIFF_5: 24, P3, OP1;

      hence f is_partial_differentiable_on`1 Z by LM300;

    end;

    theorem :: NDIFF_7:44

    

     NDIFF5242: for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W st Z is open holds f is_partial_differentiable_on`2 Z iff Z c= ( dom f) & for x be Point of [:X, Y:] st x in Z holds f is_partial_differentiable_in`2 x

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W;

      assume

       AS: Z is open;

      set I = (( IsoCPNrSP (X,Y)) " );

      set J = ( IsoCPNrSP (X,Y));

      set g = (f * I);

      set E = (I " Z);

      

       X1: I = (( IsoCPNrSP (X,Y)) " ) & I is one-to-one onto & (for x be Point of X, y be Point of Y holds (I . <*x, y*>) = [x, y]) & ( 0. [:X, Y:]) = (I . ( 0. ( product <*X, Y*>))) & I is isometric by defISOA1, defISOA2;

      

       X2: J is one-to-one onto & (for x be Point of X, y be Point of Y holds (J . (x,y)) = <*x, y*>) & ( 0. ( product <*X, Y*>)) = (J . ( 0. [:X, Y:])) & J is isometric by defISO, ZeZe;

      

       A2: ( dom J) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      (I " Z) = (J .: Z) by FUNCT_1: 84;

      then

       OP1: E is open by AS, LM025;

      hereby

        assume f is_partial_differentiable_on`2 Z;

        then

         P2: g is_partial_differentiable_on (E,2) by LM300;

        then (I " Z) c= (I " ( dom f)) by RELAT_1: 147;

        hence Z c= ( dom f) by X1, FUNCT_1: 88;

        thus for x be Point of [:X, Y:] st x in Z holds f is_partial_differentiable_in`2 x

        proof

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

          assume

           A4: z in Z;

          set w = (( IsoCPNrSP (X,Y)) . z);

          (I . w) = z by A2, FUNCT_1: 34;

          then w in E by FUNCT_2: 38, A4;

          then g is_partial_differentiable_in (w,2) by OP1, P2, NDIFF_5: 24;

          hence f is_partial_differentiable_in`2 z by LM200;

        end;

      end;

      assume

       P1: Z c= ( dom f) & for x be Point of [:X, Y:] st x in Z holds f is_partial_differentiable_in`2 x;

      then (I " Z) c= (I " ( dom f)) by RELAT_1: 143;

      then

       P3: E c= ( dom g) by RELAT_1: 147;

      for w be Point of ( product <*X, Y*>) st w in E holds g is_partial_differentiable_in (w,2)

      proof

        let w be Point of ( product <*X, Y*>);

        assume

         A4: w in E;

        consider z be Point of [:X, Y:] such that

         F4: w = (( IsoCPNrSP (X,Y)) . z) by X2, FUNCT_2: 113;

        (I . w) = z by A2, F4, FUNCT_1: 34;

        then z in Z by A4, FUNCT_2: 38;

        hence g is_partial_differentiable_in (w,2) by F4, P1, LM200;

      end;

      then g is_partial_differentiable_on (E,2) by NDIFF_5: 24, P3, OP1;

      hence f is_partial_differentiable_on`2 Z by LM300;

    end;

    theorem :: NDIFF_7:45

    for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds (f + g) is_partial_differentiable_on`1 Z & ((f + g) `partial`1| Z) = ((f `partial`1| Z) + (g `partial`1| Z))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W;

      assume that

       O1: Z is open and

       A1: f is_partial_differentiable_on`1 Z and

       A2: g is_partial_differentiable_on`1 Z;

      set h = (f + g);

      ( dom h) = (( dom f) /\ ( dom g)) by VFUNCT_1:def 1;

      then

       D1: Z c= ( dom h) by A1, A2, XBOOLE_1: 19;

      

       X1: for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`1 x & ( partdiff`1 (h,x)) = (( partdiff`1 (f,x)) + ( partdiff`1 (g,x)))

      proof

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

        assume

         P5: x in Z;

        then

         P6: f is_partial_differentiable_in`1 x by A1, O1, NDIFF5241;

        g is_partial_differentiable_in`1 x by A2, O1, P5, NDIFF5241;

        hence h is_partial_differentiable_in`1 x & ( partdiff`1 (h,x)) = (( partdiff`1 (f,x)) + ( partdiff`1 (g,x))) by LM215, P6;

      end;

      then for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`1 x;

      hence

       P7: h is_partial_differentiable_on`1 Z by NDIFF5241, D1, O1;

      set fp = (f `partial`1| Z);

      set gp = (g `partial`1| Z);

      

       P8: ( dom fp) = Z & for x be Point of [:X, Y:] st x in Z holds (fp /. x) = ( partdiff`1 (f,x)) by A1, Def91;

      

       P9: ( dom gp) = Z & for x be Point of [:X, Y:] st x in Z holds (gp /. x) = ( partdiff`1 (g,x)) by A2, Def91;

      

       P10: ( dom (fp + gp)) = (Z /\ Z) by P8, P9, VFUNCT_1:def 1

      .= Z;

      for x be Point of [:X, Y:] st x in Z holds ((fp + gp) /. x) = ( partdiff`1 (h,x))

      proof

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

        assume

         P11: x in Z;

        

         Z1: (fp /. x) = ( partdiff`1 (f,x)) by A1, P11, Def91;

        

         Z2: (gp /. x) = ( partdiff`1 (g,x)) by A2, P11, Def91;

        

        thus ((fp + gp) /. x) = ((fp /. x) + (gp /. x)) by P11, P10, VFUNCT_1:def 1

        .= ( partdiff`1 ((f + g),x)) by P11, X1, Z1, Z2;

      end;

      hence (h `partial`1| Z) = (fp + gp) by P7, P10, Def91;

    end;

    theorem :: NDIFF_7:46

    for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds (f - g) is_partial_differentiable_on`1 Z & ((f - g) `partial`1| Z) = ((f `partial`1| Z) - (g `partial`1| Z))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W;

      assume that

       O1: Z is open and

       A1: f is_partial_differentiable_on`1 Z and

       A2: g is_partial_differentiable_on`1 Z;

      set h = (f - g);

      ( dom h) = (( dom f) /\ ( dom g)) by VFUNCT_1:def 2;

      then

       D1: Z c= ( dom h) by A1, A2, XBOOLE_1: 19;

      

       X1: for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`1 x & ( partdiff`1 (h,x)) = (( partdiff`1 (f,x)) - ( partdiff`1 (g,x)))

      proof

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

        assume

         P5: x in Z;

        then

         P6: f is_partial_differentiable_in`1 x by A1, O1, NDIFF5241;

        g is_partial_differentiable_in`1 x by A2, O1, P5, NDIFF5241;

        hence h is_partial_differentiable_in`1 x & ( partdiff`1 (h,x)) = (( partdiff`1 (f,x)) - ( partdiff`1 (g,x))) by LM215, P6;

      end;

      then for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`1 x;

      hence

       P7: h is_partial_differentiable_on`1 Z by NDIFF5241, D1, O1;

      set fp = (f `partial`1| Z);

      set gp = (g `partial`1| Z);

      

       P8: ( dom fp) = Z & for x be Point of [:X, Y:] st x in Z holds (fp /. x) = ( partdiff`1 (f,x)) by A1, Def91;

      

       P9: ( dom gp) = Z & for x be Point of [:X, Y:] st x in Z holds (gp /. x) = ( partdiff`1 (g,x)) by A2, Def91;

      

       P10: ( dom (fp - gp)) = (Z /\ Z) by P8, P9, VFUNCT_1:def 2

      .= Z;

      for x be Point of [:X, Y:] st x in Z holds ((fp - gp) /. x) = ( partdiff`1 (h,x))

      proof

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

        assume

         P11: x in Z;

        

         Z1: (fp /. x) = ( partdiff`1 (f,x)) by A1, P11, Def91;

        

         Z2: (gp /. x) = ( partdiff`1 (g,x)) by A2, P11, Def91;

        

        thus ((fp - gp) /. x) = ((fp /. x) - (gp /. x)) by P11, P10, VFUNCT_1:def 2

        .= ( partdiff`1 ((f - g),x)) by P11, X1, Z1, Z2;

      end;

      hence (h `partial`1| Z) = (fp - gp) by P7, P10, Def91;

    end;

    theorem :: NDIFF_7:47

    for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds (f + g) is_partial_differentiable_on`2 Z & ((f + g) `partial`2| Z) = ((f `partial`2| Z) + (g `partial`2| Z))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W;

      assume that

       O1: Z is open and

       A1: f is_partial_differentiable_on`2 Z and

       A2: g is_partial_differentiable_on`2 Z;

      set h = (f + g);

      ( dom h) = (( dom f) /\ ( dom g)) by VFUNCT_1:def 1;

      then

       D1: Z c= ( dom h) by A1, A2, XBOOLE_1: 19;

      

       X1: for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`2 x & ( partdiff`2 (h,x)) = (( partdiff`2 (f,x)) + ( partdiff`2 (g,x)))

      proof

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

        assume

         P5: x in Z;

        then

         P6: f is_partial_differentiable_in`2 x by A1, O1, NDIFF5242;

        g is_partial_differentiable_in`2 x by A2, O1, P5, NDIFF5242;

        hence h is_partial_differentiable_in`2 x & ( partdiff`2 (h,x)) = (( partdiff`2 (f,x)) + ( partdiff`2 (g,x))) by LM216, P6;

      end;

      then for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`2 x;

      hence

       P7: h is_partial_differentiable_on`2 Z by NDIFF5242, D1, O1;

      set fp = (f `partial`2| Z);

      set gp = (g `partial`2| Z);

      

       P8: ( dom fp) = Z & for x be Point of [:X, Y:] st x in Z holds (fp /. x) = ( partdiff`2 (f,x)) by A1, Def92;

      

       P9: ( dom gp) = Z & for x be Point of [:X, Y:] st x in Z holds (gp /. x) = ( partdiff`2 (g,x)) by A2, Def92;

      

       P10: ( dom (fp + gp)) = (Z /\ Z) by P8, P9, VFUNCT_1:def 1

      .= Z;

      for x be Point of [:X, Y:] st x in Z holds ((fp + gp) /. x) = ( partdiff`2 (h,x))

      proof

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

        assume

         P11: x in Z;

        then

         Z1: (fp /. x) = ( partdiff`2 (f,x)) by A1, Def92;

        

         Z2: (gp /. x) = ( partdiff`2 (g,x)) by A2, P11, Def92;

        

        thus ((fp + gp) /. x) = ((fp /. x) + (gp /. x)) by P11, P10, VFUNCT_1:def 1

        .= ( partdiff`2 ((f + g),x)) by P11, X1, Z1, Z2;

      end;

      hence (h `partial`2| Z) = (fp + gp) by P7, P10, Def92;

    end;

    theorem :: NDIFF_7:48

    for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds (f - g) is_partial_differentiable_on`2 Z & ((f - g) `partial`2| Z) = ((f `partial`2| Z) - (g `partial`2| Z))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f,g be PartFunc of [:X, Y:], W;

      assume that

       O1: Z is open and

       A1: f is_partial_differentiable_on`2 Z and

       A2: g is_partial_differentiable_on`2 Z;

      set h = (f - g);

      ( dom h) = (( dom f) /\ ( dom g)) by VFUNCT_1:def 2;

      then

       D1: Z c= ( dom h) by A1, A2, XBOOLE_1: 19;

      

       X1: for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`2 x & ( partdiff`2 (h,x)) = (( partdiff`2 (f,x)) - ( partdiff`2 (g,x)))

      proof

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

        assume

         P5: x in Z;

        then

         P6: f is_partial_differentiable_in`2 x by A1, O1, NDIFF5242;

        g is_partial_differentiable_in`2 x by A2, O1, P5, NDIFF5242;

        hence h is_partial_differentiable_in`2 x & ( partdiff`2 (h,x)) = (( partdiff`2 (f,x)) - ( partdiff`2 (g,x))) by LM216, P6;

      end;

      then for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`2 x;

      hence

       P7: h is_partial_differentiable_on`2 Z by NDIFF5242, D1, O1;

      set fp = (f `partial`2| Z);

      set gp = (g `partial`2| Z);

      

       P8: ( dom fp) = Z & for x be Point of [:X, Y:] st x in Z holds (fp /. x) = ( partdiff`2 (f,x)) by A1, Def92;

      ( dom gp) = Z & for x be Point of [:X, Y:] st x in Z holds (gp /. x) = ( partdiff`2 (g,x)) by A2, Def92;

      

      then

       P10: ( dom (fp - gp)) = (Z /\ Z) by P8, VFUNCT_1:def 2

      .= Z;

      for x be Point of [:X, Y:] st x in Z holds ((fp - gp) /. x) = ( partdiff`2 (h,x))

      proof

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

        assume

         P11: x in Z;

        then

         Z1: (fp /. x) = ( partdiff`2 (f,x)) by A1, Def92;

        

         Z2: (gp /. x) = ( partdiff`2 (g,x)) by A2, P11, Def92;

        

        thus ((fp - gp) /. x) = ((fp /. x) - (gp /. x)) by P11, P10, VFUNCT_1:def 2

        .= ( partdiff`2 ((f - g),x)) by P11, X1, Z1, Z2;

      end;

      hence (h `partial`2| Z) = (fp - gp) by P7, P10, Def92;

    end;

    theorem :: NDIFF_7:49

    for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W st Z is open & f is_partial_differentiable_on`1 Z holds (r (#) f) is_partial_differentiable_on`1 Z & ((r (#) f) `partial`1| Z) = (r (#) (f `partial`1| Z))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W;

      assume that

       O1: Z is open and

       A1: f is_partial_differentiable_on`1 Z;

      set h = (r (#) f);

      

       D1: Z c= ( dom h) by A1, VFUNCT_1:def 4;

      

       X1: for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`1 x & ( partdiff`1 (h,x)) = (r * ( partdiff`1 (f,x)))

      proof

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

        assume x in Z;

        then f is_partial_differentiable_in`1 x by A1, O1, NDIFF5241;

        hence h is_partial_differentiable_in`1 x & ( partdiff`1 (h,x)) = (r * ( partdiff`1 (f,x))) by LM217;

      end;

      then for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`1 x;

      hence

       P7: h is_partial_differentiable_on`1 Z by D1, O1, NDIFF5241;

      set fp = (f `partial`1| Z);

      

       P8: ( dom fp) = Z & for x be Point of [:X, Y:] st x in Z holds (fp /. x) = ( partdiff`1 (f,x)) by A1, Def91;

      

       P10: ( dom (r (#) fp)) = Z by P8, VFUNCT_1:def 4;

      for x be Point of [:X, Y:] st x in Z holds ((r (#) fp) /. x) = ( partdiff`1 (h,x))

      proof

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

        assume

         P11: x in Z;

        

         Z1: (fp /. x) = ( partdiff`1 (f,x)) by A1, P11, Def91;

        

        thus ((r (#) fp) /. x) = (r * (fp /. x)) by P11, P10, VFUNCT_1:def 4

        .= ( partdiff`1 ((r (#) f),x)) by P11, X1, Z1;

      end;

      hence (h `partial`1| Z) = (r (#) fp) by P7, P10, Def91;

    end;

    theorem :: NDIFF_7:50

    for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W st Z is open & f is_partial_differentiable_on`2 Z holds (r (#) f) is_partial_differentiable_on`2 Z & ((r (#) f) `partial`2| Z) = (r (#) (f `partial`2| Z))

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], r be Real, f be PartFunc of [:X, Y:], W;

      assume that

       O1: Z is open and

       A1: f is_partial_differentiable_on`2 Z;

      set h = (r (#) f);

      

       D1: Z c= ( dom h) by A1, VFUNCT_1:def 4;

      

       X1: for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`2 x & ( partdiff`2 (h,x)) = (r * ( partdiff`2 (f,x)))

      proof

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

        assume x in Z;

        then f is_partial_differentiable_in`2 x by A1, O1, NDIFF5242;

        hence h is_partial_differentiable_in`2 x & ( partdiff`2 (h,x)) = (r * ( partdiff`2 (f,x))) by LM218;

      end;

      then for x be Point of [:X, Y:] st x in Z holds h is_partial_differentiable_in`2 x;

      hence

       P7: h is_partial_differentiable_on`2 Z by D1, O1, NDIFF5242;

      set fp = (f `partial`2| Z);

      

       P8: ( dom fp) = Z & for x be Point of [:X, Y:] st x in Z holds (fp /. x) = ( partdiff`2 (f,x)) by A1, Def92;

      

       P10: ( dom (r (#) fp)) = Z by P8, VFUNCT_1:def 4;

      for x be Point of [:X, Y:] st x in Z holds ((r (#) fp) /. x) = ( partdiff`2 (h,x))

      proof

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

        assume

         P11: x in Z;

        

         Z1: (fp /. x) = ( partdiff`2 (f,x)) by A1, P11, Def92;

        

        thus ((r (#) fp) /. x) = (r * (fp /. x)) by P11, P10, VFUNCT_1:def 4

        .= ( partdiff`2 ((r (#) f),x)) by P11, X1, Z1;

      end;

      hence (h `partial`2| Z) = (r (#) fp) by P7, P10, Def92;

    end;

    theorem :: NDIFF_7:51

    

     LMX1: for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W st f is_differentiable_on Z holds (f `| Z) is_continuous_on Z iff ((f * (( IsoCPNrSP (X,Y)) " )) `| ((( IsoCPNrSP (X,Y)) " ) " Z)) is_continuous_on ((( IsoCPNrSP (X,Y)) " ) " Z)

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W;

      assume

       AS1: f is_differentiable_on Z;

      set I = (( IsoCPNrSP (X,Y)) " );

      

       X1: I = (( IsoCPNrSP (X,Y)) " ) & I is one-to-one onto & (for x be Point of X, y be Point of Y holds (I . <*x, y*>) = [x, y]) & ( 0. [:X, Y:]) = (I . ( 0. ( product <*X, Y*>))) & I is isometric by defISOA1, defISOA2;

      set J = ( IsoCPNrSP (X,Y));

      

       X2: J is one-to-one onto & (for x be Point of X, y be Point of Y holds (J . (x,y)) = <*x, y*>) & ( 0. ( product <*X, Y*>)) = (J . ( 0. [:X, Y:])) & J is isometric by defISO, ZeZe;

      set g = (f * I);

      set E = (I " Z);

      

       A2: ( dom J) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      

       IJ1: (I " ) = J by FUNCT_1: 43;

      

       AS2: g is_differentiable_on E by LM155, AS1;

      

       P1: ( dom (f `| Z)) = Z by AS1, NDIFF_1:def 9;

      

       P2: ( dom (g `| E)) = E by AS2, NDIFF_1:def 9;

      set F = (f `| Z);

      set G = (g `| E);

      hereby

        assume

         Q2: F is_continuous_on Z;

        for y0 be Point of ( product <*X, Y*>), r be Real st y0 in E & 0 < r holds ex s be Real st 0 < s & for y1 be Point of ( product <*X, Y*>) st y1 in E & ||.(y1 - y0).|| < s holds ||.((G /. y1) - (G /. y0)).|| < r

        proof

          let y0 be Point of ( product <*X, Y*>), r be Real;

          assume

           H1: y0 in E & 0 < r;

          consider x0 be Point of [:X, Y:] such that

           F4: y0 = (J . x0) by X2, FUNCT_2: 113;

          

           F8: (I . y0) = x0 by A2, F4, FUNCT_1: 34;

          then

           F9: x0 in Z by H1, FUNCT_2: 38;

          then

          consider s be Real such that

           F10: 0 < s & for x1 be Point of [:X, Y:] st x1 in Z & ||.(x1 - x0).|| < s holds ||.((F /. x1) - (F /. x0)).|| < r by Q2, H1, NFCONT_1: 19;

          take s;

          thus 0 < s by F10;

          thus for y1 be Point of ( product <*X, Y*>) st y1 in E & ||.(y1 - y0).|| < s holds ||.((G /. y1) - (G /. y0)).|| < r

          proof

            let y1 be Point of ( product <*X, Y*>);

            assume

             H3: y1 in E & ||.(y1 - y0).|| < s;

            consider x1 be Point of [:X, Y:] such that

             G4: y1 = (J . x1) by X2, FUNCT_2: 113;

            

             G8: (I . y1) = x1 by A2, G4, FUNCT_1: 34;

            then

             G9: x1 in Z by H3, FUNCT_2: 38;

             ||.(x1 - x0).|| = ||.(y1 - y0).|| by X1, F8, G8;

            then

             H5: ||.((F /. x1) - (F /. x0)).|| < r by F10, G9, H3;

            

             H7: (F /. x1) = (F . x1) by G9, P1, PARTFUN1:def 6

            .= ((G /. y1) * J) by AS1, G4, G9, P1, IJ1, LM166;

            

             H8: (F /. x0) = (F . x0) by F9, P1, PARTFUN1:def 6

            .= ((G /. y0) * J) by AS1, F4, F9, P1, IJ1, LM166;

            reconsider Gy1y0 = ((G /. y1) - (G /. y0)) as Lipschitzian LinearOperator of ( product <*X, Y*>), W by LOPBAN_1:def 9;

            reconsider Fx1x0 = ((F /. x1) - (F /. x0)) as Lipschitzian LinearOperator of [:X, Y:], W by LOPBAN_1:def 9;

            now

              let t be VECTOR of [:X, Y:];

              

               U2: ((((G /. y1) - (G /. y0)) * J) . t) = (((G /. y1) - (G /. y0)) . (J . t)) by A2, FUNCT_1: 13

              .= (((G /. y1) . (J . t)) - ((G /. y0) . (J . t))) by LOPBAN_1: 40;

              

               U3: ((F /. x1) . t) = ((G /. y1) . (J . t)) by A2, H7, FUNCT_1: 13;

              ((F /. x0) . t) = ((G /. y0) . (J . t)) by A2, H8, FUNCT_1: 13;

              hence ((Gy1y0 * J) . t) = (Fx1x0 . t) by U2, U3, LOPBAN_1: 40;

            end;

            then (Gy1y0 * J) = Fx1x0;

            hence ||.((G /. y1) - (G /. y0)).|| < r by H5, LMX00;

          end;

        end;

        hence G is_continuous_on E by P2, NFCONT_1: 19;

      end;

      assume

       Q2: (g `| E) is_continuous_on E;

      for x0 be Point of [:X, Y:], r be Real st x0 in Z & 0 < r holds ex s be Real st 0 < s & for x1 be Point of [:X, Y:] st x1 in Z & ||.(x1 - x0).|| < s holds ||.((F /. x1) - (F /. x0)).|| < r

      proof

        let x0 be Point of [:X, Y:], r be Real;

        assume

         H1: x0 in Z & 0 < r;

        set y0 = (J . x0);

        (I . y0) = x0 by A2, FUNCT_1: 34;

        then y0 in E by FUNCT_2: 38, H1;

        then

        consider s be Real such that

         F10: 0 < s & for y1 be Point of ( product <*X, Y*>) st y1 in E & ||.(y1 - y0).|| < s holds ||.((G /. y1) - (G /. y0)).|| < r by H1, Q2, NFCONT_1: 19;

        take s;

        thus 0 < s by F10;

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

        assume

         H3: x1 in Z & ||.(x1 - x0).|| < s;

        set y1 = (J . x1);

        (I . y1) = x1 by A2, FUNCT_1: 34;

        then

         G9: y1 in E by FUNCT_2: 38, H3;

         ||.(y1 - y0).|| = ||.(x1 - x0).|| by X2;

        then

         H5: ||.((G /. y1) - (G /. y0)).|| < r by F10, G9, H3;

        

         H7: (F /. x1) = (F . x1) by H3, P1, PARTFUN1:def 6

        .= ((G /. y1) * J) by AS1, H3, IJ1, P1, LM166;

        

         H8: (F /. x0) = (F . x0) by H1, P1, PARTFUN1:def 6

        .= ((G /. y0) * J) by AS1, H1, IJ1, P1, LM166;

        reconsider Gy1y0 = ((G /. y1) - (G /. y0)) as Lipschitzian LinearOperator of ( product <*X, Y*>), W by LOPBAN_1:def 9;

        reconsider Fx1x0 = ((F /. x1) - (F /. x0)) as Lipschitzian LinearOperator of [:X, Y:], W by LOPBAN_1:def 9;

        now

          let t be VECTOR of [:X, Y:];

          

           U2: ((((G /. y1) - (G /. y0)) * J) . t) = (((G /. y1) - (G /. y0)) . (J . t)) by A2, FUNCT_1: 13

          .= (((G /. y1) . (J . t)) - ((G /. y0) . (J . t))) by LOPBAN_1: 40;

          

           U3: ((F /. x1) . t) = ((G /. y1) . (J . t)) by A2, H7, FUNCT_1: 13;

          ((F /. x0) . t) = ((G /. y0) . (J . t)) by A2, H8, FUNCT_1: 13;

          hence ((Gy1y0 * J) . t) = (Fx1x0 . t) by U2, U3, LOPBAN_1: 40;

        end;

        then (Gy1y0 * J) = Fx1x0;

        hence ||.((F /. x1) - (F /. x0)).|| < r by H5, LMX00;

      end;

      hence (f `| Z) is_continuous_on Z by P1, NFCONT_1: 19;

    end;

    theorem :: NDIFF_7:52

    for X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W st Z is open holds (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) iff f is_differentiable_on Z & (f `| Z) is_continuous_on Z

    proof

      let X,Y,W be RealNormSpace, Z be Subset of [:X, Y:], f be PartFunc of [:X, Y:], W;

      assume

       AS: Z is open;

      set I = (( IsoCPNrSP (X,Y)) " );

      set J = ( IsoCPNrSP (X,Y));

      set g = (f * I);

      set E = (I " Z);

      

       X1: I = (( IsoCPNrSP (X,Y)) " ) & I is one-to-one onto & (for x be Point of X, y be Point of Y holds (I . <*x, y*>) = [x, y]) & ( 0. [:X, Y:]) = (I . ( 0. ( product <*X, Y*>))) & I is isometric by defISOA1, defISOA2;

      (I " Z) = (J .: Z) by FUNCT_1: 84;

      then

       OP1: E is open by AS, LM025;

      

       D1: ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      then

       D2: 1 in ( dom <*X, Y*>);

      then ( In (1,( dom <*X, Y*>))) = 1 by SUBSET_1:def 8;

      then

       BX1: ( <*X, Y*> . ( In (1,( dom <*X, Y*>)))) = X by FINSEQ_1: 44;

      

       D3: 2 in ( dom <*X, Y*>) by D1;

      then ( In (2,( dom <*X, Y*>))) = 2 by SUBSET_1:def 8;

      then

       BX2: ( <*X, Y*> . ( In (2,( dom <*X, Y*>)))) = Y by FINSEQ_1: 44;

      

       JE1: (J " E) = ((J " ) .: (I " Z)) by FUNCT_1: 85

      .= Z by X1, FUNCT_1: 77;

      hereby

        assume

         P1: 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;

        

         P2: g is_partial_differentiable_on (E,1) by P1, LM300;

        

         P3: g is_partial_differentiable_on (E,2) by P1, LM300;

        

         P4: (f `partial`1| Z) = ((g `partial| (E,1)) * J) by LM400, P1;

        

         P5: (f `partial`2| Z) = ((g `partial| (E,2)) * J) by LM401, P1;

        for i be set st i in ( dom <*X, Y*>) holds g is_partial_differentiable_on (E,i) & (g `partial| (E,i)) is_continuous_on E

        proof

          let i be set;

          assume

           CX: i in ( dom <*X, Y*>);

          then

           C1: i = 1 or i = 2 by D1, TARSKI:def 2, FINSEQ_1: 2;

          thus g is_partial_differentiable_on (E,i) by CX, D1, P2, P3, TARSKI:def 2, FINSEQ_1: 2;

          thus (g `partial| (E,i)) is_continuous_on E by BX1, BX2, C1, P1, P4, P5, JE1, LM045;

        end;

        then

         GF1: g is_differentiable_on E & (g `| E) is_continuous_on E by NDIFF_5: 57, OP1;

        hence f is_differentiable_on Z by LM155;

        hence (f `| Z) is_continuous_on Z by GF1, LMX1;

      end;

      assume

       X0: f is_differentiable_on Z & (f `| Z) is_continuous_on Z;

      then

       X1: g is_differentiable_on E by LM155;

      

       X3: (g `| E) is_continuous_on E by X0, LMX1;

      

       P2: g is_partial_differentiable_on (E,1) by D2, OP1, X1, X3, NDIFF_5: 57;

      hence f is_partial_differentiable_on`1 Z by LM300;

      

       P3: g is_partial_differentiable_on (E,2) by D3, OP1, X1, X3, NDIFF_5: 57;

      hence f is_partial_differentiable_on`2 Z by LM300;

      

       P6: (g `partial| (E,1)) is_continuous_on E by D2, OP1, X1, X3, NDIFF_5: 57;

      

       P7: (g `partial| (E,2)) is_continuous_on E by D3, OP1, X1, X3, NDIFF_5: 57;

      (f `partial`1| Z) = ((g `partial| (E,1)) * J) by P2, LM300, LM400;

      hence (f `partial`1| Z) is_continuous_on Z by BX1, P6, LM045, JE1;

      (f `partial`2| Z) = ((g `partial| (E,2)) * J) by P3, LM300, LM401;

      hence (f `partial`2| Z) is_continuous_on Z by BX2, P7, LM045, JE1;

    end;