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