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 X and
A6: g is_differentiable_on 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:
A8: Z c= dom u

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in Z ; :: thesis:
then consider x, t being Real such that
A80: ( z = <*x,t*> & x in X & t in T ) by A3;
thus z in dom u by A80, A1, A4; :: thesis:

end;

for z being Element of REAL 2 st z in Z holds
u is_partial_differentiable_in z,1

let z be Element of REAL 2; :: thesis:
assume z in Z ; :: thesis:
then consider x, t being 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; :: thesis:

end;

then P1: u is_partial_differentiable_on Z,1 by A2, A8, PDIFF_9:60;
hence u is_partial_differentiable_on Z,<*1*> ; :: thesis:
P3: u `partial| (Z,<*1*>) = u `partial| (Z,1) by A2, PDIFF_9:82, P1;
P5: for x, t being Real
for z being Element of REAL 2 st x in X & t in T & z = <*x,t*> holds
partdiff (u,z,1) = (diff (f,x)) * (g /. t)

let x, t be Real; :: thesis:
let z be Element of REAL 2; :: thesis:
assume P50: ( x in X & t in T & z = <*x,t*> ) ; :: thesis:
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 partdiff (u,z,1) = (diff (f,x)) * (g /. t) by P51, P52, FDIFF_1:15; :: thesis:

end;

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

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

end;

for z being Element of REAL 2 st z in Z holds
u is_partial_differentiable_in z,2

let z be Element of REAL 2; :: thesis:
assume z in Z ; :: thesis:
then consider x, t being 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; :: thesis:

end;

then P1: u is_partial_differentiable_on Z,2 by A2, A8, PDIFF_9:60;
hence u is_partial_differentiable_on Z,<*2*> ; :: thesis:
P3: u `partial| (Z,<*2*>) = u `partial| (Z,2) by A2, PDIFF_9:82, P1;
P5: for x, t being Real
for z being Element of REAL 2 st x in X & t in T & z = <*x,t*> holds
partdiff (u,z,2) = (f /. x) * (diff (g,t))

let x, t be Real; :: thesis:
let z be Element of REAL 2; :: thesis:
assume P50: ( x in X & t in T & z = <*x,t*> ) ; :: thesis:
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 partdiff (u,z,2) = (f /. x) * (diff (g,t)) by FDIFF_1:15, P51, P52; :: thesis:

end;

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