let E, F be RealNormSpace; :: thesis: for Z being non empty Subset of E
for L1 being PartFunc of E,F
for L0 being Point of F st Z is open & L1 = Z --> L0 holds
( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) )
let Z be non empty Subset of E; :: thesis: for L1 being PartFunc of E,F
for L0 being Point of F st Z is open & L1 = Z --> L0 holds
( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) )
let L1 be PartFunc of E,F; :: thesis: for L0 being Point of F st Z is open & L1 = Z --> L0 holds
( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) )
let L0 be Point of F; :: thesis: ( Z is open & L1 = Z --> L0 implies ( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) ) )
assume A1: ( Z is open & L1 = Z --> L0 ) ; :: thesis: ( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) )
A2: dom L1 = Z by A1, FUNCOP_1:13;
A3: rng L1 = {L0} by A1, FUNCOP_1:8;
then A4: ( L1 is_differentiable_on Z & ( for x being Point of E st x in Z holds
(L1 `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) ) ) by A1, A2, NDIFF_1:33;
A5: dom (L1 `| Z) = Z by A4, NDIFF_1:def 9;
A6: for z being object st z in dom (L1 `| Z) holds
(L1 `| Z) . z = 0. (R_NormSpace_of_BoundedLinearOperators (E,F))

proof

let z be object ; :: thesis: ( z in dom (L1 `| Z) implies (L1 `| Z) . z = 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) )
assume A7: z in dom (L1 `| Z) ; :: thesis: (L1 `| Z) . z = 0. (R_NormSpace_of_BoundedLinearOperators (E,F))
then reconsider x = z as Point of E ;
thus (L1 `| Z) . z = (L1 `| Z) /. x by PARTFUN1:def 6, A7
.= 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) by A1, A2, A3, A5, A7, NDIFF_1:33 ; :: thesis: verum

end;

then A8: L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) by A5, FUNCOP_1:11;
rng (L1 `| Z) = {(0. (R_NormSpace_of_BoundedLinearOperators (E,F)))} by A8, FUNCOP_1:8;
hence ( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) ) by A1, A2, A3, A5, A6, FUNCOP_1:11, NDIFF_1:33, NDIFF_1:45; :: thesis: verum