A1:
{ f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } c= Funcs (X,REAL)

dom (X --> 0) = X by FUNCT_2:def 1;

then reconsider g = X --> 0 as PartFunc of (REAL m),REAL by A3, RELSET_1:5;

A4: dom g = X by FUNCT_2:def 1;

g is_continuously_differentiable_up_to_order k,X by Th19;

then g in { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } by A4;

hence { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } is non empty Subset of (RAlgebra X) by A1; :: thesis: verum

proof

A3:
X --> 0 is Function of X,REAL
by XREAL_0:def 1, FUNCOP_1:45;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } or x in Funcs (X,REAL) )

assume x in { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ; :: thesis: x in Funcs (X,REAL)

then consider f being PartFunc of (REAL m),REAL such that

A2: ( x = f & f is_continuously_differentiable_up_to_order k,X & dom f = X ) ;

rng f c= REAL ;

then f is Function of X,REAL by A2, FUNCT_2:2;

hence x in Funcs (X,REAL) by A2, FUNCT_2:8; :: thesis: verum

end;assume x in { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ; :: thesis: x in Funcs (X,REAL)

then consider f being PartFunc of (REAL m),REAL such that

A2: ( x = f & f is_continuously_differentiable_up_to_order k,X & dom f = X ) ;

rng f c= REAL ;

then f is Function of X,REAL by A2, FUNCT_2:2;

hence x in Funcs (X,REAL) by A2, FUNCT_2:8; :: thesis: verum

dom (X --> 0) = X by FUNCT_2:def 1;

then reconsider g = X --> 0 as PartFunc of (REAL m),REAL by A3, RELSET_1:5;

A4: dom g = X by FUNCT_2:def 1;

g is_continuously_differentiable_up_to_order k,X by Th19;

then g in { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } by A4;

hence { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } is non empty Subset of (RAlgebra X) by A1; :: thesis: verum