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 ) } & f is_differentiable_in x0 & ( 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,1 & partdiff (u,z,1) = (diff (f,x0)) * (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 ) } & f is_differentiable_in x0 & ( 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,1 & partdiff (u,z,1) = (diff (f,x0)) * (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 ) } & f is_differentiable_in x0 & ( 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,1 & partdiff (u,z,1) = (diff (f,x0)) * (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 ) } & f is_differentiable_in x0 & ( 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,1 & partdiff (u,z,1) = (diff (f,x0)) * (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: f is_differentiable_in x0 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,1 & partdiff (u,z,1) = (diff (f,x0)) * (g /. t0) )
P51: u * (reproj (1,z)) = (g /. t0) (#) f by LM11, A0, A4, A7;
(proj (1,2)) . z = x0 by A0, LM03;
hence u is_partial_differentiable_in z,1 by A5, FDIFF_1:15, P51; :: thesis: partdiff (u,z,1) = (diff (f,x0)) * (g /. t0)
thus partdiff (u,z,1) = diff (((g /. t0) (#) f),x0) by A0, LM03, P51
.= (diff (f,x0)) * (g /. t0) by A5, FDIFF_1:15 ; :: thesis: verum