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)
proof
let x be
object ;
TARSKI:def 3 ( 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 ) }
;
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;
verum
end;
A3:
X --> 0 is Function of X,REAL
by XREAL_0:def 1, FUNCOP_1:45;
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; verum