let f, g be PartFunc of REAL,REAL; :: thesis: 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)) )
let u be PartFunc of (REAL 2),REAL; :: thesis: 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)) )
let x0, t0 be Real; :: thesis: 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)) )
let z be Element of REAL 2; :: thesis: ( 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) ) implies ( u is_partial_differentiable_in z,2 & partdiff (u,z,2) = (f /. x0) * (diff (g,t0)) ) )
assume that
A0: ( x0 in dom f & t0 in dom g & z = <*x0,t0*> ) and
A4: dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } and
A5: g is_differentiable_in t0 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: ( u is_partial_differentiable_in z,2 & partdiff (u,z,2) = (f /. x0) * (diff (g,t0)) )
P52: (proj (2,2)) . z = t0 by A0, LM03;
(f /. x0) (#) g is_differentiable_in t0 by A5, FDIFF_1:15;
hence u is_partial_differentiable_in z,2 by LM11, A0, A4, A7, P52; :: thesis: partdiff (u,z,2) = (f /. x0) * (diff (g,t0))
thus partdiff (u,z,2) = diff (((f /. x0) (#) g),t0) by A0, LM11, A4, A7, P52
.= (f /. x0) * (diff (g,t0)) by A5, FDIFF_1:15 ; :: thesis: verum