let E, F be RealNormSpace; for L being Lipschitzian LinearOperator of E,F
for i being Nat holds
( diff (L,(i + 1),([#] E)) is_differentiable_on [#] E & (diff (L,(i + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP ((i + 2),E,F))) & (diff (L,(i + 1),([#] E))) `| ([#] E) is_continuous_on [#] E )
let L be Lipschitzian LinearOperator of E,F; for i being Nat holds
( diff (L,(i + 1),([#] E)) is_differentiable_on [#] E & (diff (L,(i + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP ((i + 2),E,F))) & (diff (L,(i + 1),([#] E))) `| ([#] E) is_continuous_on [#] E )
defpred S1[ Nat] means ( diff (L,($1 + 1),([#] E)) is_differentiable_on [#] E & (diff (L,($1 + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP (($1 + 2),E,F))) & (diff (L,($1 + 1),([#] E))) `| ([#] E) is_continuous_on [#] E );
A1:
L is Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
by LOPBAN_1:def 9;
A2:
S1[ 0 ]
proof
A3:
diff_SP (1,
E,
F)
= R_NormSpace_of_BoundedLinearOperators (
E,
F)
by NDIFF_6:7;
diff_SP (2,
E,
F) =
diff_SP (
(1 + 1),
E,
F)
.=
R_NormSpace_of_BoundedLinearOperators (
E,
(diff_SP (1,E,F)))
by NDIFF_6:10
;
then A4:
0. (diff_SP (2,E,F)) =
([#] E) --> (0. (diff_SP (1,E,F)))
by LOPBAN_1:31
.=
([#] E) --> (([#] E) --> (0. F))
by A3, LOPBAN_1:31
;
set L1 =
diff (
L,
(0 + 1),
([#] E));
A5:
diff (
L,
(0 + 1),
([#] E))
= ([#] E) --> L
by Th16;
then A6:
dom (diff (L,(0 + 1),([#] E))) = [#] E
by FUNCOP_1:13;
rng (diff (L,(0 + 1),([#] E))) = {L}
by A5, FUNCOP_1:8;
hence
diff (
L,
(0 + 1),
([#] E))
is_differentiable_on [#] E
by A1, A3, A6, NDIFF_1:33;
( (diff (L,(0 + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP ((0 + 2),E,F))) & (diff (L,(0 + 1),([#] E))) `| ([#] E) is_continuous_on [#] E )
thus A7:
(diff (L,(0 + 1),([#] E))) `| ([#] E) =
diff (
L,
(1 + 1),
([#] E))
by NDIFF_6:13
.=
([#] E) --> (0. (diff_SP ((0 + 2),E,F)))
by A4, Th16
;
(diff (L,(0 + 1),([#] E))) `| ([#] E) is_continuous_on [#] E
then A8:
dom ((diff (L,(0 + 1),([#] E))) `| ([#] E)) = [#] E
by FUNCOP_1:13;
reconsider r =
0. (diff_SP (((0 + 1) + 1),E,F)) as
Point of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP ((0 + 1),E,F)))) by NDIFF_6:10;
rng ((diff (L,(0 + 1),([#] E))) `| ([#] E)) = {r}
by A7, FUNCOP_1:8;
hence
(diff (L,(0 + 1),([#] E))) `| ([#] E) is_continuous_on [#] E
by A8, NFCONT_1:47;
verum
end;
A9:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A10:
S1[
i]
;
S1[i + 1]
set L1 =
diff (
L,
((i + 1) + 1),
([#] E));
A11:
diff (
L,
((i + 1) + 1),
([#] E))
= (diff (L,(i + 1),([#] E))) `| ([#] E)
by NDIFF_6:13;
then A12:
dom (diff (L,((i + 1) + 1),([#] E))) = [#] E
by A10, FUNCOP_1:13;
rng (diff (L,((i + 1) + 1),([#] E))) = {(0. (diff_SP ((i + 2),E,F)))}
by A10, A11, FUNCOP_1:8;
hence
diff (
L,
((i + 1) + 1),
([#] E))
is_differentiable_on [#] E
by A12, NDIFF_1:33;
( (diff (L,((i + 1) + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP (((i + 1) + 2),E,F))) & (diff (L,((i + 1) + 1),([#] E))) `| ([#] E) is_continuous_on [#] E )
thus A13:
(diff (L,((i + 1) + 1),([#] E))) `| ([#] E) =
diff (
L,
((i + 2) + 1),
([#] E))
by NDIFF_6:13
.=
([#] E) --> (0. (diff_SP (((i + 1) + 2),E,F)))
by Th18
;
(diff (L,((i + 1) + 1),([#] E))) `| ([#] E) is_continuous_on [#] E
then A14:
dom ((diff (L,((i + 1) + 1),([#] E))) `| ([#] E)) = [#] E
by FUNCOP_1:13;
R_NormSpace_of_BoundedLinearOperators (
E,
(diff_SP ((i + 2),E,F)))
= diff_SP (
((i + 2) + 1),
E,
F)
by NDIFF_6:10;
then reconsider r =
0. (diff_SP (((i + 1) + 2),E,F)) as
Point of
(R_NormSpace_of_BoundedLinearOperators (E,(diff_SP ((i + 2),E,F)))) ;
rng ((diff (L,((i + 1) + 1),([#] E))) `| ([#] E)) = {r}
by A13, FUNCOP_1:8;
hence
(diff (L,((i + 1) + 1),([#] E))) `| ([#] E) is_continuous_on [#] E
by A14, NFCONT_1:47;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A2, A9);
hence
for i being Nat holds
( diff (L,(i + 1),([#] E)) is_differentiable_on [#] E & (diff (L,(i + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP ((i + 2),E,F))) & (diff (L,(i + 1),([#] E))) `| ([#] E) is_continuous_on [#] E )
; verum