let f, g be Function of REAL,REAL; :: thesis: for u being PartFunc of (REAL 2),REAL
for c being Real st f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & dom u = [#] (REAL 2) & ( for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) ) & ( for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
let u be PartFunc of (REAL 2),REAL; :: thesis: for c being Real st f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & dom u = [#] (REAL 2) & ( for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) ) & ( for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
let c be Real; :: thesis: ( f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & dom u = [#] (REAL 2) & ( for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) ) & ( for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) ) implies ( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) ) )
assume that
AS1: f is_differentiable_on 2, [#] REAL and
AS2: g is_differentiable_on 2, [#] REAL and
AS3: dom u = [#] (REAL 2) and
AS4: for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) and
AS5: for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) ; :: thesis: ( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
P1: ( [#] REAL = dom f & [#] REAL = dom g ) by FUNCT_2:def 1;
P4: for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) by AS4;
for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>)

proof

let x, t be Real; :: thesis: (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>)
X1: (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) by AS5;
X3: ( x in [#] REAL & t in [#] REAL ) by XREAL_0:def 1;
then (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) by LM30, AS1, AS2, AS3, P1, LMOP3, P4;
hence (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) by LM30, AS1, AS2, AS3, P1, LMOP3, P4, X1, X3; :: thesis: verum

end;

hence ( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) ) by LM30, AS1, AS2, AS3, P1, LMOP3, P4; :: thesis: verum