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 ; :: 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 ;
hence x in Funcs (X,REAL) by ; :: thesis: verum
end;
A3: X --> 0 is Function of X,REAL by ;
dom (X --> 0) = X by FUNCT_2:def 1;
then reconsider g = X --> 0 as PartFunc of (REAL m),REAL by ;
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 () by A1; :: thesis: verum