let F, G be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of F,G holds
( L is_differentiable_on [#] F & L `| ([#] F) is_continuous_on [#] F & ( for x being Point of F holds (L `| ([#] F)) /. x = L ) )
let L be Lipschitzian LinearOperator of F,G; :: thesis: ( L is_differentiable_on [#] F & L `| ([#] F) is_continuous_on [#] F & ( for x being Point of F holds (L `| ([#] F)) /. x = L ) )
A1: diff (L,0,([#] F)) = L | ([#] F) by NDIFF_6:11
.= L ;
(diff_SP (F,G)) . 0 = G by NDIFF_6:7;
hence A3: ( L is_differentiable_on [#] F & L `| ([#] F) is_continuous_on [#] F ) by A1, NDIFF12:20; :: thesis: for x being Point of F holds (L `| ([#] F)) /. x = L
let x be Point of F; :: thesis: (L `| ([#] F)) /. x = L
thus (L `| ([#] F)) /. x = diff (L,x) by A3, NDIFF_1:def 9
.= L by NDIFF_7:26 ; :: thesis: verum