let X, Y be RealNormSpace; :: thesis: for Z being non empty open Subset of X
for n being Nat
for f being PartFunc of X,Y holds
( f in Continuously_differentiable_Functions (Z,Y,n) iff ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) )
let Z be non empty open Subset of X; :: thesis: for n being Nat
for f being PartFunc of X,Y holds
( f in Continuously_differentiable_Functions (Z,Y,n) iff ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) )
let n be Nat; :: thesis: for f being PartFunc of X,Y holds
( f in Continuously_differentiable_Functions (Z,Y,n) iff ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) )
let f be PartFunc of X,Y; :: thesis: ( f in Continuously_differentiable_Functions (Z,Y,n) iff ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) )

hereby :: thesis: ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z implies f in Continuously_differentiable_Functions (Z,Y,n) )

assume f in Continuously_differentiable_Functions (Z,Y,n) ; :: thesis: ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z )
then ex f1 being PartFunc of X,Y st
( f = f1 & dom f1 = Z & f1 is_differentiable_on n,Z & diff (f1,n,Z) is_continuous_on Z ) ;
hence ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) ; :: thesis: verum

end;

assume ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) ; :: thesis: f in Continuously_differentiable_Functions (Z,Y,n)
hence f in Continuously_differentiable_Functions (Z,Y,n) ; :: thesis: verum