let E, F be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of E,F
for i being Nat holds
( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E )
let L be Lipschitzian LinearOperator of E,F; :: thesis: for i being Nat holds
( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E )
let i be Nat; :: thesis: ( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E )

per cases ( i = 0 or i <> 0 ) ;

suppose A1: i = 0 ; :: thesis: ( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E )

then A2: diff (L,i,([#] E)) = L | ([#] E) by NDIFF_6:11
.= L ;
A3: (diff (L,i,([#] E))) `| ([#] E) = diff (L,(i + 1),([#] E)) by NDIFF_6:13
.= ([#] E) --> L by A1, Th16 ;
A4: diff_SP (0,E,F) = F by NDIFF_6:def 2;
hence diff (L,i,([#] E)) is_differentiable_on [#] E by A1, A2, FUNCT_2:def 1, NDIFF_7:26; :: thesis: (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E
A5: dom ((diff (L,i,([#] E))) `| ([#] E)) = [#] E by A3, FUNCOP_1:13;
reconsider r = L as Point of (R_NormSpace_of_BoundedLinearOperators (E,(diff_SP (0,E,F)))) by A4, LOPBAN_1:def 9;
rng ((diff (L,i,([#] E))) `| ([#] E)) = {r} by A3, FUNCOP_1:8;
hence (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E by A1, A5, NFCONT_1:47; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: ( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E )

then ex j being Nat st i = j + 1 by NAT_1:6;
hence ( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E ) by Th19; :: thesis: verum

end;

end;