let m be non zero Element of NAT ; :: thesis: 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
let k be Element of NAT ; :: thesis: for X being non empty open Subset of (REAL m) holds 0. (R_Algebra_of_Ck_Functions (k,X)) = X --> 0
let X be non empty open Subset of (REAL m); :: thesis: 0. (R_Algebra_of_Ck_Functions (k,X)) = X --> 0
0. (RAlgebra X) = X --> 0 ;
hence 0. (R_Algebra_of_Ck_Functions (k,X)) = X --> 0 by C0SP1:8; :: thesis: verum