let E, F be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of E,F holds
( (diff (L,([#] E))) . 0 = L & (diff (L,([#] E))) . 1 = ([#] E) --> L & (diff (L,([#] E))) . 2 = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) & (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F)))) )
let L be Lipschitzian LinearOperator of E,F; :: thesis: ( (diff (L,([#] E))) . 0 = L & (diff (L,([#] E))) . 1 = ([#] E) --> L & (diff (L,([#] E))) . 2 = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) & (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F)))) )
thus (diff (L,([#] E))) . 0 = L | ([#] E) by NDIFF_6:11
.= L ; :: thesis: ( (diff (L,([#] E))) . 1 = ([#] E) --> L & (diff (L,([#] E))) . 2 = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) & (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F)))) )
A2: L is_differentiable_on [#] E by FUNCT_2:def 1, NDIFF_7:26;
then A3: dom (L `| ([#] E)) = [#] E by NDIFF_1:def 9;
A4: L is Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) by LOPBAN_1:def 9;
A5: for z being object st z in dom (L `| ([#] E)) holds
(L `| ([#] E)) . z = L

proof

let z be object ; :: thesis: ( z in dom (L `| ([#] E)) implies (L `| ([#] E)) . z = L )
assume A6: z in dom (L `| ([#] E)) ; :: thesis: (L `| ([#] E)) . z = L
then reconsider x = z as Point of E ;
thus (L `| ([#] E)) . z = (L `| ([#] E)) /. x by A6, PARTFUN1:def 6
.= diff (L,x) by A2, NDIFF_1:def 9
.= L by NDIFF_7:26 ; :: thesis: verum

end;

then L `| ([#] E) = ([#] E) --> L by A3, FUNCOP_1:11;
then A7: rng (L `| ([#] E)) = {L} by FUNCOP_1:8;
then A8: ( L `| ([#] E) is_differentiable_on [#] E & ( for x being Point of E st x in [#] E holds
((L `| ([#] E)) `| ([#] E)) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,F)))) ) ) by A3, A4, NDIFF_1:33;
A9: 0. (R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,F)))) = ([#] E) --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) by LOPBAN_1:31
.= ([#] E) --> (([#] E) --> (0. F)) by LOPBAN_1:31 ;
A10: dom ((L `| ([#] E)) `| ([#] E)) = [#] E by A8, NDIFF_1:def 9;
A11: for z being object st z in dom ((L `| ([#] E)) `| ([#] E)) holds
((L `| ([#] E)) `| ([#] E)) . z = ([#] E) --> (([#] E) --> (0. F))

proof

let z be object ; :: thesis: ( z in dom ((L `| ([#] E)) `| ([#] E)) implies ((L `| ([#] E)) `| ([#] E)) . z = ([#] E) --> (([#] E) --> (0. F)) )
assume A12: z in dom ((L `| ([#] E)) `| ([#] E)) ; :: thesis: ((L `| ([#] E)) `| ([#] E)) . z = ([#] E) --> (([#] E) --> (0. F))
then reconsider x = z as Point of E ;
thus ((L `| ([#] E)) `| ([#] E)) . z = ((L `| ([#] E)) `| ([#] E)) /. x by A12, PARTFUN1:def 6
.= ([#] E) --> (([#] E) --> (0. F)) by A3, A4, A7, A9, NDIFF_1:33 ; :: thesis: verum

end;

thus (diff (L,([#] E))) . 1 = (L | ([#] E)) `| ([#] E) by NDIFF_6:11
.= ([#] E) --> L by A3, A5, FUNCOP_1:11 ; :: thesis: ( (diff (L,([#] E))) . 2 = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) & (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F)))) )
thus A13: (diff (L,([#] E))) . 2 = ((L | ([#] E)) `| ([#] E)) `| ([#] E) by NDIFF_6:11
.= ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) by A10, A11, FUNCOP_1:11 ; :: thesis: (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F))))
A14: diff_SP (2,E,F) = R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,F))) by NDIFF_6:7;
then reconsider L1 = (diff (L,([#] E))) . 2 as PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,F)))) by NDIFF_6:12;
A15: (diff (L,([#] E))) . 3 = (diff (L,([#] E))) . (2 + 1)
.= (modetrans (((diff (L,([#] E))) . 2),E,(diff_SP (2,E,F)))) `| ([#] E) by NDIFF_6:def 5
.= L1 `| ([#] E) by A14, NDIFF_6:def 4 ;
A16: dom L1 = [#] E by A13, FUNCOP_1:13;
A17: rng L1 = {(([#] E) --> (([#] E) --> (0. F)))} by A13, FUNCOP_1:8;
then A18: ( L1 is_differentiable_on [#] E & ( for x being Point of E st x in [#] E holds
(L1 `| ([#] E)) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,F)))))) ) ) by A9, A16, NDIFF_1:33;
A19: dom (L1 `| ([#] E)) = [#] E by A18, NDIFF_1:def 9;
A20: 0. (R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,(R_NormSpace_of_BoundedLinearOperators (E,F)))))) = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) by A9, LOPBAN_1:31;
for z being object st z in dom (L1 `| ([#] E)) holds
(L1 `| ([#] E)) . z = ([#] E) --> (([#] E) --> (([#] E) --> (0. F)))

proof

let z be object ; :: thesis: ( z in dom (L1 `| ([#] E)) implies (L1 `| ([#] E)) . z = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) )
assume A21: z in dom (L1 `| ([#] E)) ; :: thesis: (L1 `| ([#] E)) . z = ([#] E) --> (([#] E) --> (([#] E) --> (0. F)))
then reconsider x = z as Point of E ;
thus (L1 `| ([#] E)) . z = (L1 `| ([#] E)) /. x by A21, PARTFUN1:def 6
.= ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) by A9, A17, A16, A20, NDIFF_1:33 ; :: thesis: verum

end;

hence (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F)))) by A15, A19, FUNCOP_1:11; :: thesis: verum