pdiffeq1.miz



    begin

    reserve m,n for non zero Element of NAT ;

    reserve i,j,k for Element of NAT ;

    reserve Z for Subset of ( REAL 2);

    reserve c for Real;

    reserve I for non empty FinSequence of NAT ;

    reserve d1,d2 for Element of REAL ;

    

     LMSIN1: for n be Nat holds ( sin . (n * PI )) = 0

    proof

      defpred P[ Nat] means ( sin . ($1 * PI )) = 0 ;

      

       A1: P[ 0 ] by SIN_COS: 30;

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: P[n];

        ( sin . ((n + 1) * PI )) = ( sin . ((n * PI ) + PI ))

        .= (( 0 * ( cos . PI )) + (( cos . (n * PI )) * ( sin . PI ))) by SIN_COS: 74, A3

        .= 0 by SIN_COS: 77;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: PDIFFEQ1:1

    

     DOMP1: for m be non zero Element of NAT , X be Subset of ( REAL m), I be non empty FinSequence of NAT , f be PartFunc of ( REAL m), REAL st f is_partial_differentiable_on (X,I) holds ( dom (f `partial| (X,I))) = X

    proof

      let m be non zero Element of NAT , Z be Subset of ( REAL m), I be non empty FinSequence of NAT , f be PartFunc of ( REAL m), REAL ;

      reconsider k = (( len I) - 1) as Element of NAT by INT_1: 5, FINSEQ_1: 20;

      assume f is_partial_differentiable_on (Z,I);

      then

       A1: (( PartDiffSeq (f,Z,I)) . k) is_partial_differentiable_on (Z,(I /. (k + 1)));

      ( dom (( PartDiffSeq (f,Z,I)) . (k + 1))) = ( dom ((( PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1))))) by PDIFF_9:def 7;

      hence thesis by A1, PDIFF_9:def 6;

    end;

    registration

      cluster ( [#] REAL ) -> open;

      coherence

      proof

        now

          let r be Element of REAL ;

          assume r in ( [#] REAL );

           ].(r - 1), (r + 1).[ is Neighbourhood of r by RCOMP_1:def 6;

          hence ex N be Neighbourhood of r st N c= ( [#] REAL );

        end;

        hence thesis by RCOMP_1: 20;

      end;

      cluster ( [#] ( REAL 2)) -> open;

      coherence

      proof

        for x be Element of ( REAL 2) st x in ( [#] ( REAL 2)) holds ex r be Real st r > 0 & { y where y be Element of ( REAL 2) : |.(y - x).| < r } c= ( [#] ( REAL 2))

        proof

          let x be Element of ( REAL 2);

          assume x in ( [#] ( REAL 2));

          take 1;

          thus 0 < 1;

          now

            let s be object;

            assume s in { y where y be Element of ( REAL 2) : |.(y - x).| < 1 };

            then ex y be Element of ( REAL 2) st s = y & |.(y - x).| < 1;

            hence s in ( [#] ( REAL 2));

          end;

          hence { y where y be Element of ( REAL 2) : |.(y - x).| < 1 } c= ( [#] ( REAL 2));

        end;

        hence thesis by PDIFF_7: 31;

      end;

    end

    

     LMOP3: ( [#] ( REAL 2)) = { <*x, t*> where x,t be Real : x in ( [#] REAL ) & t in ( [#] REAL ) }

    proof

      set S = { <*x, t*> where x,t be Real : x in ( [#] REAL ) & t in ( [#] REAL ) };

      for z be object holds (z in ( [#] ( REAL 2)) iff z in S)

      proof

        let z be object;

        hereby

          assume z in ( [#] ( REAL 2));

          then z in the set of all <*d1, d2*> where d1,d2 be Element of REAL by FINSEQ_2: 99;

          then ex d1,d2 be Element of REAL st z = <*d1, d2*>;

          hence z in S;

        end;

        assume z in S;

        then ex x,t be Real st z = <*x, t*> & x in ( [#] REAL ) & t in ( [#] REAL );

        then z in the set of all <*d1, d2*> where d1,d2 be Element of REAL ;

        hence z in ( [#] ( REAL 2)) by FINSEQ_2: 99;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     LM001: for f be PartFunc of REAL , REAL , Z be Subset of REAL , x0 be Real st Z is open & x0 in Z & f is_differentiable_in x0 holds (f | Z) is_differentiable_in x0 & ( diff (f,x0)) = ( diff ((f | Z),x0))

    proof

      let f be PartFunc of REAL , REAL , Z be Subset of REAL , x0 be Real;

      assume that

       AS1: Z is open and

       AS3: x0 in Z and

       AS4: f is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A10: N1 c= Z by AS1, AS3, RCOMP_1: 18;

      consider N be Neighbourhood of x0 such that

       A11: N c= ( dom f) and

       A12: ex L be LinearFunc, R be RestFunc st for x be Real st x in N holds ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by AS4, FDIFF_1:def 4;

      consider N2 be Neighbourhood of x0 such that

       A13: N2 c= N1 and

       A14: N2 c= N by RCOMP_1: 17;

      

       A15: N2 c= Z by A10, A13;

      N2 c= ( dom f) by A11, A14;

      then N2 c= (( dom f) /\ Z) by A15, XBOOLE_1: 19;

      then

       A16: N2 c= ( dom (f | Z)) by RELAT_1: 61;

      consider L be LinearFunc, R be RestFunc such that

       A17: for x be Real st x in N holds ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A12;

      

       A18: x0 in N2 by RCOMP_1: 16;

       Y1:

      now

        let x be Real;

        assume

         A19: x in N2;

        then ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A14, A17;

        then (((f | Z) . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A16, A19, FUNCT_1: 47;

        hence (((f | Z) . x) - ((f | Z) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A16, A18, FUNCT_1: 47;

      end;

      hence (f | Z) is_differentiable_in x0 by A16, FDIFF_1:def 4;

      

      hence ( diff ((f | Z),x0)) = (L . 1) by A16, Y1, FDIFF_1:def 5

      .= ( diff (f,x0)) by AS4, A11, A17, FDIFF_1:def 5;

    end;

    theorem :: PDIFFEQ1:2

    

     LM002: for f be PartFunc of REAL , REAL , Z be Subset of REAL , x0 be Real st Z is open & x0 in Z holds (f is_differentiable_in x0 iff (f | Z) is_differentiable_in x0) & (f is_differentiable_in x0 implies ( diff (f,x0)) = ( diff ((f | Z),x0)))

    proof

      let f be PartFunc of REAL , REAL , Z be Subset of REAL , x0 be Real;

      assume that

       AS1: Z is open and

       AS3: x0 in Z;

      thus f is_differentiable_in x0 iff (f | Z) is_differentiable_in x0

      proof

        thus f is_differentiable_in x0 implies (f | Z) is_differentiable_in x0 by LM001, AS1, AS3;

        thus (f | Z) is_differentiable_in x0 implies f is_differentiable_in x0

        proof

          assume (f | Z) is_differentiable_in x0;

          then

          consider N be Neighbourhood of x0 such that

           A11: N c= ( dom (f | Z)) and

           A12: ex L be LinearFunc, R be RestFunc st for x be Real st x in N holds (((f | Z) . x) - ((f | Z) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by FDIFF_1:def 4;

          consider L be LinearFunc, R be RestFunc such that

           A17: for x be Real st x in N holds (((f | Z) . x) - ((f | Z) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A12;

          

           Y0: ( dom (f | Z)) c= ( dom f) by RELAT_1: 60;

          now

            let x be Real;

            assume

             A19: x in N;

            then

             A20: x in Z by RELAT_1: 58, A11, TARSKI:def 3;

            (((f | Z) . x) - ((f | Z) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A17, A19;

            then (((f | Z) . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by AS3, FUNCT_1: 49;

            hence ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A20, FUNCT_1: 49;

          end;

          hence f is_differentiable_in x0 by Y0, A11, XBOOLE_1: 1, FDIFF_1:def 4;

        end;

      end;

      thus (f is_differentiable_in x0 implies ( diff (f,x0)) = ( diff ((f | Z),x0))) by AS1, AS3, LM001;

    end;

    theorem :: PDIFFEQ1:3

    

     LM003: for f be PartFunc of REAL , REAL , X be Subset of REAL st X is open & X c= ( dom f) holds f is_differentiable_on X iff (f | X) is_differentiable_on X

    proof

      let f be PartFunc of REAL , REAL , X be Subset of REAL ;

      assume that

       AS1: X is open and

       AS2: X c= ( dom f);

      hereby

        assume

         A1: f is_differentiable_on X;

        

         A3: ( dom (f | X)) = X by RELAT_1: 62, AS2;

        now

          let x be Real;

          assume

           A4: x in X;

          then f is_differentiable_in x by A1, AS1, FDIFF_1: 9;

          hence (f | X) is_differentiable_in x by LM002, AS1, A4;

        end;

        hence (f | X) is_differentiable_on X by AS1, A3, FDIFF_1: 9;

      end;

      assume

       A1: (f | X) is_differentiable_on X;

      now

        let x be Real;

        assume

         A4: x in X;

        then (f | X) is_differentiable_in x by A1, AS1, FDIFF_1: 9;

        hence f is_differentiable_in x by LM002, AS1, A4;

      end;

      hence f is_differentiable_on X by AS1, AS2, FDIFF_1: 9;

    end;

    theorem :: PDIFFEQ1:4

    

     LM00: for f be PartFunc of REAL , REAL , X be Subset of REAL st X is open & X c= ( dom f) & f is_differentiable_on X holds ((f | X) `| X) = (f `| X)

    proof

      let f be PartFunc of REAL , REAL , X be Subset of REAL ;

      assume that

       AS1: X is open and

       AS2: X c= ( dom f) and

       AS3: f is_differentiable_on X;

      

       A1: (f | X) is_differentiable_on X by AS1, AS2, AS3, LM003;

      

       A2: ( dom (f `| X)) = X & for x be Real st x in X holds ((f `| X) . x) = ( diff (f,x)) by FDIFF_1:def 7, AS3;

      

       A3: ( dom ((f | X) `| X)) = X & for x be Real st x in X holds (((f | X) `| X) . x) = ( diff ((f | X),x)) by FDIFF_1:def 7, A1;

      now

        let x be object;

        assume

         A4: x in ( dom ((f | X) `| X));

        then

         A5: x in X by FDIFF_1:def 7, A1;

        reconsider x0 = x as Real by A4;

        

         A6: f is_differentiable_in x0 by AS1, AS3, A5, FDIFF_1: 9;

        

        thus (((f | X) `| X) . x) = ( diff ((f | X),x0)) by FDIFF_1:def 7, A1, A5

        .= ( diff (f,x0)) by A6, AS1, A5, LM002

        .= ((f `| X) . x) by FDIFF_1:def 7, AS3, A5;

      end;

      hence ((f | X) `| X) = (f `| X) by FUNCT_1: 2, A2, A3;

    end;

    theorem :: PDIFFEQ1:5

    

     DIFF1: for f be PartFunc of REAL , REAL , Z be Subset of REAL st Z c= ( dom f) & Z is open & f is_differentiable_on (1,Z) holds f is_differentiable_on Z & (( diff (f,Z)) . 1) = (f `| Z)

    proof

      let f be PartFunc of REAL , REAL , Z be Subset of REAL ;

      assume

       AS: Z c= ( dom f) & Z is open & f is_differentiable_on (1,Z);

      then (( diff (f,Z)) . 0 ) is_differentiable_on Z;

      then (f | Z) is_differentiable_on Z by TAYLOR_1:def 5;

      hence

       X1: f is_differentiable_on Z by LM003, AS;

      

      thus (( diff (f,Z)) . 1) = (( diff (f,Z)) . ( 0 + 1))

      .= ((( diff (f,Z)) . 0 ) `| Z) by TAYLOR_1:def 5

      .= ((f | Z) `| Z) by TAYLOR_1:def 5

      .= (f `| Z) by AS, X1, LM00;

    end;

    theorem :: PDIFFEQ1:6

    

     DIFF2: for f be PartFunc of REAL , REAL , Z be Subset of REAL st Z c= ( dom f) & Z is open & f is_differentiable_on (2,Z) holds f is_differentiable_on Z & (( diff (f,Z)) . 1) = (f `| Z) & (f `| Z) is_differentiable_on Z & (( diff (f,Z)) . 2) = ((f `| Z) `| Z)

    proof

      let f be PartFunc of REAL , REAL , Z be Subset of REAL ;

      assume

       AS: Z c= ( dom f) & Z is open & f is_differentiable_on (2,Z);

      f is_differentiable_on (1,Z) by AS, TAYLOR_1: 23;

      then

       A3: f is_differentiable_on Z & (( diff (f,Z)) . 1) = (f `| Z) by AS, DIFF1;

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

      .= ((f `| Z) `| Z) by TAYLOR_1:def 5, A3;

      hence thesis by AS, A3;

    end;

    

     LM02: for x,t be Real holds <*x, t*> in ( REAL 2)

    proof

      let x,t be Real;

      

       P1: (2 -tuples_on REAL ) = the set of all <*d1, d2*> by FINSEQ_2: 99;

      x in REAL & t in REAL by XREAL_0:def 1;

      hence <*x, t*> in ( REAL 2) by P1;

    end;

    

     LM03: for x,t be Real, z be Element of ( REAL 2) st z = <*x, t*> holds (( proj (1,2)) . z) = x & (( proj (2,2)) . z) = t

    proof

      let x,t be Real, z be Element of ( REAL 2);

      assume

       AS: z = <*x, t*>;

      

      thus (( proj (1,2)) . z) = (z . 1) by PDIFF_1:def 1

      .= x by AS, FINSEQ_1: 44;

      

      thus (( proj (2,2)) . z) = (z . 2) by PDIFF_1:def 1

      .= t by AS, FINSEQ_1: 44;

    end;

    theorem :: PDIFFEQ1:7

    

     LM10: for X,T be Subset of REAL , f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL st X c= ( dom f) & T c= ( dom g) holds ex u be PartFunc of ( REAL 2), REAL st ( dom u) = { <*x, t*> where x,t be Real : x in X & t in T } & for x,t be Real st x in X & t in T holds (u /. <*x, t*>) = ((f /. x) * (g /. t))

    proof

      let X,T be Subset of REAL , f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL ;

      assume X c= ( dom f) & T c= ( dom g);

      defpred P1[ object, object] means ex x,t be Real st x in X & t in T & $1 = <*x, t*> & $2 = ((f /. x) * (g /. t));

      

       P1: for z,w be object st z in ( REAL 2) & P1[z, w] holds w in REAL ;

      

       P2: for z,w1,w2 be object st z in ( REAL 2) & P1[z, w1] & P1[z, w2] holds w1 = w2

      proof

        let z,w1,w2 be object;

        assume that z in ( REAL 2) and

         P21: P1[z, w1] and

         P22: P1[z, w2];

        consider x1,t1 be Real such that

         P23: z = <*x1, t1*> & w1 = ((f /. x1) * (g /. t1)) by P21;

        consider x2,t2 be Real such that

         P24: z = <*x2, t2*> & w2 = ((f /. x2) * (g /. t2)) by P22;

        x1 = x2 & t1 = t2 by P23, P24, FINSEQ_1: 77;

        hence w1 = w2 by P23, P24;

      end;

      consider u be PartFunc of ( REAL 2), REAL such that

       P3: for z be object holds (z in ( dom u) iff (z in ( REAL 2) & ex w be object st P1[z, w])) and

       P4: for z be object st z in ( dom u) holds P1[z, (u . z)] from PARTFUN1:sch 2( P1, P2);

      take u;

      for z be object holds (z in ( dom u) iff z in { <*x, t*> where x,t be Real : x in X & t in T })

      proof

        let z be object;

        hereby

          assume z in ( dom u);

          then z in ( REAL 2) & ex w be object st P1[z, w] by P3;

          hence z in { <*x, t*> where x,t be Real : x in X & t in T };

        end;

        assume z in { <*x, t*> where x,t be Real : x in X & t in T };

        then

        consider x,t be Real such that

         P51: z = <*x, t*> & x in X & t in T;

        ((f /. x) * (g /. t)) in REAL ;

        hence z in ( dom u) by P3, P51, LM02;

      end;

      hence

       P5: ( dom u) = { <*x, t*> where x,t be Real : x in X & t in T } by TARSKI: 2;

      let x,t be Real;

      assume x in X & t in T;

      then

       P7: <*x, t*> in ( dom u) by P5;

      then

      consider x1,t1 be Real such that x1 in X & t1 in T and

       P9: <*x, t*> = <*x1, t1*> and

       P10: (u . <*x, t*>) = ((f /. x1) * (g /. t1)) by P4;

      x = x1 & t = t1 by P9, FINSEQ_1: 77;

      hence (u /. <*x, t*>) = ((f /. x) * (g /. t)) by P10, P7, PARTFUN1:def 6;

    end;

    theorem :: PDIFFEQ1:8

    

     LM11: for f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL , x0,t0 be Real, z be Element of ( REAL 2) st ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } & (for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t))) & z = <*x0, t0*> & x0 in ( dom f) & t0 in ( dom g) holds (u * ( reproj (1,z))) = ((g /. t0) (#) f) & (u * ( reproj (2,z))) = ((f /. x0) (#) g)

    proof

      let f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL , x0,t0 be Real, z be Element of ( REAL 2);

      assume that

       AS1: ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } and

       AS2: for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t)) and

       AS3: z = <*x0, t0*> & x0 in ( dom f) & t0 in ( dom g);

      

       P21: for s be object holds s in ( dom (u * ( reproj (1,z)))) iff s in ( dom f)

      proof

        let s be object;

        hereby

          assume

           P10: s in ( dom (u * ( reproj (1,z))));

          then

          reconsider r = s as Real;

          

           A4a: r is Element of REAL by XREAL_0:def 1;

          (( reproj (1,z)) . r) = ( Replace (z,1,r)) by PDIFF_1:def 5, A4a

          .= <*r, t0*> by AS3, FINSEQ_7: 13, A4a;

          then <*r, t0*> in { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } by P10, FUNCT_1: 11, AS1;

          then ex x,t be Real st <*r, t0*> = <*x, t*> & x in ( dom f) & t in ( dom g);

          hence s in ( dom f) by FINSEQ_1: 77;

        end;

        assume

         P12: s in ( dom f);

        then

        reconsider r = s as Real;

        

         P13: s in REAL by P12;

        

         P14: (( reproj (1,z)) . r) = ( Replace (z,1,r)) by PDIFF_1:def 5, P12

        .= <*r, t0*> by AS3, FINSEQ_7: 13, P12;

        

         P15: (( reproj (1,z)) . s) in ( dom u) by P12, P14, AS1, AS3;

        s in ( dom ( reproj (1,z))) by P13, FUNCT_2:def 1;

        hence s in ( dom (u * ( reproj (1,z)))) by P15, FUNCT_1: 11;

      end;

      then

       P2: ( dom (u * ( reproj (1,z)))) = ( dom f) by TARSKI: 2;

      

       P31: for s be object holds (s in ( dom (u * ( reproj (2,z)))) iff s in ( dom g))

      proof

        let s be object;

        hereby

          assume

           P10: s in ( dom (u * ( reproj (2,z))));

          then

          reconsider r = s as Real;

          

           A4: r is Element of REAL by XREAL_0:def 1;

          (( reproj (2,z)) . r) = ( Replace (z,2,r)) by PDIFF_1:def 5, A4

          .= <*x0, r*> by AS3, FINSEQ_7: 14, A4;

          then <*x0, r*> in { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } by P10, FUNCT_1: 11, AS1;

          then ex x,t be Real st <*x0, r*> = <*x, t*> & x in ( dom f) & t in ( dom g);

          hence s in ( dom g) by FINSEQ_1: 77;

        end;

        assume

         P12: s in ( dom g);

        then

        reconsider r = s as Real;

        

         P14: (( reproj (2,z)) . r) = ( Replace (z,2,r)) by PDIFF_1:def 5, P12

        .= <*x0, r*> by AS3, FINSEQ_7: 14, P12;

        

         P15: <*x0, r*> in { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } by P12, AS3;

        s in REAL by P12;

        then s in ( dom ( reproj (2,z))) by FUNCT_2:def 1;

        hence s in ( dom (u * ( reproj (2,z)))) by P15, P14, AS1, FUNCT_1: 11;

      end;

      

       P4: ( dom ((g /. t0) (#) f)) = ( dom f) by VALUED_1:def 5;

      

       P5: ( dom ((f /. x0) (#) g)) = ( dom g) by VALUED_1:def 5;

      for s be object st s in ( dom (u * ( reproj (1,z)))) holds ((u * ( reproj (1,z))) . s) = (((g /. t0) (#) f) . s)

      proof

        let s be object;

        assume

         A1: s in ( dom (u * ( reproj (1,z))));

        then

        reconsider r = s as Real;

        

         A3: <*r, t0*> in ( dom u) by P2, A1, AS3, AS1;

        

         A4a: r is Element of REAL by XREAL_0:def 1;

        

        thus ((u * ( reproj (1,z))) . s) = (u . (( reproj (1,z)) . r)) by FUNCT_1: 12, A1

        .= (u . ( Replace (z,1,r))) by PDIFF_1:def 5, A4a

        .= (u . <*r, t0*>) by AS3, FINSEQ_7: 13, A4a

        .= (u /. <*r, t0*>) by A3, PARTFUN1:def 6

        .= ((f /. r) * (g /. t0)) by A1, AS3, AS2, P21

        .= ((f . r) * (g /. t0)) by PARTFUN1:def 6, A1, P21

        .= (((g /. t0) (#) f) . s) by VALUED_1:def 5, A1, P21, P4;

      end;

      hence (u * ( reproj (1,z))) = ((g /. t0) (#) f) by FUNCT_1: 2, P21, TARSKI: 2, P4;

      for s be object st s in ( dom (u * ( reproj (2,z)))) holds ((u * ( reproj (2,z))) . s) = (((f /. x0) (#) g) . s)

      proof

        let s be object;

        assume

         A1: s in ( dom (u * ( reproj (2,z))));

        then

        reconsider r = s as Real;

        s in ( dom g) by P31, A1;

        then

         A3: <*x0, r*> in ( dom u) by AS3, AS1;

        

         A4a: r is Element of REAL by XREAL_0:def 1;

        

        thus ((u * ( reproj (2,z))) . s) = (u . (( reproj (2,z)) . r)) by FUNCT_1: 12, A1

        .= (u . ( Replace (z,2,r))) by PDIFF_1:def 5, A4a

        .= (u . <*x0, r*>) by AS3, FINSEQ_7: 14, A4a

        .= (u /. <*x0, r*>) by A3, PARTFUN1:def 6

        .= ((f /. x0) * (g /. r)) by P31, A1, AS3, AS2

        .= ((g . r) * (f /. x0)) by PARTFUN1:def 6, P31, A1

        .= (((f /. x0) (#) g) . s) by VALUED_1:def 5, P31, A1, P5;

      end;

      hence (u * ( reproj (2,z))) = ((f /. x0) (#) g) by FUNCT_1: 2, P31, TARSKI: 2, P5;

    end;

    theorem :: PDIFFEQ1:9

    for f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL , x0,t0 be Real, z be Element of ( REAL 2) st x0 in ( dom f) & t0 in ( dom g) & z = <*x0, t0*> & ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } & f is_differentiable_in x0 & (for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t))) holds u is_partial_differentiable_in (z,1) & ( partdiff (u,z,1)) = (( diff (f,x0)) * (g /. t0))

    proof

      let f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL , x0,t0 be Real, z be Element of ( REAL 2);

      assume that

       A0: x0 in ( dom f) & t0 in ( dom g) & z = <*x0, t0*> and

       A4: ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } and

       A5: f is_differentiable_in x0 and

       A7: for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t));

      

       P51: (u * ( reproj (1,z))) = ((g /. t0) (#) f) by LM11, A0, A4, A7;

      (( proj (1,2)) . z) = x0 by A0, LM03;

      hence u is_partial_differentiable_in (z,1) by A5, FDIFF_1: 15, P51;

      

      thus ( partdiff (u,z,1)) = ( diff (((g /. t0) (#) f),x0)) by A0, LM03, P51

      .= (( diff (f,x0)) * (g /. t0)) by A5, FDIFF_1: 15;

    end;

    theorem :: PDIFFEQ1:10

    for f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL , x0,t0 be Real, z be Element of ( REAL 2) st x0 in ( dom f) & t0 in ( dom g) & z = <*x0, t0*> & ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } & g is_differentiable_in t0 & (for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t))) holds u is_partial_differentiable_in (z,2) & ( partdiff (u,z,2)) = ((f /. x0) * ( diff (g,t0)))

    proof

      let f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL , x0,t0 be Real, z be Element of ( REAL 2);

      assume that

       A0: x0 in ( dom f) & t0 in ( dom g) & z = <*x0, t0*> and

       A4: ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } and

       A5: g is_differentiable_in t0 and

       A7: for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t));

      

       P52: (( proj (2,2)) . z) = t0 by A0, LM03;

      ((f /. x0) (#) g) is_differentiable_in t0 by A5, FDIFF_1: 15;

      hence u is_partial_differentiable_in (z,2) by LM11, A0, A4, A7, P52;

      

      thus ( partdiff (u,z,2)) = ( diff (((f /. x0) (#) g),t0)) by A0, LM11, A4, A7, P52

      .= ((f /. x0) * ( diff (g,t0))) by A5, FDIFF_1: 15;

    end;

    theorem :: PDIFFEQ1:11

    

     LM20: for X,T be Subset of REAL , Z be Subset of ( REAL 2), f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL st X c= ( dom f) & T c= ( dom g) & X is open & T is open & Z is open & Z = { <*x, t*> where x,t be Real : x in X & t in T } & ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } & f is_differentiable_on X & g is_differentiable_on T & (for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t))) holds u is_partial_differentiable_on (Z, <*1*>) & (for x,t be Real st x in X & t in T holds ((u `partial| (Z, <*1*>)) /. <*x, t*>) = (( diff (f,x)) * (g /. t))) & u is_partial_differentiable_on (Z, <*2*>) & (for x,t be Real st x in X & t in T holds ((u `partial| (Z, <*2*>)) /. <*x, t*>) = ((f /. x) * ( diff (g,t))))

    proof

      let X,T be Subset of REAL , Z be Subset of ( REAL 2), f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL ;

      assume that

       A1: X c= ( dom f) & T c= ( dom g) and

       A2: X is open & T is open & Z is open and

       A3: Z = { <*x, t*> where x,t be Real : x in X & t in T } and

       A4: ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } and

       A5: f is_differentiable_on X and

       A6: g is_differentiable_on T and

       A7: for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t));

      

       A8: Z c= ( dom u)

      proof

        let z be object;

        assume z in Z;

        then

        consider x,t be Real such that

         A80: z = <*x, t*> & x in X & t in T by A3;

        thus z in ( dom u) by A80, A1, A4;

      end;

      for z be Element of ( REAL 2) st z in Z holds u is_partial_differentiable_in (z,1)

      proof

        let z be Element of ( REAL 2);

        assume z in Z;

        then

        consider x,t be Real such that

         P01: z = <*x, t*> & x in X & t in T by A3;

        

         P51: (u * ( reproj (1,z))) = ((g /. t) (#) f) by A1, P01, LM11, A4, A7;

        

         P52: (( proj (1,2)) . z) = x by P01, LM03;

        f is_differentiable_in x by P01, A2, A5, FDIFF_1: 9;

        hence u is_partial_differentiable_in (z,1) by P51, P52, FDIFF_1: 15;

      end;

      then

       P1: u is_partial_differentiable_on (Z,1) by A2, A8, PDIFF_9: 60;

      hence u is_partial_differentiable_on (Z, <*1*>);

      

       P3: (u `partial| (Z, <*1*>)) = (u `partial| (Z,1)) by A2, PDIFF_9: 82, P1;

      

       P5: for x,t be Real, z be Element of ( REAL 2) st x in X & t in T & z = <*x, t*> holds ( partdiff (u,z,1)) = (( diff (f,x)) * (g /. t))

      proof

        let x,t be Real, z be Element of ( REAL 2);

        assume

         P50: x in X & t in T & z = <*x, t*>;

        then

         P51: (u * ( reproj (1,z))) = ((g /. t) (#) f) by A1, LM11, A4, A7;

        

         P52: (( proj (1,2)) . z) = x by P50, LM03;

        f is_differentiable_in x by P50, A2, A5, FDIFF_1: 9;

        hence thesis by P51, P52, FDIFF_1: 15;

      end;

      thus for x,t be Real st x in X & t in T holds ((u `partial| (Z, <*1*>)) /. <*x, t*>) = (( diff (f,x)) * (g /. t))

      proof

        let x,t be Real;

        assume

         P6: x in X & t in T;

        reconsider z = <*x, t*> as Element of ( REAL 2) by LM02;

         <*x, t*> in Z by A3, P6;

        

        hence ((u `partial| (Z, <*1*>)) /. <*x, t*>) = ( partdiff (u,z,1)) by P3, PDIFF_9:def 6, P1

        .= (( diff (f,x)) * (g /. t)) by P5, P6;

      end;

      for z be Element of ( REAL 2) st z in Z holds u is_partial_differentiable_in (z,2)

      proof

        let z be Element of ( REAL 2);

        assume z in Z;

        then

        consider x,t be Real such that

         P01: z = <*x, t*> & x in X & t in T by A3;

        

         P51: (u * ( reproj (2,z))) = ((f /. x) (#) g) by A1, LM11, P01, A4, A7;

        

         P52: (( proj (2,2)) . z) = t by P01, LM03;

        g is_differentiable_in t by P01, A2, A6, FDIFF_1: 9;

        hence u is_partial_differentiable_in (z,2) by FDIFF_1: 15, P51, P52;

      end;

      then

       P1: u is_partial_differentiable_on (Z,2) by A2, A8, PDIFF_9: 60;

      hence u is_partial_differentiable_on (Z, <*2*>);

      

       P3: (u `partial| (Z, <*2*>)) = (u `partial| (Z,2)) by A2, PDIFF_9: 82, P1;

      

       P5: for x,t be Real, z be Element of ( REAL 2) st x in X & t in T & z = <*x, t*> holds ( partdiff (u,z,2)) = ((f /. x) * ( diff (g,t)))

      proof

        let x,t be Real, z be Element of ( REAL 2);

        assume

         P50: x in X & t in T & z = <*x, t*>;

        then

         P51: (u * ( reproj (2,z))) = ((f /. x) (#) g) by A1, LM11, A4, A7;

        

         P52: (( proj (2,2)) . z) = t by P50, LM03;

        g is_differentiable_in t by P50, A2, A6, FDIFF_1: 9;

        hence thesis by FDIFF_1: 15, P51, P52;

      end;

      let x,t be Real;

      assume

       P6: x in X & t in T;

      reconsider z = <*x, t*> as Element of ( REAL 2) by LM02;

       <*x, t*> in Z by A3, P6;

      

      hence ((u `partial| (Z, <*2*>)) /. <*x, t*>) = ( partdiff (u,z,2)) by P3, PDIFF_9:def 6, P1

      .= ((f /. x) * ( diff (g,t))) by P5, P6;

    end;

    theorem :: PDIFFEQ1:12

    

     LM30: for X,T be Subset of REAL , Z be Subset of ( REAL 2), f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL st X c= ( dom f) & T c= ( dom g) & X is open & T is open & Z is open & Z = { <*x, t*> where x,t be Real : x in X & t in T } & ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } & f is_differentiable_on (2,X) & g is_differentiable_on (2,T) & (for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t))) holds u is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & (for x,t be Real st x in X & t in T holds ((u `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>) = (((( diff (f,X)) . 2) /. x) * (g /. t))) & u is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st x in X & t in T holds ((u `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((f /. x) * ((( diff (g,T)) . 2) /. t)))

    proof

      let X,T be Subset of REAL , Z be Subset of ( REAL 2), f be PartFunc of REAL , REAL , g be PartFunc of REAL , REAL , u be PartFunc of ( REAL 2), REAL ;

      assume that

       A1: X c= ( dom f) & T c= ( dom g) and

       A2: X is open & T is open & Z is open and

       A3: Z = { <*x, t*> where x,t be Real : x in X & t in T } and

       A4: ( dom u) = { <*x, t*> where x,t be Real : x in ( dom f) & t in ( dom g) } and

       A5: f is_differentiable_on (2,X) and

       A6: g is_differentiable_on (2,T) and

       A7: for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t));

      (( diff (f,X)) . 0 ) is_differentiable_on X by A5;

      then

       D6: (f | X) is_differentiable_on X by TAYLOR_1:def 5;

      then

       B50: X c= ( dom (f | X)) & (for x be Real st x in X holds ((f | X) | X) is_differentiable_in x) by FDIFF_1:def 6;

      

       B51: ((f | X) | X) = (f | X) by RELAT_1: 72;

      then

       B5: f is_differentiable_on X by B50, FDIFF_1:def 6, A1;

      (( diff (g,T)) . 0 ) is_differentiable_on T by A6;

      then

       C6: (g | T) is_differentiable_on T by TAYLOR_1:def 5;

      then

       B60: T c= ( dom (g | T)) & (for x be Real st x in T holds ((g | T) | T) is_differentiable_in x) by FDIFF_1:def 6;

      

       B61: ((g | T) | T) = (g | T) by RELAT_1: 72;

      then

       B6: g is_differentiable_on T by B60, FDIFF_1:def 6, A1;

      

       B7: u is_partial_differentiable_on (Z, <*1*>) & (for x,t be Real st x in X & t in T holds ((u `partial| (Z, <*1*>)) /. <*x, t*>) = (( diff (f,x)) * (g /. t))) & u is_partial_differentiable_on (Z, <*2*>) & (for x,t be Real st x in X & t in T holds ((u `partial| (Z, <*2*>)) /. <*x, t*>) = ((f /. x) * ( diff (g,t)))) by LM20, A1, A2, A3, A4, B5, B6, A7;

      

       C0: u is_partial_differentiable_on (Z,1) by LM20, A1, A3, A4, B5, B6, A7, A2;

      

       C1: X = ( dom (f `| X)) by FDIFF_1:def 7, B5;

      

       C3: T = ( dom (g | T)) by A1, RELAT_1: 62;

      (u `partial| (Z, <*1*>)) = (u `partial| (Z,1)) by C0, PDIFF_9: 82, A2;

      then

       C4: ( dom (u `partial| (Z, <*1*>))) = { <*x, t*> where x,t be Real : x in ( dom (f `| X)) & t in ( dom (g | T)) } by PDIFF_9:def 6, C0, C1, A3, C3;

      

       X5: (( diff (f,X)) . ( 0 + 1)) = ((( diff (f,X)) . 0 ) `| X) by TAYLOR_1:def 5

      .= ((f | X) `| X) by TAYLOR_1:def 5

      .= (f `| X) by LM00, A1, A2, B51, B50, FDIFF_1:def 6;

      then

       C5: (f `| X) is_differentiable_on X by A5;

      

       C7: for x,t be Real st x in ( dom (f `| X)) & t in ( dom (g | T)) holds ((u `partial| (Z, <*1*>)) /. <*x, t*>) = (((f `| X) /. x) * ((g | T) /. t))

      proof

        let x,t be Real;

        assume

         C70: x in ( dom (f `| X)) & t in ( dom (g | T));

        then

         C71: x in X & t in T by FDIFF_1:def 7, B5, A1, RELAT_1: 62;

        

         C72: ( diff (f,x)) = ((f `| X) . x) by C71, B5, FDIFF_1:def 7

        .= ((f `| X) /. x) by C70, PARTFUN1:def 6;

        ((g | T) /. t) = ((g | T) . t) by PARTFUN1:def 6, C70

        .= (g . t) by C70, C3, FUNCT_1: 49

        .= (g /. t) by PARTFUN1:def 6, C70, C3, A1;

        hence ((u `partial| (Z, <*1*>)) /. <*x, t*>) = (((f `| X) /. x) * ((g | T) /. t)) by LM20, A1, A2, A3, A4, B5, B6, A7, C71, C72;

      end;

      then (u `partial| (Z, <*1*>)) is_partial_differentiable_on (Z, <*1*>) & (for x,t be Real st x in X & t in T holds (((u `partial| (Z, <*1*>)) `partial| (Z, <*1*>)) /. <*x, t*>) = (( diff ((f `| X),x)) * ((g | T) /. t))) by LM20, A2, A3, C1, C3, C4, C5, C6;

      hence u is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) by B7, PDIFF_9: 80;

      thus for x,t be Real st x in X & t in T holds ((u `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>) = (((( diff (f,X)) . 2) /. x) * (g /. t))

      proof

        let x,t be Real;

        assume

         F1: x in X & t in T;

        then

         F2: (((u `partial| (Z, <*1*>)) `partial| (Z, <*1*>)) /. <*x, t*>) = (( diff ((f `| X),x)) * ((g | T) /. t)) by LM20, A2, A3, C1, C3, C4, C5, C6, C7;

        

         G3: x in ( dom ((f `| X) `| X)) by C5, F1, FDIFF_1:def 7;

        (( diff (f,X)) . (1 + 1)) = ((f `| X) `| X) by TAYLOR_1:def 5, X5;

        

        then

         F4: ((( diff (f,X)) . 2) /. x) = (((f `| X) `| X) . x) by G3, PARTFUN1:def 6

        .= ( diff ((f `| X),x)) by F1, C5, FDIFF_1:def 7;

        ((g | T) /. t) = ((g | T) . t) by PARTFUN1:def 6, F1, B60

        .= (g . t) by F1, FUNCT_1: 49

        .= (g /. t) by PARTFUN1:def 6, F1, A1;

        hence thesis by F2, PDIFF_9: 88, B7, F4;

      end;

      

       C0: u is_partial_differentiable_on (Z,2) by LM20, A1, A2, A3, A4, B5, B6, A7;

      

       C1: T = ( dom (g `| T)) by FDIFF_1:def 7, B6;

      

       C3: X = ( dom (f | X)) by A1, RELAT_1: 62;

      (u `partial| (Z, <*2*>)) = (u `partial| (Z,2)) by C0, PDIFF_9: 82, A2;

      then

       C4: ( dom (u `partial| (Z, <*2*>))) = { <*x, t*> where x,t be Real : x in ( dom (f | X)) & t in ( dom (g `| T)) } by PDIFF_9:def 6, C0, C1, A3, C3;

      

       X5: (( diff (g,T)) . ( 0 + 1)) = ((( diff (g,T)) . 0 ) `| T) by TAYLOR_1:def 5

      .= ((g | T) `| T) by TAYLOR_1:def 5

      .= (g `| T) by LM00, A1, A2, B60, B61, FDIFF_1:def 6;

      then

       C5: (g `| T) is_differentiable_on T by A6;

      

       C7: for x,t be Real st x in ( dom (f | X)) & t in ( dom (g `| T)) holds ((u `partial| (Z, <*2*>)) /. <*x, t*>) = (((f | X) /. x) * ((g `| T) /. t))

      proof

        let x,t be Real;

        assume

         C70: x in ( dom (f | X)) & t in ( dom (g `| T));

        then

         C71: x in X & t in T by FDIFF_1:def 7, B6, A1, RELAT_1: 62;

        

         C72: ( diff (g,t)) = ((g `| T) . t) by C71, B6, FDIFF_1:def 7

        .= ((g `| T) /. t) by C70, PARTFUN1:def 6;

        ((f | X) /. x) = ((f | X) . x) by PARTFUN1:def 6, C70

        .= (f . x) by C71, FUNCT_1: 49

        .= (f /. x) by PARTFUN1:def 6, C71, A1;

        hence ((u `partial| (Z, <*2*>)) /. <*x, t*>) = (((f | X) /. x) * ((g `| T) /. t)) by LM20, A1, A2, A3, A4, B5, B6, A7, C71, C72;

      end;

      then (u `partial| (Z, <*2*>)) is_partial_differentiable_on (Z, <*2*>) & (for x,t be Real st x in X & t in T holds (((u `partial| (Z, <*2*>)) `partial| (Z, <*2*>)) /. <*x, t*>) = (((f | X) /. x) * ( diff ((g `| T),t)))) by LM20, A2, A3, C1, C3, C4, C5, D6;

      hence u is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) by B7, PDIFF_9: 80;

      let x,t be Real;

      assume

       F1: x in X & t in T;

      

       F3: (u `partial| (Z,( <*2*> ^ <*2*>))) = ((u `partial| (Z, <*2*>)) `partial| (Z, <*2*>)) by PDIFF_9: 88, B7;

      

       G3: t in ( dom ((g `| T) `| T)) by C5, F1, FDIFF_1:def 7;

      (( diff (g,T)) . (1 + 1)) = ((g `| T) `| T) by TAYLOR_1:def 5, X5;

      

      then

       F4: ((( diff (g,T)) . 2) /. t) = (((g `| T) `| T) . t) by G3, PARTFUN1:def 6

      .= ( diff ((g `| T),t)) by F1, C5, FDIFF_1:def 7;

      ((f | X) /. x) = ((f | X) . x) by PARTFUN1:def 6, F1, B50

      .= (f . x) by F1, FUNCT_1: 49

      .= (f /. x) by PARTFUN1:def 6, F1, A1;

      hence thesis by F1, F3, F4, LM20, A2, A3, C1, C3, C4, C5, D6, C7;

    end;

    theorem :: PDIFFEQ1:13

    

     LM40: for f,g be Function of REAL , REAL , u be PartFunc of ( REAL 2), REAL , c be Real st f is_differentiable_on (2,( [#] REAL )) & g is_differentiable_on (2,( [#] REAL )) & ( dom u) = ( [#] ( REAL 2)) & (for x,t be Real holds (u /. <*x, t*>) = ((f /. x) * (g /. t))) & for x,t be Real holds ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t)) holds u is_partial_differentiable_on (( [#] ( REAL 2)),( <*1*> ^ <*1*>)) & (for x,t be Real st x in ( [#] REAL ) & t in ( [#] REAL ) holds ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = (((( diff (f,( [#] REAL ))) . 2) /. x) * (g /. t))) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*2*> ^ <*2*>)) & (for x,t be Real st x in ( [#] REAL ) & t in ( [#] REAL ) holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t))) & for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>))

    proof

      let f,g be Function of REAL , REAL , u be PartFunc of ( REAL 2), REAL , c be Real;

      assume that

       AS1: f is_differentiable_on (2,( [#] REAL )) and

       AS2: g is_differentiable_on (2,( [#] REAL )) and

       AS3: ( dom u) = ( [#] ( REAL 2)) and

       AS4: for x,t be Real holds (u /. <*x, t*>) = ((f /. x) * (g /. t)) and

       AS5: for x,t be Real holds ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t));

      

       P1: ( [#] REAL ) = ( dom f) & ( [#] REAL ) = ( dom g) by FUNCT_2:def 1;

      

       P4: for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t)) by AS4;

      for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>))

      proof

        let x,t be Real;

        

         X1: ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t)) by AS5;

        

         X3: x in ( [#] REAL ) & t in ( [#] REAL ) by XREAL_0:def 1;

        then ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = (((( diff (f,( [#] REAL ))) . 2) /. x) * (g /. t)) by LM30, AS1, AS2, AS3, P1, LMOP3, P4;

        hence thesis by LM30, AS1, AS2, AS3, P1, LMOP3, P4, X1, X3;

      end;

      hence thesis by LM30, AS1, AS2, AS3, P1, LMOP3, P4;

    end;

    

     LM410: for A,e be Real, f be PartFunc of REAL , REAL st f = (A (#) ( cos * (e (#) ( id ( [#] REAL ))))) holds f is_differentiable_on ( [#] REAL ) & for x be Real st x in ( [#] REAL ) holds ((f `| ( [#] REAL )) . x) = ( - ((A * e) * ( sin . (e * x))))

    proof

      let A,e be Real, f be PartFunc of REAL , REAL ;

      assume

       AS1: f = (A (#) ( cos * (e (#) ( id ( [#] REAL )))));

      reconsider Z = ( [#] REAL ) as open Subset of REAL ;

      reconsider E = (e (#) ( id ( [#] REAL ))) as Function of REAL , REAL ;

      

       P2: ( [#] REAL ) = ( dom E) & ( rng E) c= ( [#] REAL ) by FUNCT_2:def 1;

      

       P3: for x be Real st x in Z holds (E . x) = ((e * x) + 0 qua Real)

      proof

        let x be Real;

        assume

         AS2: x in Z;

        

        hence (E . x) = (e * (( id ( [#] REAL )) . x)) by VALUED_1:def 5, P2

        .= ((e * x) + 0 qua Real) by AS2, FUNCT_1: 18;

      end;

      

       P4: E is_differentiable_on Z & for x be Real st x in Z holds ((E `| Z) . x) = e by P2, P3, FDIFF_1: 23;

      

       P5: ( dom ( cos * E)) = ( [#] REAL ) by FUNCT_2:def 1;

      

       P6: ( dom (A (#) ( cos * E))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       P7: for x be Real st x in Z holds ( cos * E) is_differentiable_in x & ( diff (( cos * E),x)) = ( - (e * ( sin . (E . x))))

      proof

        let x be Real;

        assume

         P70: x in Z;

        then

         P71: E is_differentiable_in x by P4, FDIFF_1: 9;

        

         P73: cos is_differentiable_in (E . x) & ( diff ( cos ,(E . x))) = ( - ( sin . (E . x))) by SIN_COS: 63;

        

        then ( diff (( cos * E),x)) = (( - ( sin . (E . x))) * ( diff (E,x))) by FDIFF_2: 13, P71

        .= (( - ( sin . (E . x))) * ((E `| Z) . x)) by FDIFF_1:def 7, P4, P70

        .= (( - ( sin . (E . x))) * e) by P2, P3, FDIFF_1: 23, P70

        .= ( - (e * ( sin . (E . x))));

        hence thesis by P73, FDIFF_2: 13, P71;

      end;

      then for x be Real st x in Z holds ( cos * E) is_differentiable_in x;

      then

       P8: ( cos * E) is_differentiable_on Z by P5, FDIFF_1: 9;

      for x be Real st x in Z holds (((A (#) ( cos * E)) `| Z) . x) = ( - ((A * e) * ( sin . (e * x))))

      proof

        let x be Real;

        assume

         P90: x in Z;

        then

         P91: (E . x) = ((e * x) + 0 qua Real) by P3;

        

        thus (((A (#) ( cos * E)) `| Z) . x) = (A * ( diff (( cos * E),x))) by P90, P8, P6, FDIFF_1: 20

        .= (A * ( - (e * ( sin . (E . x))))) by P7, P90

        .= ( - ((A * e) * ( sin . (e * x)))) by P91;

      end;

      hence thesis by AS1, P8, P6, FDIFF_1: 20;

    end;

    

     LM411: for A,e be Real, f be PartFunc of REAL , REAL st f = (A (#) ( sin * (e (#) ( id ( [#] REAL ))))) holds f is_differentiable_on ( [#] REAL ) & for x be Real st x in ( [#] REAL ) holds ((f `| ( [#] REAL )) . x) = ((A * e) * ( cos . (e * x)))

    proof

      let A,e be Real, f be PartFunc of REAL , REAL ;

      assume

       AS1: f = (A (#) ( sin * (e (#) ( id ( [#] REAL )))));

      reconsider Z = ( [#] REAL ) as open Subset of REAL ;

      reconsider E = (e (#) ( id ( [#] REAL ))) as Function of REAL , REAL ;

      

       P2: ( [#] REAL ) = ( dom E) & ( rng E) c= ( [#] REAL ) by FUNCT_2:def 1;

      

       P3: for x be Real st x in Z holds (E . x) = ((e * x) + 0 qua Real)

      proof

        let x be Real;

        assume

         AS2: x in Z;

        

        hence (E . x) = (e * (( id ( [#] REAL )) . x)) by VALUED_1:def 5, P2

        .= ((e * x) + 0 qua Real) by AS2, FUNCT_1: 18;

      end;

      

       P4: E is_differentiable_on Z & for x be Real st x in Z holds ((E `| Z) . x) = e by P2, P3, FDIFF_1: 23;

      

       P5: ( dom ( sin * E)) = ( [#] REAL ) by FUNCT_2:def 1;

      

       P6: ( dom (A (#) ( sin * E))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       P7: for x be Real st x in Z holds ( sin * E) is_differentiable_in x & ( diff (( sin * E),x)) = (e * ( cos . (E . x)))

      proof

        let x be Real;

        assume

         P70: x in Z;

        then

         P71: E is_differentiable_in x by P4, FDIFF_1: 9;

        

         P73: sin is_differentiable_in (E . x) & ( diff ( sin ,(E . x))) = ( cos . (E . x)) by SIN_COS: 64;

        

        then ( diff (( sin * E),x)) = (( cos . (E . x)) * ( diff (E,x))) by FDIFF_2: 13, P71

        .= (( cos . (E . x)) * ((E `| Z) . x)) by FDIFF_1:def 7, P4, P70

        .= (e * ( cos . (E . x))) by P2, P3, FDIFF_1: 23, P70;

        hence thesis by P73, FDIFF_2: 13, P71;

      end;

      then for x be Real st x in Z holds ( sin * E) is_differentiable_in x;

      then

       P8: ( sin * E) is_differentiable_on Z by P5, FDIFF_1: 9;

      for x be Real st x in Z holds (((A (#) ( sin * E)) `| Z) . x) = ((A * e) * ( cos . (e * x)))

      proof

        let x be Real;

        assume

         P90: x in Z;

        then

         P91: (E . x) = ((e * x) + 0 qua Real) by P3;

        

        thus (((A (#) ( sin * E)) `| Z) . x) = (A * ( diff (( sin * E),x))) by P90, P8, P6, FDIFF_1: 20

        .= (A * (e * ( cos . (E . x)))) by P7, P90

        .= ((A * e) * ( cos . (e * x))) by P91;

      end;

      hence thesis by AS1, P8, P6, FDIFF_1: 20;

    end;

    theorem :: PDIFFEQ1:14

    

     LM412: for A,B,e be Real, f be Function of REAL , REAL st for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) holds f is_differentiable_on ( [#] REAL ) & for x be Real holds ((f `| ( [#] REAL )) . x) = ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x))))))

    proof

      let A,B,e be Real, f be Function of REAL , REAL ;

      assume

       AS1: for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x))));

      reconsider f1 = (A (#) ( cos * (e (#) ( id ( [#] REAL ))))), f2 = (B (#) ( sin * (e (#) ( id ( [#] REAL ))))) as PartFunc of REAL , REAL ;

      reconsider Z = ( [#] REAL ) as open Subset of REAL ;

      reconsider E = (e (#) ( id ( [#] REAL ))) as Function of REAL , REAL ;

      

       P00: ( [#] REAL ) = ( dom E) & ( rng E) c= ( [#] REAL ) by FUNCT_2:def 1;

      

       E01: for x be Real st x in Z holds (E . x) = (e * x)

      proof

        let x be Real;

        assume

         AS2: x in Z;

        

        hence (E . x) = (e * (( id ( [#] REAL )) . x)) by VALUED_1:def 5, P00

        .= (e * x) by AS2, FUNCT_1: 18;

      end;

      

       P4: ( dom (f1 + f2)) = Z by FUNCT_2:def 1;

      

       P01: ( dom f1) = Z by FUNCT_2:def 1;

      ( dom f2) = Z by FUNCT_2:def 1;

      then

       P6: ( dom f) = (( dom f1) /\ ( dom f2)) by FUNCT_2:def 1, P01;

      for x be object st x in ( dom f) holds (f . x) = ((f1 . x) + (f2 . x))

      proof

        let x be object;

        assume

         P50: x in ( dom f);

        then

        reconsider r = x as Real;

        

        thus (f . x) = ((A * ( cos . (e * r))) + (B * ( sin . (e * r)))) by AS1

        .= ((A * ( cos . (E . r))) + (B * ( sin . (e * r)))) by E01, P50

        .= ((A * ( cos . (E . r))) + (B * ( sin . (E . r)))) by E01, P50

        .= ((A * (( cos * E) . r)) + (B * ( sin . (E . r)))) by FUNCT_1: 13, P50, P00

        .= ((A * (( cos * E) . r)) + (B * (( sin * E) . r))) by FUNCT_1: 13, P50, P00

        .= ((f1 . r) + (B * (( sin * E) . r))) by VALUED_1: 6

        .= ((f1 . x) + (f2 . x)) by VALUED_1: 6;

      end;

      then

       P1: f = (f1 + f2) by P6, VALUED_1:def 1;

      

       P2: f1 is_differentiable_on ( [#] REAL ) & for x be Real st x in ( [#] REAL ) holds ((f1 `| ( [#] REAL )) . x) = ( - ((A * e) * ( sin . (e * x)))) by LM410;

      

       P3: f2 is_differentiable_on ( [#] REAL ) & for x be Real st x in ( [#] REAL ) holds ((f2 `| ( [#] REAL )) . x) = ((B * e) * ( cos . (e * x))) by LM411;

      for x be Real holds ((f `| ( [#] REAL )) . x) = ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x))))))

      proof

        let x be Real;

        

         P60: x in Z by XREAL_0:def 1;

        ((f `| Z) . x) = (( diff (f1,x)) + ( diff (f2,x))) by XREAL_0:def 1, FDIFF_1: 18, P1, P2, P3, P4

        .= (((f1 `| ( [#] REAL )) . x) + ( diff (f2,x))) by P2, P60, FDIFF_1:def 7

        .= (((f1 `| ( [#] REAL )) . x) + ((f2 `| ( [#] REAL )) . x)) by P3, P60, FDIFF_1:def 7

        .= (( - ((e * A) * ( sin . (e * x)))) + ((f2 `| ( [#] REAL )) . x)) by LM410, XREAL_0:def 1

        .= (( - (e * (A * ( sin . (e * x))))) + ((B * e) * ( cos . (e * x)))) by LM411, XREAL_0:def 1

        .= ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x))))));

        hence thesis;

      end;

      hence thesis by FDIFF_1: 18, P1, P2, P3, P4;

    end;

    begin

    theorem :: PDIFFEQ1:15

    

     LM41: for A,B,e be Real, f be Function of REAL , REAL st for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) holds f is_differentiable_on (2,( [#] REAL )) & for x be Real holds ((f `| ( [#] REAL )) . x) = ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x)))))) & (((f `| ( [#] REAL )) `| ( [#] REAL )) . x) = ( - ((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))))) & (((( diff (f,( [#] REAL ))) . 2) /. x) + ((e ^2 ) * (f /. x))) = 0

    proof

      let A,B,e be Real, f be Function of REAL , REAL ;

      assume

       AS1: for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x))));

      then

       P1: f is_differentiable_on ( [#] REAL ) & for x be Real holds ((f `| ( [#] REAL )) . x) = ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x)))))) by LM412;

      

       P2: for x be Real holds ((f `| ( [#] REAL )) . x) = (((e * B) * ( cos . (e * x))) + (( - (e * A)) * ( sin . (e * x))))

      proof

        let x be Real;

        

        thus ((f `| ( [#] REAL )) . x) = ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x)))))) by AS1, LM412

        .= (((e * B) * ( cos . (e * x))) + (( - (e * A)) * ( sin . (e * x))));

      end;

      

       P4: ( rng (f `| ( [#] REAL ))) c= REAL ;

      

       D0: ( dom f) = REAL by FUNCT_2:def 1;

      ( dom (f `| ( [#] REAL ))) = ( [#] REAL ) by FDIFF_1:def 7, P1;

      then

       P30: (f `| ( [#] REAL )) is Function of REAL , REAL by P4, FUNCT_2: 2;

      

       X1: for i be Nat st i <= (2 - 1) holds (( diff (f,( [#] REAL ))) . i) is_differentiable_on ( [#] REAL )

      proof

        let i be Nat;

        assume i <= (2 - 1);

        then i <= ( 0 + 1);

        per cases by NAT_1: 8;

          suppose i = 0 ;

          

          then (( diff (f,( [#] REAL ))) . i) = (f | ( [#] REAL )) by TAYLOR_1:def 5

          .= f by D0, RELAT_1: 69;

          hence (( diff (f,( [#] REAL ))) . i) is_differentiable_on ( [#] REAL ) by AS1, LM412;

        end;

          suppose i = 1;

          

          then (( diff (f,( [#] REAL ))) . i) = (( diff (f,( [#] REAL ))) . ( 0 + 1))

          .= ((( diff (f,( [#] REAL ))) . 0 ) `| ( [#] REAL )) by TAYLOR_1:def 5

          .= ((f | ( [#] REAL )) `| ( [#] REAL )) by TAYLOR_1:def 5

          .= (f `| ( [#] REAL )) by D0, RELAT_1: 69;

          hence (( diff (f,( [#] REAL ))) . i) is_differentiable_on ( [#] REAL ) by P30, LM412, P2;

        end;

      end;

      hence f is_differentiable_on (2,( [#] REAL ));

      let x be Real;

      thus ((f `| ( [#] REAL )) . x) = ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x)))))) by AS1, LM412;

      

      thus

       P90: (((f `| ( [#] REAL )) `| ( [#] REAL )) . x) = ( - (e * (((e * B) * ( sin . (e * x))) - (( - (e * A)) * ( cos . (e * x)))))) by P30, LM412, P2

      .= ( - ((e * e) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))))

      .= ( - ((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))))) by SQUARE_1:def 1;

      

       P92: (( diff (f,( [#] REAL ))) . (1 + 1)) = ((( diff (f,( [#] REAL ))) . 1) `| ( [#] REAL )) by TAYLOR_1:def 5;

      

       P93: (( diff (f,( [#] REAL ))) . 1) = (( diff (f,( [#] REAL ))) . ( 0 + 1))

      .= ((( diff (f,( [#] REAL ))) . 0 ) `| ( [#] REAL )) by TAYLOR_1:def 5

      .= ((f | ( [#] REAL )) `| ( [#] REAL )) by TAYLOR_1:def 5

      .= (f `| ( [#] REAL )) by D0, RELAT_1: 69;

      (( diff (f,( [#] REAL ))) . 1) is_differentiable_on ( [#] REAL ) by X1;

      then ( dom (( diff (f,( [#] REAL ))) . 2)) = ( [#] REAL ) by P92, FDIFF_1:def 7;

      then

       P91: ((( diff (f,( [#] REAL ))) . 2) /. x) = ( - ((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))))) by XREAL_0:def 1, PARTFUN1:def 6, P92, P93, P90;

      (f /. x) = (f . x) by D0, XREAL_0:def 1, PARTFUN1:def 6;

      then ((e ^2 ) * (f /. x)) = ((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) by AS1;

      hence thesis by P91;

    end;

    theorem :: PDIFFEQ1:16

    

     LM42: for A,B,e be Real holds ex f be Function of REAL , REAL st for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))

    proof

      let A,B,e be Real;

      defpred P[ object, object] means ex t be Real st $1 = t & $2 = ((A * ( cos . (e * t))) + (B * ( sin . (e * t))));

      

       A0: for x be object st x in REAL holds ex y be object st y in REAL & P[x, y]

      proof

        let x be object;

        assume x in REAL ;

        then

        reconsider t = x as Real;

        ((A * ( cos . (e * t))) + (B * ( sin . (e * t)))) in REAL by XREAL_0:def 1;

        hence thesis;

      end;

      consider f be Function of REAL , REAL such that

       A1: for x be object st x in REAL holds P[x, (f . x)] from FUNCT_2:sch 1( A0);

      take f;

      let x be Real;

      ex t be Real st x = t & (f . x) = ((A * ( cos . (e * t))) + (B * ( sin . (e * t)))) by XREAL_0:def 1, A1;

      hence thesis;

    end;

    theorem :: PDIFFEQ1:17

    

     LM43: for A,B,C,d,c,e be Real, f,g be Function of REAL , REAL st (for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) & (for t be Real holds (g . t) = ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))) holds for x,t be Real holds ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t))

    proof

      let A,B,C,d,c,e be Real, f,g be Function of REAL , REAL ;

      assume

       AS: (for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) & (for t be Real holds (g . t) = ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))));

      let x,t be Real;

      (((( diff (f,( [#] REAL ))) . 2) /. x) + ((e ^2 ) * (f /. x))) = 0 by AS, LM41;

      

      then

       Q3: (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t)) = (((c ^2 ) * ( - ((e ^2 ) * (f /. x)))) * (g /. t))

      .= ( - ((((c ^2 ) * (e ^2 )) * (f /. x)) * (g /. t)));

      (((( diff (g,( [#] REAL ))) . 2) /. t) + (((e * c) ^2 ) * (g /. t))) = 0 by AS, LM41;

      

      then ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = ((f /. x) * ( - (((e * c) ^2 ) * (g /. t))))

      .= ((f /. x) * ( - (((e * c) * (e * c)) * (g /. t)))) by SQUARE_1:def 1

      .= ((f /. x) * ( - (((e * e) * (c * c)) * (g /. t))))

      .= ((f /. x) * ( - (((e ^2 ) * (c * c)) * (g /. t)))) by SQUARE_1:def 1

      .= ((f /. x) * ( - (((e ^2 ) * (c ^2 )) * (g /. t)))) by SQUARE_1:def 1

      .= ( - ((((c ^2 ) * (e ^2 )) * (f /. x)) * (g /. t)));

      hence thesis by Q3;

    end;

    theorem :: PDIFFEQ1:18

    

     LM50: for f,g be Function of REAL , REAL , u be Function of ( REAL 2), REAL st f is_differentiable_on (2,( [#] REAL )) & g is_differentiable_on (2,( [#] REAL )) & (for x,t be Real holds ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t))) & (for x,t be Real holds (u /. <*x, t*>) = ((f /. x) * (g /. t))) holds u is_partial_differentiable_on (( [#] ( REAL 2)), <*1*>) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = (( diff (f,x)) * (g /. t))) & u is_partial_differentiable_on (( [#] ( REAL 2)), <*2*>) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*2*>)) /. <*x, t*>) = ((f /. x) * ( diff (g,t)))) & f is_differentiable_on (2,( [#] REAL )) & g is_differentiable_on (2,( [#] REAL )) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*1*> ^ <*1*>)) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = (((( diff (f,( [#] REAL ))) . 2) /. x) * (g /. t))) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*2*> ^ <*2*>)) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t))) & for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>))

    proof

      let f,g be Function of REAL , REAL , u be Function of ( REAL 2), REAL ;

      assume that

       XP1: f is_differentiable_on (2,( [#] REAL )) and

       XP2: g is_differentiable_on (2,( [#] REAL )) and

       XP3: for x,t be Real holds ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t)) and

       AS4: for x,t be Real holds (u /. <*x, t*>) = ((f /. x) * (g /. t));

      

       P0: ( dom u) = ( [#] ( REAL 2)) by FUNCT_2:def 1;

      

       P1: ( [#] REAL ) = ( dom f) & ( [#] REAL ) = ( dom g) by FUNCT_2:def 1;

      

       P4: for x,t be Real st x in ( dom f) & t in ( dom g) holds (u /. <*x, t*>) = ((f /. x) * (g /. t)) by AS4;

      (( diff (f,( [#] REAL ))) . 0 ) is_differentiable_on ( [#] REAL ) by XP1;

      then (f | ( [#] REAL )) is_differentiable_on ( [#] REAL ) by TAYLOR_1:def 5;

      then

       B50: ( [#] REAL ) c= ( dom (f | ( [#] REAL ))) & (for x be Real st x in ( [#] REAL ) holds ((f | ( [#] REAL )) | ( [#] REAL )) is_differentiable_in x) by FDIFF_1:def 6;

      ((f | ( [#] REAL )) | ( [#] REAL )) = (f | ( [#] REAL )) by RELAT_1: 72;

      then

       Q1: f is_differentiable_on ( [#] REAL ) by B50, FDIFF_1:def 6, P1;

      (( diff (g,( [#] REAL ))) . 0 ) is_differentiable_on ( [#] REAL ) by XP2;

      then (g | ( [#] REAL )) is_differentiable_on ( [#] REAL ) by TAYLOR_1:def 5;

      then

       B50: ( [#] REAL ) c= ( dom (g | ( [#] REAL ))) & (for x be Real st x in ( [#] REAL ) holds ((g | ( [#] REAL )) | ( [#] REAL )) is_differentiable_in x) by FDIFF_1:def 6;

      ((g | ( [#] REAL )) | ( [#] REAL )) = (g | ( [#] REAL )) by RELAT_1: 72;

      then

       Q2: g is_differentiable_on ( [#] REAL ) by B50, FDIFF_1:def 6, P1;

      

       Y1: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = (( diff (f,x)) * (g /. t))

      proof

        let x,t be Real;

        x in ( [#] REAL ) & t in ( [#] REAL ) by XREAL_0:def 1;

        hence thesis by Q1, Q2, LM20, P4, P0, P1, LMOP3;

      end;

      

       Y2: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*2*>)) /. <*x, t*>) = ((f /. x) * ( diff (g,t)))

      proof

        let x,t be Real;

        x in ( [#] REAL ) & t in ( [#] REAL ) by XREAL_0:def 1;

        hence thesis by Q1, Q2, LM20, P4, P0, P1, LMOP3;

      end;

      

       Y3: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = (((( diff (f,( [#] REAL ))) . 2) /. x) * (g /. t))

      proof

        let x,t be Real;

        x in ( [#] REAL ) & t in ( [#] REAL ) by XREAL_0:def 1;

        hence thesis by LM40, AS4, P0, XP1, XP2, XP3;

      end;

      for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t))

      proof

        let x,t be Real;

        x in ( [#] REAL ) & t in ( [#] REAL ) by XREAL_0:def 1;

        hence thesis by LM40, AS4, P0, XP1, XP2, XP3;

      end;

      hence thesis by AS4, Q1, Q2, LM20, P4, P0, P1, LMOP3, Y1, Y2, Y3, XP1, XP2, XP3, LM40;

    end;

    theorem :: PDIFFEQ1:19

    

     Th10: for A,B,C,d,e,c be Real, u be Function of ( REAL 2), REAL st for x,t be Real holds (u /. <*x, t*>) = (((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))) holds u is_partial_differentiable_on (( [#] ( REAL 2)), <*1*>) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = ((( - ((A * e) * ( sin . (e * x)))) + ((B * e) * ( cos . (e * x)))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))) & u is_partial_differentiable_on (( [#] ( REAL 2)), <*2*>) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*2*>)) /. <*x, t*>) = (((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) * (( - ((C * (e * c)) * ( sin . ((e * c) * t)))) + ((d * (e * c)) * ( cos . ((e * c) * t)))))) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*1*> ^ <*1*>)) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = ( - (((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*2*> ^ <*2*>)) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ( - ((((e * c) ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))))) & for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>))

    proof

      let A,B,C,d,e,c be Real, u be Function of ( REAL 2), REAL ;

      assume

       AS: for x,t be Real holds (u /. <*x, t*>) = (((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))));

      consider f be Function of REAL , REAL such that

       A1: for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) by LM42;

      consider g be Function of REAL , REAL such that

       A2: for t be Real holds (g . t) = ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))) by LM42;

      

       D0: ( dom f) = REAL & ( dom g) = REAL by FUNCT_2:def 1;

      

       A3: for x,t be Real holds (u /. <*x, t*>) = ((f /. x) * (g /. t))

      proof

        let x,t be Real;

        

         A31: (f /. x) = (f . x) by PARTFUN1:def 6, D0, XREAL_0:def 1

        .= ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) by A1;

        (g /. t) = (g . t) by PARTFUN1:def 6, D0, XREAL_0:def 1

        .= ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))) by A2;

        hence thesis by AS, A31;

      end;

      

       X1: f is_differentiable_on (2,( [#] REAL )) by LM41, A1;

      

       X2: g is_differentiable_on (2,( [#] REAL )) by LM41, A2;

      

       X3: for x,t be Real holds ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t)) by LM43, A1, A2;

      

       Y1: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = ((( - ((A * e) * ( sin . (e * x)))) + ((B * e) * ( cos . (e * x)))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))

      proof

        let x,t be Real;

        

         Y11: ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = (( diff (f,x)) * (g /. t)) by X1, X2, X3, LM50, A3;

        

         Y12: ((f `| ( [#] REAL )) . x) = ( - (e * ((A * ( sin . (e * x))) - (B * ( cos . (e * x)))))) by LM41, A1;

        

         Y13: f is_differentiable_on ( [#] REAL ) by D0, X1, DIFF2;

        

         Y14: x in ( [#] REAL ) by XREAL_0:def 1;

        (g /. t) = (g . t) by PARTFUN1:def 6, D0, XREAL_0:def 1

        .= ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))) by A2;

        hence thesis by Y11, Y12, Y13, Y14, FDIFF_1:def 7;

      end;

      

       Y2: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*2*>)) /. <*x, t*>) = (((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) * (( - ((C * (e * c)) * ( sin . ((e * c) * t)))) + ((d * (e * c)) * ( cos . ((e * c) * t)))))

      proof

        let x,t be Real;

        

         Y12: ((g `| ( [#] REAL )) . t) = ( - ((e * c) * ((C * ( sin . ((e * c) * t))) - (d * ( cos . ((e * c) * t)))))) by LM41, A2;

        

         Y13: g is_differentiable_on ( [#] REAL ) by D0, X2, DIFF2;

        t in ( [#] REAL ) by XREAL_0:def 1;

        then

         Y14: ( diff (g,t)) = ((g `| ( [#] REAL )) . t) by Y13, FDIFF_1:def 7;

        (f /. x) = (f . x) by PARTFUN1:def 6, D0, XREAL_0:def 1

        .= ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) by A1;

        hence thesis by X1, X2, X3, LM50, A3, Y12, Y14;

      end;

      

       Y3: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = ( - (((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))))

      proof

        let x,t be Real;

        

         Y11: ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = (((( diff (f,( [#] REAL ))) . 2) /. x) * (g /. t)) by X1, X2, X3, LM50, A3;

        

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

        

         R2: (f `| ( [#] REAL )) is_differentiable_on ( [#] REAL ) by R1, X1, DIFF2;

        x in ( [#] REAL ) by XREAL_0:def 1;

        then

         Y13: x in ( dom ((f `| ( [#] REAL )) `| ( [#] REAL ))) by R2, FDIFF_1:def 7;

        

         Y15: ((( diff (f,( [#] REAL ))) . 2) /. x) = (((f `| ( [#] REAL )) `| ( [#] REAL )) /. x) by D0, X1, DIFF2

        .= (((f `| ( [#] REAL )) `| ( [#] REAL )) . x) by Y13, PARTFUN1:def 6

        .= ( - ((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))))) by LM41, A1;

        (g /. t) = (g . t) by PARTFUN1:def 6, D0, XREAL_0:def 1

        .= ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))) by A2;

        hence thesis by Y11, Y15;

      end;

      for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ( - ((((e * c) ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))))

      proof

        let x,t be Real;

        

         Y11: ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) by X1, X2, X3, LM50, A3;

        

         R1: ( [#] REAL ) = ( dom g) by FUNCT_2:def 1;

        

         R2: (g `| ( [#] REAL )) is_differentiable_on ( [#] REAL ) by R1, X2, DIFF2;

        t in ( [#] REAL ) by XREAL_0:def 1;

        then

         Y13: t in ( dom ((g `| ( [#] REAL )) `| ( [#] REAL ))) by R2, FDIFF_1:def 7;

        

         Y15: ((( diff (g,( [#] REAL ))) . 2) /. t) = (((g `| ( [#] REAL )) `| ( [#] REAL )) /. t) by D0, X2, DIFF2

        .= (((g `| ( [#] REAL )) `| ( [#] REAL )) . t) by Y13, PARTFUN1:def 6

        .= ( - (((e * c) ^2 ) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))) by LM41, A2;

        (f /. x) = (f . x) by PARTFUN1:def 6, D0, XREAL_0:def 1

        .= ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) by A1;

        hence thesis by Y11, Y15;

      end;

      hence thesis by X1, X2, X3, LM50, A3, Y1, Y2, Y3;

    end;

    theorem :: PDIFFEQ1:20

    for c be Real holds ex u be PartFunc of ( REAL 2), REAL st u is_partial_differentiable_on (( [#] ( REAL 2)),( <*1*> ^ <*1*>)) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*2*> ^ <*2*>)) & for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>))

    proof

      let c be Real;

      set A = the Real;

      set B = the Real;

      set C = the Real;

      set D = the Real;

      set e = the Real;

      consider f be Function of REAL , REAL such that

       A1: for x be Real holds (f . x) = ((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) by LM42;

      consider g be Function of REAL , REAL such that

       A2: for t be Real holds (g . t) = ((C * ( cos . ((e * c) * t))) + (D * ( sin . ((e * c) * t)))) by LM42;

      

       F1: ( dom f) = ( [#] REAL ) & ( dom g) = ( [#] REAL ) by FUNCT_2:def 1;

      consider u be PartFunc of ( REAL 2), REAL such that

       F2: ( dom u) = { <*x, t*> where x,t be Real : x in ( [#] REAL ) & t in ( [#] REAL ) } & for x,t be Real st x in ( [#] REAL ) & t in ( [#] REAL ) holds (u /. <*x, t*>) = ((f /. x) * (g /. t)) by LM10, F1;

      u is total by PARTFUN1:def 2, F2, LMOP3;

      then

      reconsider u as Function of ( REAL 2), REAL ;

      take u;

      

       A3: for x,t be Real holds (u /. <*x, t*>) = ((f /. x) * (g /. t))

      proof

        let x,t be Real;

        x in ( [#] REAL ) & t in ( [#] REAL ) by XREAL_0:def 1;

        hence (u /. <*x, t*>) = ((f /. x) * (g /. t)) by F2;

      end;

      

       X1: f is_differentiable_on (2,( [#] REAL )) by LM41, A1;

      

       X2: g is_differentiable_on (2,( [#] REAL )) by LM41, A2;

      for x,t be Real holds ((f /. x) * ((( diff (g,( [#] REAL ))) . 2) /. t)) = (((c ^2 ) * ((( diff (f,( [#] REAL ))) . 2) /. x)) * (g /. t)) by LM43, A1, A2;

      hence u is_partial_differentiable_on (( [#] ( REAL 2)),( <*1*> ^ <*1*>)) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*2*> ^ <*2*>)) & for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>)) by X1, X2, LM50, A3;

    end;

    begin

    theorem :: PDIFFEQ1:21

    for C,d,c be Real, n be Nat, u be Function of ( REAL 2), REAL st for x,t be Real holds (u /. <*x, t*>) = (( sin . ((n * PI ) * x)) * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t))))) holds u is_partial_differentiable_on (( [#] ( REAL 2)), <*1*>) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = (((n * PI ) * ( cos . ((n * PI ) * x))) * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t)))))) & u is_partial_differentiable_on (( [#] ( REAL 2)), <*2*>) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*2*>)) /. <*x, t*>) = (( sin . ((n * PI ) * x)) * (( - ((C * ((n * PI ) * c)) * ( sin . (((n * PI ) * c) * t)))) + ((d * ((n * PI ) * c)) * ( cos . (((n * PI ) * c) * t)))))) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*1*> ^ <*1*>)) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = ( - ((((n * PI ) ^2 ) * ( sin . ((n * PI ) * x))) * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t)))))) & u is_partial_differentiable_on (( [#] ( REAL 2)),( <*2*> ^ <*2*>)) & (for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ( - (((((n * PI ) * c) ^2 ) * ( sin . ((n * PI ) * x))) * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t)))))))) & (for t be Real holds (u /. <* 0 , t*>) = 0 & (u /. <*1, t*>) = 0 ) & for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>))

    proof

      let C,d,c be Real, n be Nat, u be Function of ( REAL 2), REAL ;

      assume

       AS: for x,t be Real holds (u /. <*x, t*>) = (( sin . ((n * PI ) * x)) * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t)))));

      set A = 0 ;

      set B = 1;

      set e = (n * PI );

      

       AS1: for x,t be Real holds (u /. <*x, t*>) = (((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))) by AS;

      

       Y1: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = ((e * ( cos . (e * x))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))

      proof

        let x,t be Real;

        ((u `partial| (( [#] ( REAL 2)), <*1*>)) /. <*x, t*>) = ((( - ((A * e) * ( sin . (e * x)))) + ((B * e) * ( cos . (e * x)))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))) by AS1, Th10;

        hence thesis;

      end;

      

       Y2: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)), <*2*>)) /. <*x, t*>) = (( sin . (e * x)) * (( - ((C * (e * c)) * ( sin . ((e * c) * t)))) + ((d * (e * c)) * ( cos . ((e * c) * t)))))

      proof

        let x,t be Real;

        ((u `partial| (( [#] ( REAL 2)), <*2*>)) /. <*x, t*>) = (((A * ( cos . (e * x))) + (B * ( sin . (e * x)))) * (( - ((C * (e * c)) * ( sin . ((e * c) * t)))) + ((d * (e * c)) * ( cos . ((e * c) * t))))) by AS1, Th10;

        hence thesis;

      end;

      

       Y3: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = ( - (((e ^2 ) * ( sin . (e * x))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))))

      proof

        let x,t be Real;

        ((u `partial| (( [#] ( REAL 2)),( <*1*> ^ <*1*>))) /. <*x, t*>) = ( - (((e ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))) by AS1, Th10;

        hence thesis;

      end;

      

       Y4: for x,t be Real holds ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ( - ((((e * c) ^2 ) * ( sin . (e * x))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t))))))

      proof

        let x,t be Real;

        ((u `partial| (( [#] ( REAL 2)),( <*2*> ^ <*2*>))) /. <*x, t*>) = ( - ((((e * c) ^2 ) * ((A * ( cos . (e * x))) + (B * ( sin . (e * x))))) * ((C * ( cos . ((e * c) * t))) + (d * ( sin . ((e * c) * t)))))) by AS1, Th10;

        hence thesis;

      end;

      for t be Real holds (u /. <* 0 , t*>) = 0 & (u /. <*1, t*>) = 0

      proof

        let t be Real;

        

        thus (u /. <* 0 , t*>) = (( sin . ((n * PI ) * 0 )) * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t))))) by AS

        .= 0 by SIN_COS: 30;

        

        thus (u /. <*1, t*>) = (( sin . ((n * PI ) * 1)) * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t))))) by AS

        .= ( 0 * ((C * ( cos . (((n * PI ) * c) * t))) + (d * ( sin . (((n * PI ) * c) * t))))) by LMSIN1

        .= 0 ;

      end;

      hence thesis by AS1, Th10, Y1, Y2, Y3, Y4;

    end;

    theorem :: PDIFFEQ1:22

    

     Th30Y: for u,v be PartFunc of ( REAL 2), REAL , Z be Subset of ( REAL 2), c be Real st Z is open & Z c= ( dom u) & Z c= ( dom v) & u is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & u is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds ((u `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))) & v is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & v is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds ((v `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((v `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))) holds Z c= ( dom (u + v)) & (u + v) is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & (u + v) is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds (((u + v) `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * (((u + v) `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)))

    proof

      let u,v be PartFunc of ( REAL 2), REAL , Z be Subset of ( REAL 2), c be Real;

      assume that

       A0: Z is open & Z c= ( dom u) & Z c= ( dom v) and

       A1: u is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) and

       A2: u is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) and

       A3: (for x,t be Real st <*x, t*> in Z holds ((u `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((u `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))) and

       B1: v is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) and

       B2: v is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) and

       B3: (for x,t be Real st <*x, t*> in Z holds ((v `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((v `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)));

      Z c= (( dom u) /\ ( dom v)) by A0, XBOOLE_1: 19;

      hence Z c= ( dom (u + v)) by VALUED_1:def 1;

      ( rng ( <*1*> ^ <*1*>)) = (( rng <*1*>) \/ ( rng <*1*>)) by FINSEQ_1: 31

      .= {1} by FINSEQ_1: 38;

      then

       C1: ( rng ( <*1*> ^ <*1*>)) c= ( Seg 2) by ZFMISC_1: 7, FINSEQ_1: 2;

      ( rng ( <*2*> ^ <*2*>)) = (( rng <*2*>) \/ ( rng <*2*>)) by FINSEQ_1: 31

      .= {2} by FINSEQ_1: 38;

      then

       C2: ( rng ( <*2*> ^ <*2*>)) c= ( Seg 2) by ZFMISC_1: 7, FINSEQ_1: 2;

      

       X2: (u + v) is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & ((u + v) `partial| (Z,( <*1*> ^ <*1*>))) = ((u `partial| (Z,( <*1*> ^ <*1*>))) + (v `partial| (Z,( <*1*> ^ <*1*>)))) by PDIFF_9: 75, A0, A1, B1, C1;

      

       X3: (u + v) is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & ((u + v) `partial| (Z,( <*2*> ^ <*2*>))) = ((u `partial| (Z,( <*2*> ^ <*2*>))) + (v `partial| (Z,( <*2*> ^ <*2*>)))) by PDIFF_9: 75, A0, A2, B2, C2;

      (for x,t be Real st <*x, t*> in Z holds (((u + v) `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * (((u + v) `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)))

      proof

        let x,t be Real;

        assume

         X4: <*x, t*> in Z;

        then

         X9: ((v `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((v `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)) by B3;

        

         Y1: ( dom ((u + v) `partial| (Z,( <*2*> ^ <*2*>)))) = Z by DOMP1, A0, PDIFF_9: 75, A2, B2, C2;

        

         Y2: ( dom ((u + v) `partial| (Z,( <*1*> ^ <*1*>)))) = Z by A0, DOMP1, C1, PDIFF_9: 75, A1, B1;

        

         Y3: ( dom (u `partial| (Z,( <*2*> ^ <*2*>)))) = Z by DOMP1, A2;

        

         Y4: ( dom (v `partial| (Z,( <*2*> ^ <*2*>)))) = Z by DOMP1, B2;

        

         Y5: ( dom (u `partial| (Z,( <*1*> ^ <*1*>)))) = Z by DOMP1, A1;

        

         Y6: ( dom (v `partial| (Z,( <*1*> ^ <*1*>)))) = Z by DOMP1, B1;

        

        thus (((u + v) `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = (((u + v) `partial| (Z,( <*2*> ^ <*2*>))) . <*x, t*>) by X4, Y1, PARTFUN1:def 6

        .= (((u `partial| (Z,( <*2*> ^ <*2*>))) . <*x, t*>) + ((v `partial| (Z,( <*2*> ^ <*2*>))) . <*x, t*>)) by X3, X4, Y1, VALUED_1:def 1

        .= (((u `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) + ((v `partial| (Z,( <*2*> ^ <*2*>))) . <*x, t*>)) by X4, Y3, PARTFUN1:def 6

        .= (((u `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) + ((v `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>)) by X4, Y4, PARTFUN1:def 6

        .= (((c ^2 ) * ((u `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)) + ((c ^2 ) * ((v `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))) by X4, A3, X9

        .= ((c ^2 ) * (((u `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>) + ((v `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)))

        .= ((c ^2 ) * (((u `partial| (Z,( <*1*> ^ <*1*>))) . <*x, t*>) + ((v `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))) by Y5, X4, PARTFUN1:def 6

        .= ((c ^2 ) * (((u `partial| (Z,( <*1*> ^ <*1*>))) . <*x, t*>) + ((v `partial| (Z,( <*1*> ^ <*1*>))) . <*x, t*>))) by Y6, X4, PARTFUN1:def 6

        .= ((c ^2 ) * (((u + v) `partial| (Z,( <*1*> ^ <*1*>))) . <*x, t*>)) by X2, X4, Y2, VALUED_1:def 1

        .= ((c ^2 ) * (((u + v) `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)) by X4, Y2, PARTFUN1:def 6;

      end;

      hence thesis by PDIFF_9: 75, A1, B1, C1, A0, A2, B2, C2;

    end;

    theorem :: PDIFFEQ1:23

    for u be Functional_Sequence of ( REAL 2), REAL , Z be Subset of ( REAL 2), c be Real st Z is open & for i be Nat holds (Z c= ( dom (u . i)) & ( dom (u . i)) = ( dom (u . 0 )) & (u . i) is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & (u . i) is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds (((u . i) `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * (((u . i) `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>)))) holds for i be Nat holds (Z c= ( dom (( Partial_Sums u) . i)) & (( Partial_Sums u) . i) is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & (( Partial_Sums u) . i) is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds (((( Partial_Sums u) . i) `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * (((( Partial_Sums u) . i) `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))))

    proof

      let u be Functional_Sequence of ( REAL 2), REAL , Z be Subset of ( REAL 2), c be Real;

      assume that

       AS1: Z is open and

       AS2: for i be Nat holds (Z c= ( dom (u . i)) & ( dom (u . i)) = ( dom (u . 0 )) & (u . i) is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & (u . i) is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds (((u . i) `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * (((u . i) `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))));

      defpred X[ Nat] means (Z c= ( dom (( Partial_Sums u) . $1)) & (( Partial_Sums u) . $1) is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & (( Partial_Sums u) . $1) is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds (((( Partial_Sums u) . $1) `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * (((( Partial_Sums u) . $1) `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))));

      

       A9: for i be Nat st X[i] holds X[(i + 1)]

      proof

        let i be Nat;

        set s = (( Partial_Sums u) . i);

        set v = (u . (i + 1));

        assume that

         A11: Z c= ( dom s) and

         A12: s is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) and

         A13: s is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) and

         A14: for x,t be Real st <*x, t*> in Z holds ((s `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((s `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>));

        

         A15: (( Partial_Sums u) . (i + 1)) = (s + v) by MESFUN9C:def 2;

        Z c= ( dom v) & ( dom v) = ( dom (u . 0 )) & v is_partial_differentiable_on (Z,( <*1*> ^ <*1*>)) & v is_partial_differentiable_on (Z,( <*2*> ^ <*2*>)) & (for x,t be Real st <*x, t*> in Z holds ((v `partial| (Z,( <*2*> ^ <*2*>))) /. <*x, t*>) = ((c ^2 ) * ((v `partial| (Z,( <*1*> ^ <*1*>))) /. <*x, t*>))) by AS2;

        hence thesis by Th30Y, A11, A12, A13, A14, AS1, A15;

      end;

      (( Partial_Sums u) . 0 ) = (u . 0 ) by MESFUN9C:def 2;

      then

       A10: X[ 0 ] by AS2;

      for n be Nat holds X[n] from NAT_1:sch 2( A10, A9);

      hence thesis;

    end;