let S be RealNormSpace-Sequence; for G being RealNormSpace
for Z being non empty Subset of (product S)
for f being PartFunc of (product S),G
for s being set
for i being Nat st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),i,Z) is_continuous_on Z )
let G be RealNormSpace; for Z being non empty Subset of (product S)
for f being PartFunc of (product S),G
for s being set
for i being Nat st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),i,Z) is_continuous_on Z )
let Z be non empty Subset of (product S); for f being PartFunc of (product S),G
for s being set
for i being Nat st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),i,Z) is_continuous_on Z )
let f be PartFunc of (product S),G; for s being set
for i being Nat st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),i,Z) is_continuous_on Z )
let s be set ; for i being Nat st f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z holds
( f `partial| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),i,Z) is_continuous_on Z )
let i be Nat; ( f is_differentiable_on i + 1,Z & diff (f,(i + 1),Z) is_continuous_on Z implies ( f `partial| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),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| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),i,Z) is_continuous_on Z )
then
f is_differentiable_on 0 + 1,Z
;
then A2:
f is_differentiable_on Z
by NDIFF_6:15, NDIFF13:2;
then A3:
Z is open
by NDIFF_1:32;
then A4:
( f is_partial_differentiable_on Z,s & ( for z being Point of (product S) st z in Z holds
(f `partial| (Z,s)) /. z = ((f `| Z) /. z) * (reproj ((In (s,(dom S))),(0. (product S)))) ) )
by A2, Th22;
set PD1 = f `partial| (Z,s);
set E = S . (In (s,(dom S)));
A5:
dom (f `partial| (Z,s)) = Z
by A4, NDIFF_5:def 9;
reconsider L10 = reproj ((In (s,(dom S))),(0. (product S))) as Lipschitzian LinearOperator of (S . (In (s,(dom S)))),(product S) by Th23;
set BL1 = R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S));
A6:
( dom (Z --> L10) = Z & rng (Z --> L10) c= {L10} )
by FUNCOP_1:13;
L10 in the carrier of (R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S)))
by LOPBAN_1:def 9;
then
{L10} c= the carrier of (R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S)))
by ZFMISC_1:31;
then A7:
rng (Z --> L10) c= the carrier of (R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S)))
by XBOOLE_1:1;
reconsider L1 = Z --> L10 as PartFunc of (product S),(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))) by RELSET_1:4, A6, A7;
reconsider L100 = L10 as Point of (R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))) by LOPBAN_1:def 9;
A8:
L1 = Z --> L100
;
then A9:
L1 is_differentiable_on i,Z
by A3, NDIFF13:49;
A10:
L1 is_differentiable_on i + 1,Z
by A3, A8, NDIFF13:49;
then A11:
diff (L1,i,Z) is_continuous_on Z
by NDIFF_1:45, NDIFF_6:14;
A12:
for z being Point of (product S) st z in Z holds
(f `partial| (Z,s)) /. z = ((f `| Z) /. z) * (L1 /. z)
proof
let z be
Point of
(product S);
( z in Z implies (f `partial| (Z,s)) /. z = ((f `| Z) /. z) * (L1 /. z) )
assume A13:
z in Z
;
(f `partial| (Z,s)) /. z = ((f `| Z) /. z) * (L1 /. z)
then A14:
L1 /. z =
L1 . z
by A6, PARTFUN1:def 6
.=
L10
by FUNCOP_1:7, A13
;
reconsider H1 =
(f `| Z) /. z as
Lipschitzian LinearOperator of
(product S),
G by LOPBAN_1:def 9;
reconsider H2 =
L1 /. z as
Lipschitzian LinearOperator of
(S . (In (s,(dom S)))),
(product S) by A14;
A16:
modetrans (
(L1 /. z),
(S . (In (s,(dom S)))),
(product S))
= H2
by LOPBAN_1:def 11;
(f `partial| (Z,s)) /. z = H1 * H2
by A2, A3, A13, A14, Th22;
hence
(f `partial| (Z,s)) /. z = ((f `| Z) /. z) * (L1 /. z)
by A16, LOPBAN_1:def 11;
verum
end;
A19:
( f `| Z is_differentiable_on i,Z & diff ((f `| Z),i,Z) is_continuous_on Z )
by A1, NDIFF13:36;
consider B being Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))),(R_NormSpace_of_BoundedLinearOperators ((product S),G)),(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),G)) such that
A20:
for u being Point of (R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S)))
for v being Point of (R_NormSpace_of_BoundedLinearOperators ((product S),G)) holds B . (u,v) = v * u
by NDIFF13:37;
set w2 = <:L1,(f `| Z):>;
A21: 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 A6
;
A22:
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 ((S . (In (s,(dom S)))),(product S))), the carrier of (R_NormSpace_of_BoundedLinearOperators ((product S),G)):]
by ZFMISC_1:96;
then
rng <:L1,(f `| Z):> c= the carrier of [:(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))),(R_NormSpace_of_BoundedLinearOperators ((product S),G)):]
by A22, XBOOLE_1:1;
then reconsider w2 = <:L1,(f `| Z):> as PartFunc of (product S),[:(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))),(R_NormSpace_of_BoundedLinearOperators ((product S),G)):] by RELSET_1:4, A21;
reconsider W = B * w2 as PartFunc of (product S),(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),G)) ;
A23:
( W is_differentiable_on i,Z & diff (W,i,Z) is_continuous_on Z )
by NDIFF13:41, A9, A11, A19;
dom B = the carrier of [:(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))),(R_NormSpace_of_BoundedLinearOperators ((product S),G)):]
by FUNCT_2:def 1;
then
rng w2 c= dom B
;
then A24:
dom W = Z
by A21, RELAT_1:27;
for x0 being object st x0 in dom (f `partial| (Z,s)) holds
(f `partial| (Z,s)) . x0 = W . x0
proof
let x0 be
object ;
( x0 in dom (f `partial| (Z,s)) implies (f `partial| (Z,s)) . x0 = W . x0 )
assume A25:
x0 in dom (f `partial| (Z,s))
;
(f `partial| (Z,s)) . x0 = W . x0
then reconsider x =
x0 as
Point of
(product S) ;
A26:
(f `partial| (Z,s)) . x0 =
(f `partial| (Z,s)) /. x
by A25, PARTFUN1:def 6
.=
((f `| Z) /. x) * (L1 /. x)
by A12, A25, A5
.=
B . (
(L1 /. x),
((f `| Z) /. x))
by A20
.=
B . [(L1 /. x),((f `| Z) /. x)]
;
A27:
dom (f `| Z) = Z
by A2, NDIFF_1:def 9;
A28:
dom <:L1,(f `| Z):> =
(dom L1) /\ (dom (f `| Z))
by FUNCT_3:def 7
.=
Z
by A6, A27
;
[(L1 /. x),((f `| Z) /. x)] =
[(L1 . x),((f `| Z) /. x)]
by A6, PARTFUN1:def 6, A25, A5
.=
[(L1 . x),((f `| Z) . x)]
by PARTFUN1:def 6, A27, A25, A5
.=
w2 . x
by A5, A25, A28, FUNCT_3:def 7
;
hence
(f `partial| (Z,s)) . x0 = W . x0
by A5, A25, A26, A28, FUNCT_1:13;
verum
end;
hence
( f `partial| (Z,s) is_differentiable_on i,Z & diff ((f `partial| (Z,s)),i,Z) is_continuous_on Z )
by A23, FUNCT_1:2, A5, A24; verum