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 holds
f `partial| (Z,s) is_differentiable_on i,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 holds
f `partial| (Z,s) is_differentiable_on i,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 holds
f `partial| (Z,s) is_differentiable_on i,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 holds
f `partial| (Z,s) is_differentiable_on i,Z
let s be set ; for i being Nat st f is_differentiable_on i + 1,Z holds
f `partial| (Z,s) is_differentiable_on i,Z
let i be Nat; ( f is_differentiable_on i + 1,Z implies f `partial| (Z,s) is_differentiable_on i,Z )
assume A1:
f is_differentiable_on i + 1,Z
; f `partial| (Z,s) is_differentiable_on i,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);
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;
then reconsider L1 = Z --> L10 as PartFunc of (product S),(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))) by A6, RELSET_1:4;
reconsider L100 = L10 as Point of (R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),(product S))) by LOPBAN_1:def 9;
L1 = Z --> L100
;
then A8:
L1 is_differentiable_on i,Z
by A3, NDIFF13:49;
A9:
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 A10:
z in Z
;
(f `partial| (Z,s)) /. z = ((f `| Z) /. z) * (L1 /. z)
then A11:
L1 /. z =
L1 . z
by A6, PARTFUN1:def 6
.=
L10
by A10, FUNCOP_1:7
;
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 A11;
A13:
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, A10, A11, Th22;
hence
(f `partial| (Z,s)) /. z = ((f `| Z) /. z) * (L1 /. z)
by A13, LOPBAN_1:def 11;
verum
end;
A16:
f `| Z is_differentiable_on i,Z
by A1, NDIFF13:35;
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
A17:
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):>;
A18: 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
;
A19:
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 A19, 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 A18, RELSET_1:4;
reconsider W = B * w2 as PartFunc of (product S),(R_NormSpace_of_BoundedLinearOperators ((S . (In (s,(dom S)))),G)) ;
A20:
W is_differentiable_on i,Z
by A8, A16, NDIFF13:38;
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 A21:
dom W = Z
by A18, 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 A22:
x0 in dom (f `partial| (Z,s))
;
(f `partial| (Z,s)) . x0 = W . x0
then reconsider x =
x0 as
Point of
(product S) ;
A23:
(f `partial| (Z,s)) . x0 =
(f `partial| (Z,s)) /. x
by A22, PARTFUN1:def 6
.=
((f `| Z) /. x) * (L1 /. x)
by A5, A9, A22
.=
B . (
(L1 /. x),
((f `| Z) /. x))
by A17
.=
B . [(L1 /. x),((f `| Z) /. x)]
;
A24:
dom (f `| Z) = Z
by A2, NDIFF_1:def 9;
A25:
dom <:L1,(f `| Z):> =
(dom L1) /\ (dom (f `| Z))
by FUNCT_3:def 7
.=
Z
by A6, A24
;
[(L1 /. x),((f `| Z) /. x)] =
[(L1 . x),((f `| Z) /. x)]
by A5, A6, A22, PARTFUN1:def 6
.=
[(L1 . x),((f `| Z) . x)]
by A5, A22, A24, PARTFUN1:def 6
.=
w2 . x
by A5, A22, A25, FUNCT_3:def 7
;
hence
(f `partial| (Z,s)) . x0 = W . x0
by A5, A22, A23, A25, FUNCT_1:13;
verum
end;
hence
f `partial| (Z,s) is_differentiable_on i,Z
by A5, A20, A21, FUNCT_1:2; verum