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

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