let n be Nat; :: thesis: for S being RealNormSpace
for Z being Subset of S
for f being PartFunc of S,S st Z is open & f = id ([#] S) holds
( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z )
let S be RealNormSpace; :: thesis: for Z being Subset of S
for f being PartFunc of S,S st Z is open & f = id ([#] S) holds
( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z )
let Z be Subset of S; :: thesis: for f being PartFunc of S,S st Z is open & f = id ([#] S) holds
( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z )
let f be PartFunc of S,S; :: thesis: ( Z is open & f = id ([#] S) implies ( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) )
assume A1: ( Z is open & f = id ([#] S) ) ; :: thesis: ( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z )
reconsider L = id ([#] S) as Lipschitzian LinearOperator of S,S by LOPBAN_2:3;
A2: dom L = [#] S ;
for i being Nat st i <= n - 1 holds
diff (L,i,([#] S)) is_differentiable_on [#] S by NDIFF12:20;
then A3: f is_differentiable_on n, [#] S by A1, A2, NDIFF_6:14;
diff (L,n,([#] S)) is_continuous_on [#] S by NDIFF_1:45, NDIFF12:20;
hence ( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) by A1, A3, Th10; :: thesis: verum