theorem :: PDIFFEQ1:10

for f, g being PartFunc of REAL,REAL
for u being PartFunc of (REAL 2),REAL
for x0, t0 being Real
for z being Element of REAL 2 st x0 in dom f & t0 in dom g & z = <*x0,t0*> & dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & g is_differentiable_in t0 & ( for x, t being 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)) )