let i be Nat; for E, F, G being RealNormSpace
for Z being non empty Subset of [:E,F:]
for f being PartFunc of [:E,F:],G st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial`1| Z is_differentiable_on i,Z & diff ((f `partial`1| Z),i,Z) is_continuous_on Z & f `partial`2| Z is_differentiable_on i,Z & diff ((f `partial`2| Z),i,Z) is_continuous_on Z )
let E, F, G be RealNormSpace; for Z being non empty Subset of [:E,F:]
for f being PartFunc of [:E,F:],G st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial`1| Z is_differentiable_on i,Z & diff ((f `partial`1| Z),i,Z) is_continuous_on Z & f `partial`2| Z is_differentiable_on i,Z & diff ((f `partial`2| Z),i,Z) is_continuous_on Z )
let Z be non empty Subset of [:E,F:]; for f being PartFunc of [:E,F:],G st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial`1| Z is_differentiable_on i,Z & diff ((f `partial`1| Z),i,Z) is_continuous_on Z & f `partial`2| Z is_differentiable_on i,Z & diff ((f `partial`2| Z),i,Z) is_continuous_on Z )
let f be PartFunc of [:E,F:],G; ( f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z implies ( f `partial`1| Z is_differentiable_on i,Z & diff ((f `partial`1| Z),i,Z) is_continuous_on Z & f `partial`2| Z is_differentiable_on i,Z & diff ((f `partial`2| Z),i,Z) is_continuous_on Z ) )
assume A1:
( f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z )
; ( f `partial`1| Z is_differentiable_on i,Z & diff ((f `partial`1| Z),i,Z) is_continuous_on Z & f `partial`2| Z is_differentiable_on i,Z & diff ((f `partial`2| Z),i,Z) is_continuous_on Z )
0 <= i
by NAT_1:2;
then
f is_differentiable_on 0 + 1,Z
by A1, NDIFF_6:17, XREAL_1:7;
then A2:
f is_differentiable_on Z
by Th3, NDIFF_6:15;
then A3:
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & ( for z being Point of [:E,F:] st z in Z holds
( ( for dx being Point of E holds ((f `partial`1| Z) /. z) . dx = ((f `| Z) /. z) . (dx,(0. F)) ) & ( for dy being Point of F holds ((f `partial`2| Z) /. z) . dy = ((f `| Z) /. z) . ((0. E),dy) ) ) ) )
by Th45;
A4:
Z is open
by A2, NDIFF_1:32;
set PD1 = f `partial`1| Z;
set PD2 = f `partial`2| Z;
A5:
( dom (f `partial`1| Z) = Z & dom (f `partial`2| Z) = Z )
by A3, NDIFF_7:def 10, NDIFF_7:def 11;
consider L10 being Lipschitzian LinearOperator of E,[:E,F:] such that
A6:
for dx being Point of E holds L10 . dx = [dx,(0. F)]
by Th46;
consider L20 being Lipschitzian LinearOperator of F,[:E,F:] such that
A7:
for dy being Point of F holds L20 . dy = [(0. E),dy]
by Th47;
set BL1 = R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]);
set BL2 = R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]);
A8:
( dom (Z --> L10) = Z & rng (Z --> L10) c= {L10} )
by FUNCOP_1:13;
L10 in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
by LOPBAN_1:def 9;
then
{L10} c= the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
by ZFMISC_1:31;
then A9:
rng (Z --> L10) c= the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
by XBOOLE_1:1;
reconsider L1 = Z --> L10 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])) by A8, A9, RELSET_1:4;
reconsider L100 = L10 as Point of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])) by LOPBAN_1:def 9;
A10:
L1 = Z --> L100
;
then A11:
L1 is_differentiable_on i,Z
by A4, Th50;
A12:
L1 is_differentiable_on i + 1,Z
by A4, A10, Th50;
A13:
diff (L1,i,Z) is_continuous_on Z
by A12, NDIFF_1:45, NDIFF_6:14;
A14:
for z being Point of [:E,F:] st z in Z holds
(f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z)
proof
let z be
Point of
[:E,F:];
( z in Z implies (f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z) )
assume A15:
z in Z
;
(f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z)
then A16:
L1 /. z =
L1 . z
by A8, PARTFUN1:def 6
.=
L10
by A15, FUNCOP_1:7
;
reconsider H1 =
(f `| Z) /. z as
Lipschitzian LinearOperator of
[:E,F:],
G by LOPBAN_1:def 9;
reconsider H2 =
L1 /. z as
Lipschitzian LinearOperator of
E,
[:E,F:] by A16;
A17:
(f `partial`1| Z) /. z is
Lipschitzian LinearOperator of
E,
G
by LOPBAN_1:def 9;
then A18:
dom ((f `partial`1| Z) /. z) = the
carrier of
E
by FUNCT_2:def 1;
A19:
modetrans (
((f `| Z) /. z),
[:E,F:],
G)
= H1
by LOPBAN_1:def 11;
A20:
dom (H1 * H2) = the
carrier of
E
by FUNCT_2:def 1;
for
dx being
object st
dx in dom ((f `partial`1| Z) /. z) holds
((f `partial`1| Z) /. z) . dx = (H1 * H2) . dx
then
(f `partial`1| Z) /. z = H1 * H2
by A18, A20, FUNCT_1:2;
hence
(f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z)
by A19, LOPBAN_1:def 11;
verum
end;
A22:
( f `| Z is_differentiable_on i,Z & diff ((f `| Z),i,Z) is_continuous_on Z )
by A1, Th37;
consider B being Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)),(R_NormSpace_of_BoundedLinearOperators (E,G)) such that
A23:
for u being Point of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
for v being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) holds B . (u,v) = v * u
by Th38;
set w2 = <:L1,(f `| Z):>;
A24: dom <:L1,(f `| Z):> =
(dom (f `| Z)) /\ (dom L1)
by FUNCT_3:def 7
.=
Z /\ (dom L1)
by A2, NDIFF_1:def 9
.=
Z
by A8
;
A25:
rng <:L1,(f `| Z):> c= [:(rng L1),(rng (f `| Z)):]
by FUNCT_3:51;
[:(rng L1),(rng (f `| Z)):] c= [: the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])), the carrier of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by ZFMISC_1:96;
then
rng <:L1,(f `| Z):> c= the carrier of [:(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by A25, XBOOLE_1:1;
then reconsider w2 = <:L1,(f `| Z):> as PartFunc of [:E,F:],[:(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):] by A24, RELSET_1:4;
reconsider W = B * w2 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (E,G)) ;
A26:
( W is_differentiable_on i,Z & diff (W,i,Z) is_continuous_on Z )
by A11, A13, A22, Th42;
dom B = the carrier of [:(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by FUNCT_2:def 1;
then
rng w2 c= dom B
;
then A27:
dom W = Z
by A24, RELAT_1:27;
for x0 being object st x0 in dom (f `partial`1| Z) holds
(f `partial`1| Z) . x0 = W . x0
proof
let x0 be
object ;
( x0 in dom (f `partial`1| Z) implies (f `partial`1| Z) . x0 = W . x0 )
assume A28:
x0 in dom (f `partial`1| Z)
;
(f `partial`1| Z) . x0 = W . x0
then reconsider x =
x0 as
Point of
[:E,F:] ;
A29:
(f `partial`1| Z) . x0 =
(f `partial`1| Z) /. x
by A28, PARTFUN1:def 6
.=
((f `| Z) /. x) * (L1 /. x)
by A5, A14, A28
.=
B . (
(L1 /. x),
((f `| Z) /. x))
by A23
.=
B . [(L1 /. x),((f `| Z) /. x)]
by BINOP_1:def 1
;
A30:
dom (f `| Z) = Z
by A2, NDIFF_1:def 9;
A31:
dom <:L1,(f `| Z):> =
(dom L1) /\ (dom (f `| Z))
by FUNCT_3:def 7
.=
Z
by A8, A30
;
[(L1 /. x),((f `| Z) /. x)] =
[(L1 . x),((f `| Z) /. x)]
by A5, A8, A28, PARTFUN1:def 6
.=
[(L1 . x),((f `| Z) . x)]
by A5, A28, A30, PARTFUN1:def 6
.=
w2 . x
by A5, A28, A31, FUNCT_3:def 7
;
hence
(f `partial`1| Z) . x0 = W . x0
by A5, A28, A29, A31, FUNCT_1:13;
verum
end;
hence
( f `partial`1| Z is_differentiable_on i,Z & diff ((f `partial`1| Z),i,Z) is_continuous_on Z )
by A5, A26, A27, FUNCT_1:2; ( f `partial`2| Z is_differentiable_on i,Z & diff ((f `partial`2| Z),i,Z) is_continuous_on Z )
A32:
( dom (Z --> L20) = Z & rng (Z --> L20) c= {L20} )
by FUNCOP_1:13;
L20 in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
by LOPBAN_1:def 9;
then
{L20} c= the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
by ZFMISC_1:31;
then A33:
rng (Z --> L20) c= the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
by XBOOLE_1:1;
reconsider L2 = Z --> L20 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])) by A32, A33, RELSET_1:4;
reconsider L100 = L20 as Point of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])) by LOPBAN_1:def 9;
A34:
L2 = Z --> L100
;
then A35:
L2 is_differentiable_on i,Z
by A4, Th50;
L2 is_differentiable_on i + 1,Z
by A4, A34, Th50;
then A36:
diff (L2,i,Z) is_continuous_on Z
by NDIFF_1:45, NDIFF_6:14;
A37:
( dom (Z --> L20) = Z & rng (Z --> L20) c= {L20} )
by FUNCOP_1:13;
A38:
for z being Point of [:E,F:] st z in Z holds
(f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z)
proof
let z be
Point of
[:E,F:];
( z in Z implies (f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z) )
assume A39:
z in Z
;
(f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z)
then A40:
L2 /. z =
L2 . z
by A37, PARTFUN1:def 6
.=
L20
by A39, FUNCOP_1:7
;
reconsider H1 =
(f `| Z) /. z as
Lipschitzian LinearOperator of
[:E,F:],
G by LOPBAN_1:def 9;
reconsider H2 =
L2 /. z as
Lipschitzian LinearOperator of
F,
[:E,F:] by A40;
A41:
(f `partial`2| Z) /. z is
Lipschitzian LinearOperator of
F,
G
by LOPBAN_1:def 9;
then A42:
dom ((f `partial`2| Z) /. z) = the
carrier of
F
by FUNCT_2:def 1;
A43:
modetrans (
(L2 /. z),
F,
[:E,F:])
= H2
by LOPBAN_1:def 11;
A44:
dom (H1 * H2) = the
carrier of
F
by FUNCT_2:def 1;
for
dx being
object st
dx in dom ((f `partial`2| Z) /. z) holds
((f `partial`2| Z) /. z) . dx = (H1 * H2) . dx
then
(f `partial`2| Z) /. z = H1 * H2
by A42, A44, FUNCT_1:2;
hence
(f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z)
by A43, LOPBAN_1:def 11;
verum
end;
A46:
( f `| Z is_differentiable_on i,Z & diff ((f `| Z),i,Z) is_continuous_on Z )
by A1, Th37;
consider B being Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)),(R_NormSpace_of_BoundedLinearOperators (F,G)) such that
A47:
for u being Point of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
for v being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) holds B . (u,v) = v * u
by Th38;
set w2 = <:L2,(f `| Z):>;
A48: dom <:L2,(f `| Z):> =
(dom (f `| Z)) /\ (dom L2)
by FUNCT_3:def 7
.=
Z /\ (dom L2)
by A2, NDIFF_1:def 9
.=
Z
by A37
;
A49:
rng <:L2,(f `| Z):> c= [:(rng L2),(rng (f `| Z)):]
by FUNCT_3:51;
[:(rng L2),(rng (f `| Z)):] c= [: the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])), the carrier of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by ZFMISC_1:96;
then
rng <:L2,(f `| Z):> c= the carrier of [:(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by A49, XBOOLE_1:1;
then reconsider w2 = <:L2,(f `| Z):> as PartFunc of [:E,F:],[:(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):] by A48, RELSET_1:4;
reconsider W = B * w2 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (F,G)) ;
A50:
( W is_differentiable_on i,Z & diff (W,i,Z) is_continuous_on Z )
by A35, A36, A46, Th42;
dom B = the carrier of [:(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by FUNCT_2:def 1;
then
rng w2 c= dom B
;
then A51:
dom W = Z
by A48, RELAT_1:27;
for x0 being object st x0 in dom (f `partial`2| Z) holds
(f `partial`2| Z) . x0 = W . x0
proof
let x0 be
object ;
( x0 in dom (f `partial`2| Z) implies (f `partial`2| Z) . x0 = W . x0 )
assume A52:
x0 in dom (f `partial`2| Z)
;
(f `partial`2| Z) . x0 = W . x0
then reconsider x =
x0 as
Point of
[:E,F:] ;
A53:
(f `partial`2| Z) . x0 =
(f `partial`2| Z) /. x
by A52, PARTFUN1:def 6
.=
((f `| Z) /. x) * (L2 /. x)
by A5, A38, A52
.=
B . (
(L2 /. x),
((f `| Z) /. x))
by A47
.=
B . [(L2 /. x),((f `| Z) /. x)]
by BINOP_1:def 1
;
A54:
dom (f `| Z) = Z
by A2, NDIFF_1:def 9;
A55:
dom <:L2,(f `| Z):> =
(dom L2) /\ (dom (f `| Z))
by FUNCT_3:def 7
.=
Z
by A37, A54
;
[(L2 /. x),((f `| Z) /. x)] =
[(L2 . x),((f `| Z) /. x)]
by A5, A37, A52, PARTFUN1:def 6
.=
[(L2 . x),((f `| Z) . x)]
by A5, A52, A54, PARTFUN1:def 6
.=
w2 . x
by A5, A52, A55, FUNCT_3:def 7
;
hence
(f `partial`2| Z) . x0 = W . x0
by A5, A52, A53, A55, FUNCT_1:13;
verum
end;
hence
( f `partial`2| Z is_differentiable_on i,Z & diff ((f `partial`2| Z),i,Z) is_continuous_on Z )
by A5, A50, A51, FUNCT_1:2; verum