let u, v be PartFunc of (REAL 2),REAL; for Z being Subset of (REAL 2)
for c being Real st Z is open & Z c= dom u & Z c= dom v & u is_partial_differentiable_on Z,<*1*> ^ <*1*> & u is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) & v is_partial_differentiable_on Z,<*1*> ^ <*1*> & v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) holds
( Z c= dom (u + v) & u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
let Z be Subset of (REAL 2); for c being Real st Z is open & Z c= dom u & Z c= dom v & u is_partial_differentiable_on Z,<*1*> ^ <*1*> & u is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) & v is_partial_differentiable_on Z,<*1*> ^ <*1*> & v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) holds
( Z c= dom (u + v) & u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
let c be Real; ( Z is open & Z c= dom u & Z c= dom v & u is_partial_differentiable_on Z,<*1*> ^ <*1*> & u is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) & v is_partial_differentiable_on Z,<*1*> ^ <*1*> & v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) implies ( Z c= dom (u + v) & u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) ) )
assume that
A0:
( Z is open & Z c= dom u & Z c= dom v )
and
A1:
u is_partial_differentiable_on Z,<*1*> ^ <*1*>
and
A2:
u is_partial_differentiable_on Z,<*2*> ^ <*2*>
and
A3:
for x, t being Real st <*x,t*> in Z holds
(u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>)
and
B1:
v is_partial_differentiable_on Z,<*1*> ^ <*1*>
and
B2:
v is_partial_differentiable_on Z,<*2*> ^ <*2*>
and
B3:
for x, t being Real st <*x,t*> in Z holds
(v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>)
; ( Z c= dom (u + v) & u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
Z c= (dom u) /\ (dom v)
by A0, XBOOLE_1:19;
hence
Z c= dom (u + v)
by VALUED_1:def 1; ( u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
rng (<*1*> ^ <*1*>) =
(rng <*1*>) \/ (rng <*1*>)
by FINSEQ_1:31
.=
{1}
by FINSEQ_1:38
;
then C1:
rng (<*1*> ^ <*1*>) c= Seg 2
by ZFMISC_1:7, FINSEQ_1:2;
rng (<*2*> ^ <*2*>) =
(rng <*2*>) \/ (rng <*2*>)
by FINSEQ_1:31
.=
{2}
by FINSEQ_1:38
;
then C2:
rng (<*2*> ^ <*2*>) c= Seg 2
by ZFMISC_1:7, FINSEQ_1:2;
X2:
( u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & (u + v) `partial| (Z,(<*1*> ^ <*1*>)) = (u `partial| (Z,(<*1*> ^ <*1*>))) + (v `partial| (Z,(<*1*> ^ <*1*>))) )
by PDIFF_9:75, A0, A1, B1, C1;
X3:
( u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & (u + v) `partial| (Z,(<*2*> ^ <*2*>)) = (u `partial| (Z,(<*2*> ^ <*2*>))) + (v `partial| (Z,(<*2*> ^ <*2*>))) )
by PDIFF_9:75, A0, A2, B2, C2;
for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>)
proof
let x,
t be
Real;
( <*x,t*> in Z implies ((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) )
assume X4:
<*x,t*> in Z
;
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>)
then X9:
(v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>)
by B3;
Y1:
dom ((u + v) `partial| (Z,(<*2*> ^ <*2*>))) = Z
by DOMP1, A0, PDIFF_9:75, A2, B2, C2;
Y2:
dom ((u + v) `partial| (Z,(<*1*> ^ <*1*>))) = Z
by A0, DOMP1, C1, PDIFF_9:75, A1, B1;
Y3:
dom (u `partial| (Z,(<*2*> ^ <*2*>))) = Z
by DOMP1, A2;
Y4:
dom (v `partial| (Z,(<*2*> ^ <*2*>))) = Z
by DOMP1, B2;
Y5:
dom (u `partial| (Z,(<*1*> ^ <*1*>))) = Z
by DOMP1, A1;
Y6:
dom (v `partial| (Z,(<*1*> ^ <*1*>))) = Z
by DOMP1, B1;
thus ((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> =
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) . <*x,t*>
by X4, Y1, PARTFUN1:def 6
.=
((u `partial| (Z,(<*2*> ^ <*2*>))) . <*x,t*>) + ((v `partial| (Z,(<*2*> ^ <*2*>))) . <*x,t*>)
by X3, X4, Y1, VALUED_1:def 1
.=
((u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*>) + ((v `partial| (Z,(<*2*> ^ <*2*>))) . <*x,t*>)
by X4, Y3, PARTFUN1:def 6
.=
((u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*>) + ((v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*>)
by X4, Y4, PARTFUN1:def 6
.=
((c ^2) * ((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>)) + ((c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>))
by X4, A3, X9
.=
(c ^2) * (((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) + ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>))
.=
(c ^2) * (((u `partial| (Z,(<*1*> ^ <*1*>))) . <*x,t*>) + ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>))
by Y5, X4, PARTFUN1:def 6
.=
(c ^2) * (((u `partial| (Z,(<*1*> ^ <*1*>))) . <*x,t*>) + ((v `partial| (Z,(<*1*> ^ <*1*>))) . <*x,t*>))
by Y6, X4, PARTFUN1:def 6
.=
(c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) . <*x,t*>)
by X2, X4, Y2, VALUED_1:def 1
.=
(c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>)
by X4, Y2, PARTFUN1:def 6
;
verum
end;
hence
( u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
by PDIFF_9:75, A1, B1, C1, A0, A2, B2, C2; verum