let c be Real; :: thesis:
let f, g be Function of REAL,REAL; :: thesis:
let u be Function of (REAL 2),REAL; :: thesis:
assume that
XP1: f is_differentiable_on 2, [#] REAL and
XP2: g is_differentiable_on 2, [#] REAL and
XP3: for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) and
AS4: for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) ; :: thesis:
P0: dom u = [#] (REAL 2) by FUNCT_2:def 1;
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;
(diff (f,([#] REAL))) . 0 is_differentiable_on [#] REAL by XP1;
then f | ([#] REAL) is_differentiable_on [#] REAL by TAYLOR_1:def 5;
then B50: ( [#] REAL c= dom (f | ([#] REAL)) & ( for x being Real st x in [#] REAL holds
(f | ([#] REAL)) | ([#] REAL) is_differentiable_in x ) ) by FDIFF_1:def 6;
(f | ([#] REAL)) | ([#] REAL) = f | ([#] REAL) by RELAT_1:72;
then Q1: f is_differentiable_on [#] REAL by B50, FDIFF_1:def 6, P1;
(diff (g,([#] REAL))) . 0 is_differentiable_on [#] REAL by XP2;
then g | ([#] REAL) is_differentiable_on [#] REAL by TAYLOR_1:def 5;
then B50: ( [#] REAL c= dom (g | ([#] REAL)) & ( for x being Real st x in [#] REAL holds
(g | ([#] REAL)) | ([#] REAL) is_differentiable_in x ) ) by FDIFF_1:def 6;
(g | ([#] REAL)) | ([#] REAL) = g | ([#] REAL) by RELAT_1:72;
then Q2: g is_differentiable_on [#] REAL by B50, FDIFF_1:def 6, P1;
Y1: for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t)

proof

let x, t be Real; :: thesis:
( x in [#] REAL & t in [#] REAL ) by XREAL_0:def 1;
hence (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t) by Q1, Q2, LM20, P4, P0, P1, LMOP3; :: thesis:

end;

Y2: for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = (f /. x) * (diff (g,t))

proof

let x, t be Real; :: thesis:
( x in [#] REAL & t in [#] REAL ) by XREAL_0:def 1;
hence (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = (f /. x) * (diff (g,t)) by Q1, Q2, LM20, P4, P0, P1, LMOP3; :: thesis:

end;

Y3: for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t)

proof

let x, t be Real; :: thesis:
( x in [#] REAL & t in [#] REAL ) by XREAL_0:def 1;
hence (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) by LM40, AS4, P0, XP1, XP2, XP3; :: thesis:

end;

for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t)

proof

let x, t be Real; :: thesis:
( x in [#] REAL & t in [#] REAL ) by XREAL_0:def 1;
hence (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) by LM40, AS4, P0, XP1, XP2, XP3; :: thesis:

end;

hence ( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = (f /. x) * (diff (g,t)) ) & f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being 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 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 AS4, Q1, Q2, LM20, P4, P0, P1, LMOP3, Y1, Y2, Y3, XP1, XP2, XP3, LM40; :: thesis: