let X, T be Subset of REAL; :: thesis:
let Z be Subset of (REAL 2); :: thesis:
let f, g be PartFunc of REAL,REAL; :: thesis:
let u be PartFunc of (REAL 2),REAL; :: thesis:
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 is Real : ( x in X & t in T ) } and
A4: dom u = { <*x,t*> where x, t is 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 being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ; :: thesis:
(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 being 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 being 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 being 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 being 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 is 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 being 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)

let x, t be Real; :: thesis:
assume C70: ( x in dom (f `| X) & t in dom (g | T) ) ; :: thesis:
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; :: thesis:

end;

then ( u `partial| (Z,<*1*>) is_partial_differentiable_on Z,<*1*> & ( for x, t being 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; :: thesis:
thus for x, t being Real st x in X & t in T holds
(u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,X)) . 2) /. x) * (g /. t) :: thesis:

let x, t be Real; :: thesis:
assume F1: ( x in X & t in T ) ; :: thesis:
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 (u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,X)) . 2) /. x) * (g /. t) by F2, PDIFF_9:88, B7, F4; :: thesis:

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 is 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 being 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)

let x, t be Real; :: thesis:
assume C70: ( x in dom (f | X) & t in dom (g `| T) ) ; :: thesis:
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; :: thesis:

end;

then ( u `partial| (Z,<*2*>) is_partial_differentiable_on Z,<*2*> & ( for x, t being 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; :: thesis:
let x, t be Real; :: thesis:
assume F1: ( x in X & t in T ) ; :: thesis:
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 (u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,T)) . 2) /. t) by F1, F3, F4, LM20, A2, A3, C1, C3, C4, C5, D6, C7; :: thesis: