let n be Nat; :: thesis: for E, F being RealNormSpace
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 n,Z & (diff (L1,n,Z)) `| Z is_continuous_on Z )
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 n,Z & (diff (L1,n,Z)) `| Z is_continuous_on Z )
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 n,Z & (diff (L1,n,Z)) `| Z is_continuous_on Z )
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 n,Z & (diff (L1,n,Z)) `| Z is_continuous_on Z )
let L0 be Point of F; :: thesis: ( Z is open & L1 = Z --> L0 implies ( L1 is_differentiable_on n,Z & (diff (L1,n,Z)) `| Z is_continuous_on Z ) )
assume A1: ( Z is open & L1 = Z --> L0 ) ; :: thesis: ( L1 is_differentiable_on n,Z & (diff (L1,n,Z)) `| Z is_continuous_on Z )
then A2: dom L1 = Z by FUNCOP_1:13;
for i being Nat st i <= n - 1 holds
diff (L1,i,Z) is_differentiable_on Z by A1, Th49;
hence L1 is_differentiable_on n,Z by A2, NDIFF_6:14; :: thesis: (diff (L1,n,Z)) `| Z is_continuous_on Z
thus (diff (L1,n,Z)) `| Z is_continuous_on Z by A1, Th49; :: thesis: verum