theorem :: CKSPACE1:21

for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m)
for F, G, H being VECTOR of (R_Algebra_of_Ck_Functions (k,X))
for f, g, h being PartFunc of (REAL m),REAL
for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )