let E, F be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of E,F
for i being Nat holds diff (L,(i + 2),([#] E)) = ([#] E) --> (0. (diff_SP ((i + 2),E,F)))
let L be Lipschitzian LinearOperator of E,F; :: thesis: for i being Nat holds diff (L,(i + 2),([#] E)) = ([#] E) --> (0. (diff_SP ((i + 2),E,F)))
defpred S₁[ Nat] means diff (L,($1 + 2),([#] E)) = ([#] E) --> (0. (diff_SP (($1 + 2),E,F)));
A1: S₁[ 0 ]

proof

A2: 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 0. (diff_SP (2,E,F)) = ([#] E) --> (0. (diff_SP (1,E,F))) by LOPBAN_1:31
.= ([#] E) --> (([#] E) --> (0. F)) by A2, LOPBAN_1:31 ;
hence diff (L,(0 + 2),([#] E)) = ([#] E) --> (0. (diff_SP ((0 + 2),E,F))) by Th16; :: thesis: verum

end;

A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
set L1 = diff (L,(i + 2),([#] E));
A6: dom (diff (L,(i + 2),([#] E))) = [#] E by A5, FUNCOP_1:13;
A7: rng (diff (L,(i + 2),([#] E))) = {(0. (diff_SP ((i + 2),E,F)))} by A5, FUNCOP_1:8;
then ( diff (L,(i + 2),([#] E)) is_differentiable_on [#] E & ( for x being Point of E st x in [#] E holds
((diff (L,(i + 2),([#] E))) `| ([#] E)) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (E,(diff_SP ((i + 2),E,F)))) ) ) by A6, NDIFF_1:33;
then A9: dom ((diff (L,(i + 2),([#] E))) `| ([#] E)) = [#] E by NDIFF_1:def 9;
A10: for z being object st z in dom ((diff (L,(i + 2),([#] E))) `| ([#] E)) holds
((diff (L,(i + 2),([#] E))) `| ([#] E)) . z = 0. (diff_SP (((i + 2) + 1),E,F))

proof

let z be object ; :: thesis: ( z in dom ((diff (L,(i + 2),([#] E))) `| ([#] E)) implies ((diff (L,(i + 2),([#] E))) `| ([#] E)) . z = 0. (diff_SP (((i + 2) + 1),E,F)) )
assume A11: z in dom ((diff (L,(i + 2),([#] E))) `| ([#] E)) ; :: thesis: ((diff (L,(i + 2),([#] E))) `| ([#] E)) . z = 0. (diff_SP (((i + 2) + 1),E,F))
then reconsider x = z as Point of E ;
thus ((diff (L,(i + 2),([#] E))) `| ([#] E)) . z = ((diff (L,(i + 2),([#] E))) `| ([#] E)) /. x by A11, PARTFUN1:def 6
.= 0. (R_NormSpace_of_BoundedLinearOperators (E,(diff_SP ((i + 2),E,F)))) by A6, A7, NDIFF_1:33
.= 0. (diff_SP (((i + 2) + 1),E,F)) by NDIFF_6:10 ; :: thesis: verum

end;

thus diff (L,((i + 1) + 2),([#] E)) = diff (L,((i + 2) + 1),([#] E))
.= (diff (L,(i + 2),([#] E))) `| ([#] E) by NDIFF_6:13
.= ([#] E) --> (0. (diff_SP (((i + 1) + 2),E,F))) by A9, A10, FUNCOP_1:11 ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A4);
hence for i being Nat holds diff (L,(i + 2),([#] E)) = ([#] E) --> (0. (diff_SP ((i + 2),E,F))) ; :: thesis: verum