theorem LM20: :: PDIFFEQ1:11

for X, T being Subset of REAL
for Z being Subset of (REAL 2)
for f, g being PartFunc of REAL,REAL
for u being 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 is Real : ( x in X & t in T ) } & dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & f is_differentiable_on X & g is_differentiable_on T & ( 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_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)) ) )