:: deftheorem defines R_Algebra_of_Ck_Functions CKSPACE1:def 3 :
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 R_Algebra_of_Ck_Functions (k,X) = AlgebraStr(# (Ck_Functions (k,X)),(mult_ ((Ck_Functions (k,X)),(RAlgebra X))),(Add_ ((Ck_Functions (k,X)),(RAlgebra X))),(Mult_ ((Ck_Functions (k,X)),(RAlgebra X))),(One_ ((Ck_Functions (k,X)),(RAlgebra X))),(Zero_ ((Ck_Functions (k,X)),(RAlgebra X))) #);