theorem LM30: :: PDIFFEQ1:12

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