ndiff_6.miz



    begin

    theorem :: NDIFF_6:1

    for D,E,F be non empty set holds ex I be Function of ( Funcs (D,( Funcs (E,F)))), ( Funcs ( [:D, E:],F)) st I is bijective & for f be Function of D, ( Funcs (E,F)), d,e be object st d in D & e in E holds ((I . f) . (d,e)) = ((f . d) . e)

    proof

      let D,E,F be non empty set;

      defpred P[ object, object] means ex f be Function of D, ( Funcs (E,F)), g be Function of [:D, E:], F st $1 = f & $2 = g & for d,e be object st d in D & e in E holds (g . (d,e)) = ((f . d) . e);

      

       A1: for x be object st x in ( Funcs (D,( Funcs (E,F)))) holds ex y be object st y in ( Funcs ( [:D, E:],F)) & P[x, y]

      proof

        let x be object;

        assume x in ( Funcs (D,( Funcs (E,F))));

        then

        consider f be Function such that

         A2: x = f & ( dom f) = D & ( rng f) c= ( Funcs (E,F)) by FUNCT_2:def 2;

        reconsider f as Function of D, ( Funcs (E,F)) by FUNCT_2: 2, A2;

        deffunc F0( object, object) = ((f . $1) . $2);

        

         A3: for x,y be object st x in D & y in E holds F0(x,y) in F

        proof

          let d,e be object;

          assume

           A4: d in D & e in E;

          then (f . d) is Function of E, F by FUNCT_2: 5, FUNCT_2: 66;

          hence thesis by A4, FUNCT_2: 5;

        end;

        consider g be Function of [:D, E:], F such that

         A5: for x,y be object st x in D & y in E holds (g . (x,y)) = F0(x,y) from BINOP_1:sch 2( A3);

        g in ( Funcs ( [:D, E:],F)) by FUNCT_2: 8;

        hence thesis by A2, A5;

      end;

      consider I be Function of ( Funcs (D,( Funcs (E,F)))), ( Funcs ( [:D, E:],F)) such that

       A6: for x be object st x in ( Funcs (D,( Funcs (E,F)))) holds P[x, (I . x)] from FUNCT_2:sch 1( A1);

      

       A7: for f be Function of D, ( Funcs (E,F)), d,e be object st d in D & e in E holds ((I . f) . (d,e)) = ((f . d) . e)

      proof

        let f be Function of D, ( Funcs (E,F)), d,e be object;

        assume

         A8: d in D & e in E;

        f in ( Funcs (D,( Funcs (E,F)))) by FUNCT_2: 8;

        then ex f0 be Function of D, ( Funcs (E,F)), g0 be Function of [:D, E:], F st f = f0 & (I . f) = g0 & for d,e be object st d in D & e in E holds (g0 . (d,e)) = ((f0 . d) . e) by A6;

        hence ((I . f) . (d,e)) = ((f . d) . e) by A8;

      end;

      now

        let z1,z2 be object;

        assume

         A9: z1 in ( Funcs (D,( Funcs (E,F)))) & z2 in ( Funcs (D,( Funcs (E,F)))) & (I . z1) = (I . z2);

        then

        reconsider z1f = z1, z2f = z2 as Function of D, ( Funcs (E,F)) by FUNCT_2: 66;

        now

          let d be object;

          assume

           A10: d in D;

          then

           A11: (z1f . d) is Function of E, F & (z2f . d) is Function of E, F by FUNCT_2: 5, FUNCT_2: 66;

          now

            let e be object;

            assume

             A12: e in E;

            then ((z1f . d) . e) = ((I . z2f) . (d,e)) by A7, A10, A9;

            hence ((z1f . d) . e) = ((z2f . d) . e) by A7, A10, A12;

          end;

          hence (z1f . d) = (z2f . d) by A11, FUNCT_2: 12;

        end;

        hence z1 = z2 by FUNCT_2: 12;

      end;

      then

       A13: I is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in ( Funcs ( [:D, E:],F));

        then

        reconsider wf = w as Function of [:D, E:], F by FUNCT_2: 66;

        defpred P[ object, object] means ex f be Function of E, F st $2 = f & for e be object st e in E holds (f . e) = (wf . ($1,e));

        

         A14: for d be object st d in D holds ex y be object st y in ( Funcs (E,F)) & P[d, y]

        proof

          let d be object;

          assume

           A15: d in D;

          deffunc F0( object) = (wf . (d,$1));

          

           A16: for e be object st e in E holds F0(e) in F

          proof

            let e be object;

            assume e in E;

            then [d, e] in [:D, E:] by A15, ZFMISC_1:def 2;

            hence thesis by FUNCT_2: 5;

          end;

          consider f be Function of E, F such that

           A17: for e be object st e in E holds (f . e) = F0(e) from FUNCT_2:sch 2( A16);

          f in ( Funcs (E,F)) by FUNCT_2: 8;

          hence thesis by A17;

        end;

        consider zf be Function of D, ( Funcs (E,F)) such that

         A18: for d be object st d in D holds P[d, (zf . d)] from FUNCT_2:sch 1( A14);

        

         A19: zf in ( Funcs (D,( Funcs (E,F)))) by FUNCT_2: 8;

         A20:

        now

          let d,e be set;

          assume

           A21: d in D & e in E;

          then

           A22: ((I . zf) . (d,e)) = ((zf . d) . e) by A7;

          ex L be Function of E, F st (zf . d) = L & for e be object st e in E holds (L . e) = (wf . (d,e)) by A18, A21;

          hence ((I . zf) . (d,e)) = (wf . (d,e)) by A22, A21;

        end;

        (I . zf) is Function of [:D, E:], F by A19, FUNCT_2: 5, FUNCT_2: 66;

        then (I . zf) = w by BINOP_1: 1, A20;

        hence w in ( rng I) by A19, FUNCT_2: 112;

      end;

      then ( Funcs ( [:D, E:],F)) c= ( rng I) by TARSKI:def 3;

      then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

      hence thesis by A7, A13;

    end;

    theorem :: NDIFF_6:2

    

     Th2: for D,E,F be non empty set holds ex I be Function of ( Funcs (D,( Funcs (E,F)))), ( Funcs ( [:E, D:],F)) st I is bijective & for f be Function of D, ( Funcs (E,F)), e,d be object st e in E & d in D holds ((I . f) . (e,d)) = ((f . d) . e)

    proof

      let D,E,F be non empty set;

      defpred P[ object, object] means ex f be Function of D, ( Funcs (E,F)), g be Function of [:E, D:], F st $1 = f & $2 = g & for e,d be object st e in E & d in D holds (g . (e,d)) = ((f . d) . e);

      

       A1: for x be object st x in ( Funcs (D,( Funcs (E,F)))) holds ex y be object st y in ( Funcs ( [:E, D:],F)) & P[x, y]

      proof

        let x be object;

        assume x in ( Funcs (D,( Funcs (E,F))));

        then

        consider f be Function such that

         A2: x = f & ( dom f) = D & ( rng f) c= ( Funcs (E,F)) by FUNCT_2:def 2;

        reconsider f as Function of D, ( Funcs (E,F)) by FUNCT_2: 2, A2;

        deffunc F0( object, object) = ((f . $2) . $1);

        

         A3: for y,x be object st y in E & x in D holds F0(y,x) in F

        proof

          let e,d be object;

          assume

           A4: e in E & d in D;

          then (f . d) is Function of E, F by FUNCT_2: 5, FUNCT_2: 66;

          hence F0(e,d) in F by A4, FUNCT_2: 5;

        end;

        consider g be Function of [:E, D:], F such that

         A5: for y,x be object st y in E & x in D holds (g . (y,x)) = F0(y,x) from BINOP_1:sch 2( A3);

        g in ( Funcs ( [:E, D:],F)) by FUNCT_2: 8;

        hence thesis by A2, A5;

      end;

      consider I be Function of ( Funcs (D,( Funcs (E,F)))), ( Funcs ( [:E, D:],F)) such that

       A6: for x be object st x in ( Funcs (D,( Funcs (E,F)))) holds P[x, (I . x)] from FUNCT_2:sch 1( A1);

      

       A7: for f be Function of D, ( Funcs (E,F)), e,d be object st e in E & d in D holds ((I . f) . (e,d)) = ((f . d) . e)

      proof

        let f be Function of D, ( Funcs (E,F)), e,d be object;

        assume

         A8: e in E & d in D;

        f in ( Funcs (D,( Funcs (E,F)))) by FUNCT_2: 8;

        then ex f0 be Function of D, ( Funcs (E,F)), g0 be Function of [:E, D:], F st f = f0 & (I . f) = g0 & for e,d be object st e in E & d in D holds (g0 . (e,d)) = ((f0 . d) . e) by A6;

        hence ((I . f) . (e,d)) = ((f . d) . e) by A8;

      end;

      now

        let z1,z2 be object;

        assume

         A9: z1 in ( Funcs (D,( Funcs (E,F)))) & z2 in ( Funcs (D,( Funcs (E,F)))) & (I . z1) = (I . z2);

        then

        reconsider z1f = z1, z2f = z2 as Function of D, ( Funcs (E,F)) by FUNCT_2: 66;

        now

          let d be object;

          assume

           A10: d in D;

          then

           A11: (z1f . d) is Function of E, F & (z2f . d) is Function of E, F by FUNCT_2: 5, FUNCT_2: 66;

          now

            let e be object;

            assume

             A12: e in E;

            then ((z1f . d) . e) = ((I . z2f) . (e,d)) by A7, A10, A9;

            hence ((z1f . d) . e) = ((z2f . d) . e) by A7, A10, A12;

          end;

          hence (z1f . d) = (z2f . d) by A11, FUNCT_2: 12;

        end;

        hence z1 = z2 by FUNCT_2: 12;

      end;

      then

       A13: I is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in ( Funcs ( [:E, D:],F));

        then

        reconsider wf = w as Function of [:E, D:], F by FUNCT_2: 66;

        defpred P[ object, object] means ex f be Function of E, F st $2 = f & for e be object st e in E holds (f . e) = (wf . (e,$1));

        

         A14: for d be object st d in D holds ex y be object st y in ( Funcs (E,F)) & P[d, y]

        proof

          let d be object;

          assume

           A15: d in D;

          deffunc F0( object) = (wf . ($1,d));

          

           A16: for e be object st e in E holds F0(e) in F

          proof

            let e be object;

            assume e in E;

            then [e, d] in [:E, D:] by A15, ZFMISC_1:def 2;

            hence thesis by FUNCT_2: 5;

          end;

          consider f be Function of E, F such that

           A17: for e be object st e in E holds (f . e) = F0(e) from FUNCT_2:sch 2( A16);

          f in ( Funcs (E,F)) by FUNCT_2: 8;

          hence thesis by A17;

        end;

        consider zf be Function of D, ( Funcs (E,F)) such that

         A18: for d be object st d in D holds P[d, (zf . d)] from FUNCT_2:sch 1( A14);

        

         A19: zf in ( Funcs (D,( Funcs (E,F)))) by FUNCT_2: 8;

         A20:

        now

          let e,d be set;

          assume

           A21: e in E & d in D;

          then

           A22: ((I . zf) . (e,d)) = ((zf . d) . e) by A7;

          ex L be Function of E, F st (zf . d) = L & for e be object st e in E holds (L . e) = (wf . (e,d)) by A18, A21;

          hence ((I . zf) . (e,d)) = (wf . (e,d)) by A22, A21;

        end;

        (I . zf) is Function of [:E, D:], F by A19, FUNCT_2: 5, FUNCT_2: 66;

        then (I . zf) = w by BINOP_1: 1, A20;

        hence w in ( rng I) by A19, FUNCT_2: 112;

      end;

      then ( Funcs ( [:E, D:],F)) c= ( rng I) by TARSKI:def 3;

      then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

      hence thesis by A7, A13;

    end;

    theorem :: NDIFF_6:3

    for D,E be non-empty non empty FinSequence, F be non empty set holds ex L be Function of ( Funcs (( product D),( Funcs (( product E),F)))), ( Funcs (( product (E ^ D)),F)) st L is bijective & for f be Function of ( product D), ( Funcs (( product E),F)), e,d be FinSequence st e in ( product E) & d in ( product D) holds ((L . f) . (e ^ d)) = ((f . d) . e)

    proof

      let D,E be non-empty non empty FinSequence, F be non empty set;

      consider I be Function of ( Funcs (( product D),( Funcs (( product E),F)))), ( Funcs ( [:( product E), ( product D):],F)) such that

       A1: I is bijective & for f be Function of ( product D), ( Funcs (( product E),F)), e,d be object st e in ( product E) & d in ( product D) holds ((I . f) . (e,d)) = ((f . d) . e) by Th2;

      consider J be Function of [:( product E), ( product D):], ( product (E ^ D)) such that

       A2: J is one-to-one onto & for x,y be FinSequence st x in ( product E) & y in ( product D) holds (J . (x,y)) = (x ^ y) by PRVECT_3: 6;

      

       A3: ( rng J) = ( product (E ^ D)) by A2, FUNCT_2:def 3;

      then

      reconsider K = (J " ) as Function of ( product (E ^ D)), [:( product E), ( product D):] by FUNCT_2: 25, A2;

      deffunc F0( object) = ((I . $1) * K);

      

       A4: for x be object st x in ( Funcs (( product D),( Funcs (( product E),F)))) holds F0(x) in ( Funcs (( product (E ^ D)),F))

      proof

        let x be object;

        assume x in ( Funcs (( product D),( Funcs (( product E),F))));

        then

         A5: (I . x) in ( Funcs ( [:( product E), ( product D):],F)) by FUNCT_2: 5;

        K in ( Funcs (( product (E ^ D)), [:( product E), ( product D):])) by FUNCT_2: 8;

        hence thesis by A5, FUNCT_2: 128;

      end;

      consider L be Function of ( Funcs (( product D),( Funcs (( product E),F)))), ( Funcs (( product (E ^ D)),F)) such that

       A6: for e be object st e in ( Funcs (( product D),( Funcs (( product E),F)))) holds (L . e) = F0(e) from FUNCT_2:sch 2( A4);

      

       A7: (K * J) = ( id [:( product E), ( product D):]) by A2, A3, FUNCT_2: 29;

      

       A8: (J * K) = ( id ( product (E ^ D))) by A2, A3, FUNCT_2: 29;

      now

        let z1,z2 be object;

        assume

         A9: z1 in ( Funcs (( product D),( Funcs (( product E),F)))) & z2 in ( Funcs (( product D),( Funcs (( product E),F)))) & (L . z1) = (L . z2);

        ((I . z1) * K) = (L . z2) by A6, A9;

        then

         A10: (((I . z1) * K) * J) = (((I . z2) * K) * J) by A6, A9;

        ((I . z1) * (K * J)) = (((I . z1) * K) * J) by RELAT_1: 36;

        then

         A11: ((I . z1) * (K * J)) = ((I . z2) * (K * J)) by A10, RELAT_1: 36;

        (I . z1) is Function of [:( product E), ( product D):], F & (I . z2) is Function of [:( product E), ( product D):], F by A9, FUNCT_2: 5, FUNCT_2: 66;

        then ((I . z1) * (K * J)) = (I . z1) & ((I . z2) * (K * J)) = (I . z2) by A7, FUNCT_2: 17;

        hence z1 = z2 by A1, FUNCT_2: 19, A9, A11;

      end;

      then

       A12: L is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in ( Funcs (( product (E ^ D)),F));

        then

        reconsider wf = w as Function of ( product (E ^ D)), F by FUNCT_2: 66;

        (wf * J) in ( Funcs ( [:( product E), ( product D):],F)) by FUNCT_2: 8;

        then (wf * J) in ( rng I) by A1, FUNCT_2:def 3;

        then

        consider zf be object such that

         A13: zf in ( Funcs (( product D),( Funcs (( product E),F)))) & (I . zf) = (wf * J) by FUNCT_2: 11;

        (L . zf) = ((wf * J) * K) by A6, A13;

        then (L . zf) = (wf * ( id ( product (E ^ D)))) by A8, RELAT_1: 36;

        then (L . zf) = w by FUNCT_2: 17;

        hence w in ( rng L) by A13, FUNCT_2: 112;

      end;

      then ( Funcs (( product (E ^ D)),F)) c= ( rng L) by TARSKI:def 3;

      then

       A14: L is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

      for f be Function of ( product D), ( Funcs (( product E),F)), e,d be FinSequence st e in ( product E) & d in ( product D) holds ((L . f) . (e ^ d)) = ((f . d) . e)

      proof

        let f be Function of ( product D), ( Funcs (( product E),F)), e,d be FinSequence;

        assume

         A15: e in ( product E) & d in ( product D);

        then

         A16: ((I . f) . (e,d)) = ((f . d) . e) by A1;

        

         A17: (J . (e,d)) = (e ^ d) by A2, A15;

        

         A18: [e, d] in [:( product E), ( product D):] by A15, ZFMISC_1: 87;

        

         A19: (K . (J . (e,d))) = [e, d] by FUNCT_2: 26, A2, A15, ZFMISC_1: 87;

        f in ( Funcs (( product D),( Funcs (( product E),F)))) by FUNCT_2: 8;

        then ((L . f) . (e ^ d)) = (((I . f) * K) . (J . (e,d))) by A17, A6;

        hence ((L . f) . (e ^ d)) = ((f . d) . e) by A16, A19, A18, FUNCT_2: 5, FUNCT_2: 15;

      end;

      hence thesis by A12, A14;

    end;

    theorem :: NDIFF_6:4

    

     Th4: for X,Y be non empty set holds ex I be Function of [:X, Y:], [:X, ( product <*Y*>):] st I is bijective & for x,y be object st x in X & y in Y holds (I . (x,y)) = [x, <*y*>]

    proof

      let X,Y be non empty set;

      consider J be Function of Y, ( product <*Y*>) such that

       A1: J is one-to-one onto & for y be object st y in Y holds (J . y) = <*y*> by PRVECT_3: 4;

      defpred P[ object, object, object] means $3 = [$1, <*$2*>];

      

       A2: for x,y be object st x in X & y in Y holds ex z be object st z in [:X, ( product <*Y*>):] & P[x, y, z]

      proof

        let x,y be object;

        assume

         A3: x in X & y in Y;

        then (J . y) = <*y*> by A1;

        then <*y*> in ( product <*Y*>) by A3, FUNCT_2: 5;

        hence thesis by A3, ZFMISC_1: 87;

      end;

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

       A4: for x,y be object st x in X & y in Y holds P[x, y, (I . (x,y))] from BINOP_1:sch 1( A2);

      reconsider I as Function of [:X, Y:], [:X, ( product <*Y*>):];

      take I;

      now

        let z1,z2 be object;

        assume

         A5: z1 in [:X, Y:] & z2 in [:X, Y:] & (I . z1) = (I . z2);

        then

        consider x1,y1 be object such that

         A6: x1 in X & y1 in Y & z1 = [x1, y1] by ZFMISC_1:def 2;

        consider x2,y2 be object such that

         A7: x2 in X & y2 in Y & z2 = [x2, y2] by A5, ZFMISC_1:def 2;

         [x1, <*y1*>] = (I . (x1,y1)) by A4, A6

        .= (I . (x2,y2)) by A5, A6, A7

        .= [x2, <*y2*>] by A4, A7;

        then x1 = x2 & <*y1*> = <*y2*> by XTUPLE_0: 1;

        hence z1 = z2 by A6, A7, FINSEQ_1: 76;

      end;

      then

       A8: I is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in [:X, ( product <*Y*>):];

        then

        consider x,y1 be object such that

         A9: x in X & y1 in ( product <*Y*>) & w = [x, y1] by ZFMISC_1:def 2;

        y1 in ( rng J) by A1, A9, FUNCT_2:def 3;

        then

        consider y be object such that

         A10: y in Y & y1 = (J . y) by FUNCT_2: 11;

        (J . y) = <*y*> by A10, A1;

        then

         A11: w = (I . (x,y)) by A4, A9, A10;

         [x, y] in [:X, Y:] by A9, A10, ZFMISC_1: 87;

        hence w in ( rng I) by A11, FUNCT_2: 4;

      end;

      then [:X, ( product <*Y*>):] c= ( rng I) by TARSKI:def 3;

      then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

      hence thesis by A4, A8;

    end;

    theorem :: NDIFF_6:5

    

     Th5: for X be non-empty non empty FinSequence, Y be non empty set holds ex K be Function of [:( product X), Y:], ( product (X ^ <*Y*>)) st K is bijective & for x be FinSequence, y be object st x in ( product X) & y in Y holds (K . (x,y)) = (x ^ <*y*>)

    proof

      let X be non-empty non empty FinSequence;

      let Y be non empty set;

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

       A1: I is bijective & for x be object, y be object st x in ( product X) & y in Y holds (I . (x,y)) = [x, <*y*>] by Th4;

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

       A2: J is one-to-one onto & for x,y be FinSequence st x in ( product X) & y in ( product <*Y*>) holds (J . (x,y)) = (x ^ y) by PRVECT_3: 6;

      set K = (J * I);

      reconsider K as Function of [:( product X), Y:], ( product (X ^ <*Y*>));

      take K;

      

       A3: ( rng J) = ( product (X ^ <*Y*>)) by A2, FUNCT_2:def 3;

      ( rng I) = [:( product X), ( product <*Y*>):] by A1, FUNCT_2:def 3;

      

      then ( rng (J * I)) = (J .: [:( product X), ( product <*Y*>):]) by RELAT_1: 127

      .= ( product (X ^ <*Y*>)) by A3, RELSET_1: 22;

      then K is onto by FUNCT_2:def 3;

      hence K is bijective by A1, A2;

      thus for x be FinSequence, y be object st x in ( product X) & y in Y holds (K . (x,y)) = (x ^ <*y*>)

      proof

        let x be FinSequence, y be object;

        assume

         A4: x in ( product X) & y in Y;

        then

         A5: (I . (x,y)) = [x, <*y*>] by A1;

         [x, y] in [:( product X), Y:] by A4, ZFMISC_1: 87;

        then (I . [x, y]) in [:( product X), ( product <*Y*>):] by FUNCT_2: 5;

        then <*y*> in ( product <*Y*>) by A5, ZFMISC_1: 87;

        then (J . (x, <*y*>)) = (x ^ <*y*>) by A4, A2;

        hence thesis by A5, A4, ZFMISC_1: 87, FUNCT_2: 15;

      end;

    end;

    theorem :: NDIFF_6:6

    for D be non empty set, E be non-empty non empty FinSequence, F be non empty set holds ex L be Function of ( Funcs (D,( Funcs (( product E),F)))), ( Funcs (( product (E ^ <*D*>)),F)) st L is bijective & for f be Function of D, ( Funcs (( product E),F)), e be FinSequence, d be object st e in ( product E) & d in D holds ((L . f) . (e ^ <*d*>)) = ((f . d) . e)

    proof

      let D be non empty set, E be non-empty non empty FinSequence, F be non empty set;

      consider I be Function of ( Funcs (D,( Funcs (( product E),F)))), ( Funcs ( [:( product E), D:],F)) such that

       A1: I is bijective & for f be Function of D, ( Funcs (( product E),F)), e,d be object st e in ( product E) & d in D holds ((I . f) . (e,d)) = ((f . d) . e) by Th2;

      consider J be Function of [:( product E), D:], ( product (E ^ <*D*>)) such that

       A2: J is bijective & for x be FinSequence, y be object st x in ( product E) & y in D holds (J . (x,y)) = (x ^ <*y*>) by Th5;

      

       A3: ( rng J) = ( product (E ^ <*D*>)) by A2, FUNCT_2:def 3;

      then

      reconsider K = (J " ) as Function of ( product (E ^ <*D*>)), [:( product E), D:] by FUNCT_2: 25, A2;

      deffunc F0( object) = ((I . $1) * K);

      

       A4: for x be object st x in ( Funcs (D,( Funcs (( product E),F)))) holds F0(x) in ( Funcs (( product (E ^ <*D*>)),F))

      proof

        let x be object;

        assume x in ( Funcs (D,( Funcs (( product E),F))));

        then (I . x) in ( Funcs ( [:( product E), D:],F)) & K in ( Funcs (( product (E ^ <*D*>)), [:( product E), D:])) by FUNCT_2: 5, FUNCT_2: 8;

        hence thesis by FUNCT_2: 128;

      end;

      consider L be Function of ( Funcs (D,( Funcs (( product E),F)))), ( Funcs (( product (E ^ <*D*>)),F)) such that

       A5: for e be object st e in ( Funcs (D,( Funcs (( product E),F)))) holds (L . e) = F0(e) from FUNCT_2:sch 2( A4);

      take L;

      

       A6: (K * J) = ( id [:( product E), D:]) by A2, A3, FUNCT_2: 29;

      

       A7: (J * K) = ( id ( product (E ^ <*D*>))) by A2, A3, FUNCT_2: 29;

      now

        let z1,z2 be object;

        assume

         A8: z1 in ( Funcs (D,( Funcs (( product E),F)))) & z2 in ( Funcs (D,( Funcs (( product E),F)))) & (L . z1) = (L . z2);

        ((I . z1) * K) = (L . z2) by A5, A8;

        then

         A9: (((I . z1) * K) * J) = (((I . z2) * K) * J) by A5, A8;

        ((I . z1) * (K * J)) = (((I . z1) * K) * J) by RELAT_1: 36;

        then

         A10: ((I . z1) * (K * J)) = ((I . z2) * (K * J)) by A9, RELAT_1: 36;

        (I . z1) is Function of [:( product E), D:], F & (I . z2) is Function of [:( product E), D:], F by A8, FUNCT_2: 5, FUNCT_2: 66;

        then ((I . z1) * (K * J)) = (I . z1) & ((I . z2) * (K * J)) = (I . z2) by A6, FUNCT_2: 17;

        hence z1 = z2 by A1, FUNCT_2: 19, A8, A10;

      end;

      then

       A11: L is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in ( Funcs (( product (E ^ <*D*>)),F));

        then

        reconsider wf = w as Function of ( product (E ^ <*D*>)), F by FUNCT_2: 66;

        (wf * J) in ( Funcs ( [:( product E), D:],F)) by FUNCT_2: 8;

        then (wf * J) in ( rng I) by A1, FUNCT_2:def 3;

        then

        consider zf be object such that

         A12: zf in ( Funcs (D,( Funcs (( product E),F)))) & (I . zf) = (wf * J) by FUNCT_2: 11;

        (L . zf) = ((wf * J) * K) by A5, A12;

        then (L . zf) = (wf * ( id ( product (E ^ <*D*>)))) by A7, RELAT_1: 36;

        then (L . zf) = w by FUNCT_2: 17;

        hence w in ( rng L) by A12, FUNCT_2: 112;

      end;

      then ( Funcs (( product (E ^ <*D*>)),F)) c= ( rng L) by TARSKI:def 3;

      then L is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

      hence L is bijective by A11;

      thus for f be Function of D, ( Funcs (( product E),F)), e be FinSequence, d be object st e in ( product E) & d in D holds ((L . f) . (e ^ <*d*>)) = ((f . d) . e)

      proof

        let f be Function of D, ( Funcs (( product E),F)), e be FinSequence, d be object;

        assume

         A13: e in ( product E) & d in D;

        then

         A14: ((I . f) . (e,d)) = ((f . d) . e) by A1;

        

         A15: (J . (e,d)) = (e ^ <*d*>) by A2, A13;

         [e, d] in [:( product E), D:] by A13, ZFMISC_1:def 2;

        then

         A16: (J . (e,d)) in ( product (E ^ <*D*>)) & (K . (J . (e,d))) = [e, d] by A2, FUNCT_2: 5, FUNCT_2: 26;

        f in ( Funcs (D,( Funcs (( product E),F)))) by FUNCT_2: 8;

        then ((L . f) . (e ^ <*d*>)) = (((I . f) * K) . (J . (e,d))) by A15, A5;

        hence ((L . f) . (e ^ <*d*>)) = ((f . d) . e) by A14, A16, FUNCT_2: 15;

      end;

    end;

    reserve S,T for RealNormSpace;

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

    reserve Z for Subset of S;

    reserve i,n for Nat;

    definition

      let S be set;

      assume

       A1: S is RealNormSpace;

      :: NDIFF_6:def1

      func modetrans (S) -> RealNormSpace equals

      : Def1: S;

      correctness by A1;

    end

    definition

      let S,T be RealNormSpace;

      :: NDIFF_6:def2

      func diff_SP (S,T) -> Function means

      : Def2: ( dom it ) = NAT & (it . 0 ) = T & for i be Nat holds (it . (i + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans (it . i))));

      existence

      proof

        defpred R[ Nat, set, set] means $3 = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans $2)));

        

         A1: for n be Nat holds for x be set holds ex y be set st R[n, x, y]

        proof

          let n be Nat;

          let x be set;

          take y = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans x)));

          thus thesis;

        end;

        thus ex g be Function st ( dom g) = NAT & (g . 0 ) = T & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 1( A1);

      end;

      uniqueness

      proof

        let seq1,seq2 be Function;

        assume that

         A2: ( dom seq1) = NAT & (seq1 . 0 ) = T & for n be Nat holds (seq1 . (n + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans (seq1 . n)))) and

         A3: ( dom seq2) = NAT & (seq2 . 0 ) = T & for n be Nat holds (seq2 . (n + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans (seq2 . n))));

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

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

        proof

          let k be Nat;

          assume P[k];

          then (seq2 . (k + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans (seq1 . k)))) by A3;

          hence (seq1 . (k + 1)) = (seq2 . (k + 1)) by A2;

        end;

        

         A5: P[ 0 ] by A2, A3;

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

        then for n be object st n in ( dom seq1) holds (seq1 . n) = (seq2 . n) by A2;

        hence seq1 = seq2 by FUNCT_1: 2, A2, A3;

      end;

    end

    theorem :: NDIFF_6:7

    

     Th7: (( diff_SP (S,T)) . 0 ) = T & (( diff_SP (S,T)) . 1) = ( R_NormSpace_of_BoundedLinearOperators (S,T)) & (( diff_SP (S,T)) . 2) = ( R_NormSpace_of_BoundedLinearOperators (S,( R_NormSpace_of_BoundedLinearOperators (S,T))))

    proof

      thus

       A1: (( diff_SP (S,T)) . 0 ) = T by Def2;

      (( diff_SP (S,T)) . 1) = (( diff_SP (S,T)) . ( 0 qua Nat + 1));

      then (( diff_SP (S,T)) . 1) = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans (( diff_SP (S,T)) . 0 )))) by Def2;

      hence

       A2: (( diff_SP (S,T)) . 1) = ( R_NormSpace_of_BoundedLinearOperators (S,T)) by A1, Def1;

      (( diff_SP (S,T)) . 2) = (( diff_SP (S,T)) . (1 + 1));

      then (( diff_SP (S,T)) . 2) = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans (( diff_SP (S,T)) . 1)))) by Def2;

      hence (( diff_SP (S,T)) . 2) = ( R_NormSpace_of_BoundedLinearOperators (S,( R_NormSpace_of_BoundedLinearOperators (S,T)))) by A2, Def1;

    end;

    theorem :: NDIFF_6:8

    

     Th8: for i be Nat holds (( diff_SP (S,T)) . i) is RealNormSpace

    proof

      defpred P[ Nat] means (( diff_SP (S,T)) . $1) is RealNormSpace;

      

       A1: P[ 0 ] by Th7;

       A2:

      now

        let i be Nat;

        assume P[i];

        then

        reconsider H = (( diff_SP (S,T)) . i) as RealNormSpace;

        ( modetrans (( diff_SP (S,T)) . i)) = H by Def1;

        then (( diff_SP (S,T)) . (i + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,H)) by Def2;

        hence P[(i + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: NDIFF_6:9

    

     Th9: for i be Nat holds ex H be RealNormSpace st H = (( diff_SP (S,T)) . i) & (( diff_SP (S,T)) . (i + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,H))

    proof

      let i be Nat;

      take H = ( modetrans (( diff_SP (S,T)) . i));

      thus H = (( diff_SP (S,T)) . i) by Def1, Th8;

      thus (( diff_SP (S,T)) . (i + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,H)) by Def2;

    end;

    definition

      let S,T be RealNormSpace, i be Nat;

      :: NDIFF_6:def3

      func diff_SP (i,S,T) -> RealNormSpace equals (( diff_SP (S,T)) . i);

      correctness

      proof

        ex H be RealNormSpace st H = (( diff_SP (S,T)) . i) & (( diff_SP (S,T)) . (i + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,H)) by Th9;

        hence thesis;

      end;

    end

    theorem :: NDIFF_6:10

    

     Th10: for i be Nat holds ( diff_SP ((i + 1),S,T)) = ( R_NormSpace_of_BoundedLinearOperators (S,( diff_SP (i,S,T))))

    proof

      let i be Nat;

      set H = ( diff_SP (i,S,T));

      ex H1 be RealNormSpace st H1 = (( diff_SP (S,T)) . i) & (( diff_SP (S,T)) . (i + 1)) = ( R_NormSpace_of_BoundedLinearOperators (S,H1)) by Th9;

      hence thesis;

    end;

    definition

      let S,T be RealNormSpace, f be set;

      assume

       A1: f is PartFunc of S, T;

      :: NDIFF_6:def4

      func modetrans (f,S,T) -> PartFunc of S, T equals

      : Def4: f;

      correctness by A1;

    end

    definition

      let S,T be RealNormSpace, f be PartFunc of S, T, Z be Subset of S;

      :: NDIFF_6:def5

      func diff (f,Z) -> Function means

      : Def5: ( dom it ) = NAT & (it . 0 ) = (f | Z) & for i be Nat holds (it . (i + 1)) = (( modetrans ((it . i),S,( diff_SP (i,S,T)))) `| Z);

      existence

      proof

        defpred R[ Nat, set, set] means $3 = (( modetrans ($2,S,( diff_SP ($1,S,T)))) `| Z);

        

         A1: for n be Nat holds for x be set holds ex y be set st R[n, x, y];

        ex g be Function st ( dom g) = NAT & (g . 0 ) = (f | Z) & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 1( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Function;

        assume that

         A2: ( dom seq1) = NAT & (seq1 . 0 ) = (f | Z) & for n be Nat holds (seq1 . (n + 1)) = (( modetrans ((seq1 . n),S,( diff_SP (n,S,T)))) `| Z) and

         A3: ( dom seq2) = NAT & (seq2 . 0 ) = (f | Z) & for n be Nat holds (seq2 . (n + 1)) = (( modetrans ((seq2 . n),S,( diff_SP (n,S,T)))) `| Z);

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

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

        proof

          let k be Nat;

          assume P[k];

          then (( modetrans ((seq1 . k),S,( diff_SP (k,S,T)))) `| Z) = (seq2 . (k + 1)) by A3;

          hence (seq1 . (k + 1)) = (seq2 . (k + 1)) by A2;

        end;

        

         A5: P[ 0 ] by A2, A3;

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

        then for n be object st n in ( dom seq1) holds (seq1 . n) = (seq2 . n) by A2;

        hence seq1 = seq2 by FUNCT_1: 2, A2, A3;

      end;

    end

    theorem :: NDIFF_6:11

    

     Th11: (( diff (f,Z)) . 0 ) = (f | Z) & (( diff (f,Z)) . 1) = ((f | Z) `| Z) & (( diff (f,Z)) . 2) = (((f | Z) `| Z) `| Z)

    proof

      thus

       A1: (( diff (f,Z)) . 0 ) = (f | Z) by Def5;

      

       A2: ( diff_SP ( 0 ,S,T)) = T by Th7;

      then

       A3: ( modetrans ((( diff (f,Z)) . 0 ),S,( diff_SP ( 0 ,S,T)))) = (f | Z) by A1, Def4;

      (( diff (f,Z)) . 1) = (( diff (f,Z)) . ( 0 qua Nat + 1));

      hence

       A4: (( diff (f,Z)) . 1) = ((f | Z) `| Z) by A3, A2, Def5;

      

       A5: ( diff_SP (1,S,T)) = ( R_NormSpace_of_BoundedLinearOperators (S,T)) by Th7;

      then

       A6: ( modetrans ((( diff (f,Z)) . 1),S,( diff_SP (1,S,T)))) = ((f | Z) `| Z) by A4, Def4;

      (( diff (f,Z)) . 2) = (( diff (f,Z)) . (1 + 1));

      hence (( diff (f,Z)) . 2) = (((f | Z) `| Z) `| Z) by A5, A6, Def5;

    end;

    theorem :: NDIFF_6:12

    

     Th12: for i be Nat holds (( diff (f,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T))

    proof

      defpred P[ Nat] means (( diff (f,Z)) . $1) is PartFunc of S, ( diff_SP ($1,S,T));

      (( diff (f,Z)) . 0 ) = (f | Z) by Def5;

      then

       A1: P[ 0 ] by Th7;

       A2:

      now

        let i be Nat;

        assume P[i];

        

         A3: (( diff (f,Z)) . (i + 1)) = (( modetrans ((( diff (f,Z)) . i),S,( diff_SP (i,S,T)))) `| Z) by Def5;

        ( diff_SP ((i + 1),S,T)) = ( R_NormSpace_of_BoundedLinearOperators (S,( modetrans (( diff_SP (S,T)) . i)))) by Def2

        .= ( R_NormSpace_of_BoundedLinearOperators (S,( diff_SP (i,S,T)))) by Def1;

        hence P[(i + 1)] by A3;

      end;

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

      hence thesis;

    end;

    definition

      let S,T be RealNormSpace, f be PartFunc of S, T, Z be Subset of S, i be Nat;

      :: NDIFF_6:def6

      func diff (f,i,Z) -> PartFunc of S, ( diff_SP (i,S,T)) equals (( diff (f,Z)) . i);

      correctness by Th12;

    end

    theorem :: NDIFF_6:13

    

     Th13: ( diff (f,(i + 1),Z)) = (( diff (f,i,Z)) `| Z)

    proof

      

       A1: (( diff (f,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T)) by Th12;

      

       A2: ( modetrans (( diff_SP (S,T)) . i)) = (( diff_SP (S,T)) . i) by Def1, Th8;

      then ( modetrans ((( diff (f,Z)) . i),S,( modetrans (( diff_SP (S,T)) . i)))) = (( diff (f,Z)) . i) by A1, Def4;

      hence thesis by A2, Def5;

    end;

    definition

      let S,T be RealNormSpace;

      let f be PartFunc of S, T;

      let Z be Subset of S;

      let n be Nat;

      :: NDIFF_6:def7

      pred f is_differentiable_on n,Z means Z c= ( dom f) & for i be Nat st i <= (n - 1) holds ( modetrans ((( diff (f,Z)) . i),S,( diff_SP (i,S,T)))) is_differentiable_on Z;

    end

    theorem :: NDIFF_6:14

    

     Th14: f is_differentiable_on (n,Z) iff Z c= ( dom f) & for i be Nat st i <= (n - 1) holds ( diff (f,i,Z)) is_differentiable_on Z

    proof

      hereby

        assume

         A1: f is_differentiable_on (n,Z);

        hence Z c= ( dom f);

        hereby

          let i be Nat;

          assume i <= (n - 1);

          then ( modetrans ((( diff (f,Z)) . i),S,( diff_SP (i,S,T)))) is_differentiable_on Z by A1;

          hence ( diff (f,i,Z)) is_differentiable_on Z by Def4;

        end;

      end;

      assume

       A2: Z c= ( dom f) & for i be Nat st i <= (n - 1) holds ( diff (f,i,Z)) is_differentiable_on Z;

      now

        let i be Nat;

        assume i <= (n - 1);

        then ( diff (f,i,Z)) is_differentiable_on Z by A2;

        hence ( modetrans ((( diff (f,Z)) . i),S,( diff_SP (i,S,T)))) is_differentiable_on Z by Def4;

      end;

      hence f is_differentiable_on (n,Z) by A2;

    end;

    theorem :: NDIFF_6:15

    

     Th15: f is_differentiable_on (1,Z) iff Z c= ( dom f) & (f | Z) is_differentiable_on Z

    proof

      hereby

        assume

         A1: f is_differentiable_on (1,Z);

        hence Z c= ( dom f);

        

         A2: ( diff (f, 0 ,Z)) is_differentiable_on Z by A1, Th14;

        (( diff (f,Z)) . 0 ) = (f | Z) by Def5;

        hence (f | Z) is_differentiable_on Z by A2, Th7;

      end;

      assume

       A3: Z c= ( dom f) & (f | Z) is_differentiable_on Z;

      for i be Nat st i <= (1 - 1) holds ( diff (f,i,Z)) is_differentiable_on Z

      proof

        let i be Nat;

        assume i <= (1 - 1);

        then

         A4: i = 0 ;

        (f | Z) = ( diff (f, 0 ,Z)) by Def5;

        hence ( diff (f,i,Z)) is_differentiable_on Z by A4, A3, Th7;

      end;

      hence f is_differentiable_on (1,Z) by A3, Th14;

    end;

    theorem :: NDIFF_6:16

    f is_differentiable_on (2,Z) iff Z c= ( dom f) & (f | Z) is_differentiable_on Z & ((f | Z) `| Z) is_differentiable_on Z

    proof

      hereby

        assume

         A1: f is_differentiable_on (2,Z);

        hence Z c= ( dom f);

        

         A2: ( diff (f, 0 ,Z)) is_differentiable_on Z by A1, Th14;

        (( diff (f,Z)) . 0 ) = (f | Z) by Def5;

        hence (f | Z) is_differentiable_on Z by A2, Th7;

        

         A3: ( diff (f,1,Z)) is_differentiable_on Z by A1, Th14;

        (( diff (f,Z)) . 1) = ((f | Z) `| Z) by Th11;

        hence ((f | Z) `| Z) is_differentiable_on Z by A3, Th7;

      end;

      assume

       A4: Z c= ( dom f) & (f | Z) is_differentiable_on Z & ((f | Z) `| Z) is_differentiable_on Z;

      for i be Nat st i <= (2 - 1) holds ( diff (f,i,Z)) is_differentiable_on Z

      proof

        let i be Nat;

        assume

         A5: i <= (2 - 1);

        per cases ;

          suppose

           A6: i = 1;

          ((f | Z) `| Z) = ( diff (f,1,Z)) by Th11;

          hence ( diff (f,i,Z)) is_differentiable_on Z by A6, A4, Th7;

        end;

          suppose i <> 1;

          then i < 1 by A5, XXREAL_0: 1;

          then

           A7: i = 0 by NAT_1: 14;

          (f | Z) = ( diff (f, 0 ,Z)) by Def5;

          hence ( diff (f,i,Z)) is_differentiable_on Z by A7, A4, Th7;

        end;

      end;

      hence f is_differentiable_on (2,Z) by Th14, A4;

    end;

    theorem :: NDIFF_6:17

    

     Th17: for S,T be RealNormSpace, f be PartFunc of S, T, Z be Subset of S, n be Nat st f is_differentiable_on (n,Z) holds for m be Nat st m <= n holds f is_differentiable_on (m,Z)

    proof

      let S,T be RealNormSpace, f be PartFunc of S, T, Z be Subset of S;

      let n be Nat such that

       A1: f is_differentiable_on (n,Z);

      let m be Nat;

      assume m <= n;

      then

       A2: (m - 1) <= (n - 1) by XREAL_1: 13;

      thus Z c= ( dom f) by A1;

      thus thesis by A1, A2, XXREAL_0: 2;

    end;

    theorem :: NDIFF_6:18

    

     Th18: for n be Nat, f be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) holds Z is open

    proof

      let n be Nat, f be PartFunc of S, T;

      assume 1 <= n & f is_differentiable_on (n,Z);

      then f is_differentiable_on (1,Z) by Th17;

      then Z c= ( dom f) & (f | Z) is_differentiable_on Z by Th15;

      hence Z is open by NDIFF_1: 32;

    end;

    theorem :: NDIFF_6:19

    

     Th19: for n be Nat, f be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) holds for i be Nat st i <= n holds (( diff_SP (S,T)) . i) is RealNormSpace & (( diff (f,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T)) & ( dom ( diff (f,i,Z))) = Z

    proof

      let n be Nat, f be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z);

      let i be Nat;

      assume

       A2: i <= n;

      ( diff_SP (i,S,T)) is RealNormSpace;

      hence (( diff_SP (S,T)) . i) is RealNormSpace;

      ( diff (f,i,Z)) is PartFunc of S, ( diff_SP (i,S,T));

      hence (( diff (f,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T));

      per cases ;

        suppose i = 0 ;

        then (f | Z) = (( diff (f,Z)) . i) by Def5;

        hence ( dom ( diff (f,i,Z))) = Z by RELAT_1: 62, A1;

      end;

        suppose i <> 0 ;

        then

        reconsider i1 = (i - 1) as Element of NAT by INT_1: 3;

        

         A3: ( diff (f,(i1 + 1),Z)) = (( diff (f,i1,Z)) `| Z) by Th13;

        ( diff (f,i1,Z)) is_differentiable_on Z by A1, XREAL_1: 9, A2, Th14;

        hence ( dom ( diff (f,i,Z))) = Z by A3, NDIFF_1:def 9;

      end;

    end;

    theorem :: NDIFF_6:20

    

     Th20: for n be Nat, f,g be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z) holds for i be Nat st i <= n holds ( diff ((f + g),i,Z)) = (( diff (f,i,Z)) + ( diff (g,i,Z)))

    proof

      let n be Nat, f,g be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z);

      then

       A2: Z is open by Th18;

      defpred P[ Nat] means $1 <= n implies ( diff ((f + g),$1,Z)) = (( diff (f,$1,Z)) + ( diff (g,$1,Z)));

      

       A3: P[ 0 ]

      proof

        assume 0 <= n;

        ( diff_SP ( 0 ,S,T)) = T & (f | Z) = ( diff (f, 0 ,Z)) & (g | Z) = ( diff (g, 0 ,Z)) & ( diff ((f + g), 0 ,Z)) = ((f + g) | Z) by Def2, Def5;

        hence ( diff ((f + g), 0 ,Z)) = (( diff (f, 0 ,Z)) + ( diff (g, 0 ,Z))) by VFUNCT_1: 27;

      end;

      

       A4: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A5: P[i];

        assume

         A6: (i + 1) <= n;

        then ((i + 1) - 1) <= (n - 1) by XREAL_1: 9;

        then

         A7: ( diff (f,i,Z)) is_differentiable_on Z & ( diff (g,i,Z)) is_differentiable_on Z by Th14, A1;

        

         A8: i <= (i + 1) by NAT_1: 11;

        then

         A9: i <= n by A6, XXREAL_0: 2;

        set f0 = ( diff (f,i,Z));

        set g0 = ( diff (g,i,Z));

        

         A10: (( diff_SP (S,T)) . i) is RealNormSpace & (( diff (f,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T)) & ( dom ( diff (f,i,Z))) = Z by Th19, A9, A1;

        

         A11: (( diff_SP (S,T)) . i) is RealNormSpace & (( diff (g,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T)) & ( dom ( diff (g,i,Z))) = Z by Th19, A9, A1;

        Z = (( dom f0) /\ Z) by A10;

        then

         A12: Z = ( dom (f0 + g0)) by A11, VFUNCT_1:def 1;

        then (f0 + g0) is_differentiable_on Z by A2, A7, NDIFF_1: 39;

        then

         A13: ( dom ((f0 + g0) `| Z)) = Z by NDIFF_1:def 9;

        

         A14: (f0 `| Z) = ( diff (f,(i + 1),Z)) & (g0 `| Z) = ( diff (g,(i + 1),Z)) & ( diff ((f + g),(i + 1),Z)) = (( diff ((f + g),i,Z)) `| Z) by Th13;

        

         A15: ( dom (f0 `| Z)) = Z & ( dom (g0 `| Z)) = Z by A7, NDIFF_1:def 9;

        then

         A16: ( dom ((f0 `| Z) + (g0 `| Z))) = (Z /\ Z) & ( dom (( diff (f,(i + 1),Z)) + ( diff (g,(i + 1),Z)))) = (Z /\ Z) by A14, VFUNCT_1:def 1;

        now

          let x be Point of S;

          assume

           A17: x in ( dom (( diff (f,(i + 1),Z)) + ( diff (g,(i + 1),Z))));

          then (((f0 `| Z) + (g0 `| Z)) . x) = (((f0 `| Z) + (g0 `| Z)) /. x) by A16, PARTFUN1:def 6;

          then

           A18: (((f0 `| Z) + (g0 `| Z)) . x) = (((f0 `| Z) /. x) + ((g0 `| Z) /. x)) by A17, A16, VFUNCT_1:def 1;

          ((f0 `| Z) /. x) = (( diff (f,(i + 1),Z)) . x) & ((g0 `| Z) /. x) = (( diff (g,(i + 1),Z)) . x) by A16, A17, A14, A15, PARTFUN1:def 6;

          then ((f0 `| Z) /. x) = (( diff (f,(i + 1),Z)) /. x) & ((g0 `| Z) /. x) = (( diff (g,(i + 1),Z)) /. x) by A16, A17, A14, A15, PARTFUN1:def 6;

          then (((f0 `| Z) + (g0 `| Z)) . x) = ((( diff (f,(i + 1),Z)) /. x) + (( diff (g,(i + 1),Z)) /. x)) by A18, Th10;

          then (((f0 `| Z) + (g0 `| Z)) . x) = ((( diff (f,(i + 1),Z)) + ( diff (g,(i + 1),Z))) /. x) by A17, VFUNCT_1:def 1;

          then

           A19: ((( diff (f,(i + 1),Z)) + ( diff (g,(i + 1),Z))) . x) = (((f0 `| Z) + (g0 `| Z)) . x) by A17, PARTFUN1:def 6;

          (((f0 + g0) `| Z) /. x) = (( diff (f0,x)) + ( diff (g0,x))) by NDIFF_1: 39, A7, A2, A12, A16, A17;

          then

           A20: (((f0 + g0) `| Z) /. x) = (((f0 `| Z) /. x) + ( diff (g0,x))) by NDIFF_1:def 9, A7, A16, A17;

          (( diff ((f + g),(i + 1),Z)) . x) = (((f0 + g0) `| Z) /. x) by A14, A5, A8, A16, A13, A17, PARTFUN1:def 6, A6, XXREAL_0: 2;

          hence (( diff ((f + g),(i + 1),Z)) . x) = ((( diff (f,(i + 1),Z)) + ( diff (g,(i + 1),Z))) . x) by A18, A19, A20, NDIFF_1:def 9, A7, A16, A17;

        end;

        hence ( diff ((f + g),(i + 1),Z)) = (( diff (f,(i + 1),Z)) + ( diff (g,(i + 1),Z))) by A16, A13, A14, A8, A5, A6, XXREAL_0: 2, PARTFUN1: 5;

      end;

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

      hence thesis;

    end;

    theorem :: NDIFF_6:21

    for n be Nat, f,g be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z) holds (f + g) is_differentiable_on (n,Z)

    proof

      let n be Nat, f,g be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z);

      then

       A2: Z is open by Th18;

      (Z /\ Z) c= (( dom f) /\ ( dom g)) by A1, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (f + g)) by VFUNCT_1:def 1;

      for i be Nat st i <= (n - 1) holds ( diff ((f + g),i,Z)) is_differentiable_on Z

      proof

        let i be Nat;

        assume

         A4: i <= (n - 1);

        then

         A5: ( diff (f,i,Z)) is_differentiable_on Z & ( diff (g,i,Z)) is_differentiable_on Z by Th14, A1;

        (n - 1) <= n by XREAL_1: 43;

        then

         A6: i <= n by A4, XXREAL_0: 2;

        then ( dom ( diff (f,i,Z))) = Z & ( dom ( diff (g,i,Z))) = Z by Th19, A1;

        then (Z /\ Z) c= (( dom ( diff (f,i,Z))) /\ ( dom ( diff (g,i,Z))));

        then Z c= ( dom (( diff (f,i,Z)) + ( diff (g,i,Z)))) by VFUNCT_1:def 1;

        then (( diff (f,i,Z)) + ( diff (g,i,Z))) is_differentiable_on Z by A2, A5, NDIFF_1: 39;

        hence ( diff ((f + g),i,Z)) is_differentiable_on Z by A1, A6, Th20;

      end;

      hence thesis by Th14, A3;

    end;

    theorem :: NDIFF_6:22

    

     Th22: for n be Nat, f,g be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z) holds for i be Nat st i <= n holds ( diff ((f - g),i,Z)) = (( diff (f,i,Z)) - ( diff (g,i,Z)))

    proof

      let n be Nat, f,g be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z);

      then

       A2: Z is open by Th18;

      defpred P[ Nat] means $1 <= n implies ( diff ((f - g),$1,Z)) = (( diff (f,$1,Z)) - ( diff (g,$1,Z)));

      

       A3: P[ 0 ]

      proof

        assume 0 <= n;

        ( diff_SP ( 0 ,S,T)) = T & (f | Z) = ( diff (f, 0 ,Z)) & (g | Z) = ( diff (g, 0 ,Z)) & ( diff ((f - g), 0 ,Z)) = ((f - g) | Z) by Def2, Def5;

        hence ( diff ((f - g), 0 ,Z)) = (( diff (f, 0 ,Z)) - ( diff (g, 0 ,Z))) by VFUNCT_1: 30;

      end;

      

       A4: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A5: P[i];

        assume

         A6: (i + 1) <= n;

        then ((i + 1) - 1) <= (n - 1) by XREAL_1: 9;

        then

         A7: ( diff (f,i,Z)) is_differentiable_on Z & ( diff (g,i,Z)) is_differentiable_on Z by Th14, A1;

        

         A8: i <= (i + 1) by NAT_1: 11;

        then

         A9: i <= n by A6, XXREAL_0: 2;

        set f0 = ( diff (f,i,Z));

        set g0 = ( diff (g,i,Z));

        

         A10: (( diff_SP (S,T)) . i) is RealNormSpace & (( diff (f,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T)) & ( dom ( diff (f,i,Z))) = Z by Th19, A9, A1;

        

         A11: (( diff_SP (S,T)) . i) is RealNormSpace & (( diff (g,Z)) . i) is PartFunc of S, ( diff_SP (i,S,T)) & ( dom ( diff (g,i,Z))) = Z by Th19, A9, A1;

        Z = (( dom f0) /\ Z) by A10;

        then

         A12: Z = ( dom (f0 - g0)) by A11, VFUNCT_1:def 2;

        then (f0 - g0) is_differentiable_on Z by A2, A7, NDIFF_1: 40;

        then

         A13: ( dom ((f0 - g0) `| Z)) = Z by NDIFF_1:def 9;

        

         A14: (f0 `| Z) = ( diff (f,(i + 1),Z)) & (g0 `| Z) = ( diff (g,(i + 1),Z)) & ( diff ((f - g),(i + 1),Z)) = (( diff ((f - g),i,Z)) `| Z) by Th13;

        

         A15: ( dom (f0 `| Z)) = Z & ( dom (g0 `| Z)) = Z by A7, NDIFF_1:def 9;

        then

         A16: ( dom ((f0 `| Z) - (g0 `| Z))) = (Z /\ Z) & ( dom (( diff (f,(i + 1),Z)) - ( diff (g,(i + 1),Z)))) = (Z /\ Z) by A14, VFUNCT_1:def 2;

        now

          let x be Point of S;

          assume

           A17: x in ( dom (( diff (f,(i + 1),Z)) - ( diff (g,(i + 1),Z))));

          then (((f0 `| Z) - (g0 `| Z)) . x) = (((f0 `| Z) - (g0 `| Z)) /. x) by A16, PARTFUN1:def 6;

          then

           A18: (((f0 `| Z) - (g0 `| Z)) . x) = (((f0 `| Z) /. x) - ((g0 `| Z) /. x)) by A17, A16, VFUNCT_1:def 2;

          ((f0 `| Z) /. x) = (( diff (f,(i + 1),Z)) . x) & ((g0 `| Z) /. x) = (( diff (g,(i + 1),Z)) . x) by A16, A17, A14, A15, PARTFUN1:def 6;

          then ((f0 `| Z) /. x) = (( diff (f,(i + 1),Z)) /. x) & ((g0 `| Z) /. x) = (( diff (g,(i + 1),Z)) /. x) by A16, A17, A14, A15, PARTFUN1:def 6;

          then (((f0 `| Z) - (g0 `| Z)) . x) = ((( diff (f,(i + 1),Z)) /. x) - (( diff (g,(i + 1),Z)) /. x)) by A18, Th10;

          then (((f0 `| Z) - (g0 `| Z)) . x) = ((( diff (f,(i + 1),Z)) - ( diff (g,(i + 1),Z))) /. x) by A17, VFUNCT_1:def 2;

          then

           A19: ((( diff (f,(i + 1),Z)) - ( diff (g,(i + 1),Z))) . x) = (((f0 `| Z) - (g0 `| Z)) . x) by A17, PARTFUN1:def 6;

          (((f0 - g0) `| Z) /. x) = (( diff (f0,x)) - ( diff (g0,x))) by NDIFF_1: 40, A7, A2, A12, A16, A17;

          then

           A20: (((f0 - g0) `| Z) /. x) = (((f0 `| Z) /. x) - ( diff (g0,x))) by NDIFF_1:def 9, A7, A16, A17;

          (( diff ((f - g),(i + 1),Z)) . x) = (((f0 - g0) `| Z) /. x) by A14, A5, A8, A16, A13, A17, PARTFUN1:def 6, A6, XXREAL_0: 2;

          hence (( diff ((f - g),(i + 1),Z)) . x) = ((( diff (f,(i + 1),Z)) - ( diff (g,(i + 1),Z))) . x) by A18, A19, A20, NDIFF_1:def 9, A7, A16, A17;

        end;

        hence ( diff ((f - g),(i + 1),Z)) = (( diff (f,(i + 1),Z)) - ( diff (g,(i + 1),Z))) by A16, A13, A14, A8, A5, A6, XXREAL_0: 2, PARTFUN1: 5;

      end;

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

      hence thesis;

    end;

    theorem :: NDIFF_6:23

    for n be Nat, f,g be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z) holds (f - g) is_differentiable_on (n,Z)

    proof

      let n be Nat, f,g be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z) & g is_differentiable_on (n,Z);

      then

       A2: Z is open by Th18;

      (Z /\ Z) c= (( dom f) /\ ( dom g)) by A1, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (f - g)) by VFUNCT_1:def 2;

      for i be Nat st i <= (n - 1) holds ( diff ((f - g),i,Z)) is_differentiable_on Z

      proof

        let i be Nat;

        assume

         A4: i <= (n - 1);

        then

         A5: ( diff (f,i,Z)) is_differentiable_on Z & ( diff (g,i,Z)) is_differentiable_on Z by Th14, A1;

        (n - 1) <= n by XREAL_1: 43;

        then

         A6: i <= n by A4, XXREAL_0: 2;

        then ( dom ( diff (f,i,Z))) = Z & ( dom ( diff (g,i,Z))) = Z by Th19, A1;

        then (Z /\ Z) c= (( dom ( diff (f,i,Z))) /\ ( dom ( diff (g,i,Z))));

        then Z c= ( dom (( diff (f,i,Z)) - ( diff (g,i,Z)))) by VFUNCT_1:def 2;

        then (( diff (f,i,Z)) - ( diff (g,i,Z))) is_differentiable_on Z by A2, A5, NDIFF_1: 40;

        hence ( diff ((f - g),i,Z)) is_differentiable_on Z by A1, A6, Th22;

      end;

      hence thesis by Th14, A3;

    end;

    theorem :: NDIFF_6:24

    

     Th24: for n be Nat, r be Real, f be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) holds for i be Nat st i <= n holds ( diff ((r (#) f),i,Z)) = (r (#) ( diff (f,i,Z)))

    proof

      let n be Nat, r be Real, f be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z);

      

       A2: Z is open by Th18, A1;

      defpred P[ Nat] means $1 <= n implies ( diff ((r (#) f),$1,Z)) = (r (#) ( diff (f,$1,Z)));

      

       A3: P[ 0 ]

      proof

        assume 0 <= n;

        set H = (( diff_SP (S,T)) . 0 );

        (( diff_SP (S,T)) . 0 ) = T & (f | Z) = ( diff (f, 0 ,Z)) by Def2, Def5;

        then ((r (#) f) | Z) = (r (#) ( diff (f, 0 ,Z))) by VFUNCT_1: 31;

        hence ( diff ((r (#) f), 0 ,Z)) = (r (#) ( diff (f, 0 ,Z))) by Def5;

      end;

      

       A4: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A5: P[i];

        assume

         A6: (i + 1) <= n;

        

         A7: i <= (i + 1) by NAT_1: 11;

        then

         A8: i <= n by A6, XXREAL_0: 2;

        ((i + 1) - 1) <= (n - 1) by A6, XREAL_1: 9;

        then

         A9: ( diff (f,i,Z)) is_differentiable_on Z by Th14, A1;

        then

         A10: Z = ( dom (( diff (f,i,Z)) `| Z)) by NDIFF_1:def 9;

        ( dom ( diff (f,i,Z))) = Z by Th19, A8, A1;

        then

         A11: Z = ( dom (r (#) ( diff (f,i,Z)))) by VFUNCT_1:def 4;

        then (r (#) ( diff (f,i,Z))) is_differentiable_on Z by A2, A9, NDIFF_1: 41;

        then

         A12: ( dom ((r (#) ( diff (f,i,Z))) `| Z)) = Z by NDIFF_1:def 9;

        now

          let x be Point of S;

          assume

           A13: x in ( dom ((r (#) ( diff (f,i,Z))) `| Z));

          then (((r (#) ( diff (f,i,Z))) `| Z) /. x) = (r * ( diff (( diff (f,i,Z)),x))) by NDIFF_1: 41, A9, A2, A11, A12;

          hence (((r (#) ( diff (f,i,Z))) `| Z) /. x) = (r * ((( diff (f,i,Z)) `| Z) /. x)) by NDIFF_1:def 9, A9, A12, A13;

        end;

        then

         A14: ((r (#) ( diff (f,i,Z))) `| Z) = (r (#) (( diff (f,i,Z)) `| Z)) by A12, A10, VFUNCT_1:def 4;

        

         A15: ( diff_SP ((i + 1),S,T)) = ( R_NormSpace_of_BoundedLinearOperators (S,( diff_SP (i,S,T)))) by Th10;

        ( diff ((r (#) f),(i + 1),Z)) = (( diff ((r (#) f),i,Z)) `| Z) by Th13;

        hence ( diff ((r (#) f),(i + 1),Z)) = (r (#) ( diff (f,(i + 1),Z))) by Th13, A15, A14, A5, A7, A6, XXREAL_0: 2;

      end;

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

      hence thesis;

    end;

    theorem :: NDIFF_6:25

    

     Th25: for n be Nat, r be Real, f be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) holds (r (#) f) is_differentiable_on (n,Z)

    proof

      let n be Nat, r be Real, f be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z);

      then

       A2: Z c= ( dom (r (#) f)) by VFUNCT_1:def 4;

      

       A3: Z is open by Th18, A1;

      for i be Nat st i <= (n - 1) holds ( diff ((r (#) f),i,Z)) is_differentiable_on Z

      proof

        let i be Nat;

        assume

         A4: i <= (n - 1);

        set H = ( diff_SP (i,S,T));

        set f1 = ( diff (f,i,Z));

        

         A5: ( diff (f,i,Z)) is_differentiable_on Z by A1, A4, Th14;

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

        then

         A6: i <= n by A4, XXREAL_0: 2;

        then

         A7: ( diff ((r (#) f),i,Z)) = (r (#) ( diff (f,i,Z))) by A1, Th24;

        ( dom ( diff (f,i,Z))) = Z by Th19, A6, A1;

        then Z c= ( dom (r (#) f1)) by VFUNCT_1:def 4;

        hence ( diff ((r (#) f),i,Z)) is_differentiable_on Z by A3, A5, A7, NDIFF_1: 41;

      end;

      hence thesis by Th14, A2;

    end;

    theorem :: NDIFF_6:26

    for n be Nat, f be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) holds for i be Nat st i <= n holds ( diff (( - f),i,Z)) = ( - ( diff (f,i,Z)))

    proof

      let n be Nat, f be PartFunc of S, T;

      assume

       A1: 1 <= n & f is_differentiable_on (n,Z);

      let i be Nat;

      assume i <= n;

      then ( diff ((( - 1) (#) f),i,Z)) = (( - 1) (#) ( diff (f,i,Z))) by Th24, A1;

      then (( diff ((( - 1) (#) f),Z)) . i) = ( - ( diff (f,i,Z))) by VFUNCT_1: 23;

      hence ( diff (( - f),i,Z)) = ( - ( diff (f,i,Z))) by VFUNCT_1: 23;

    end;

    theorem :: NDIFF_6:27

    for n be Nat, f be PartFunc of S, T st 1 <= n & f is_differentiable_on (n,Z) holds ( - f) is_differentiable_on (n,Z)

    proof

      let n be Nat, f be PartFunc of S, T;

      assume 1 <= n & f is_differentiable_on (n,Z);

      then (( - 1) (#) f) is_differentiable_on (n,Z) by Th25;

      hence thesis by VFUNCT_1: 23;

    end;