theorem :: CKSPACE1:23

for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds 0. (R_Algebra_of_Ck_Functions (k,X)) = X --> 0