set W = Ck_Functions (k,X);
set V = RAlgebra X;
A1: RAlgebra X is RealLinearSpace by C0SP1:7;
for v, u being Element of () st v in Ck_Functions (k,X) & u in Ck_Functions (k,X) holds
v + u in Ck_Functions (k,X)
proof
let v, u be Element of (); :: thesis: ( v in Ck_Functions (k,X) & u in Ck_Functions (k,X) implies v + u in Ck_Functions (k,X) )
assume A2: ( v in Ck_Functions (k,X) & u in Ck_Functions (k,X) ) ; :: thesis: v + u in Ck_Functions (k,X)
consider v1 being PartFunc of (REAL m),REAL such that
A3: ( v1 = v & v1 is_continuously_differentiable_up_to_order k,X & dom v1 = X ) by A2;
consider u1 being PartFunc of (REAL m),REAL such that
A4: ( u1 = u & u1 is_continuously_differentiable_up_to_order k,X & dom u1 = X ) by A2;
A5: dom (v1 + u1) = (dom v1) /\ (dom u1) by VALUED_1:def 1;
A6: v1 + u1 is_continuously_differentiable_up_to_order k,X by A3, A4, Th4;
reconsider h = v + u as Element of Funcs (X,REAL) ;
A7: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
A8: (dom v1) /\ (dom u1) = X /\ X by A4, A3;
for x being object st x in dom h holds
h . x = (v1 . x) + (u1 . x) by ;
then v + u = v1 + u1 by ;
hence v + u in Ck_Functions (k,X) by A6, A3, A4, A5; :: thesis: verum
end;
then A9: Ck_Functions (k,X) is add-closed by IDEAL_1:def 1;
A10: for v being Element of () st v in Ck_Functions (k,X) holds
- v in Ck_Functions (k,X)
proof
let v be Element of (); :: thesis: ( v in Ck_Functions (k,X) implies - v in Ck_Functions (k,X) )
assume A11: v in Ck_Functions (k,X) ; :: thesis: - v in Ck_Functions (k,X)
consider v1 being PartFunc of (REAL m),REAL such that
A12: ( v1 = v & v1 is_continuously_differentiable_up_to_order k,X & dom v1 = X ) by A11;
A13: dom (- v1) = X by ;
A14: - v1 is_continuously_differentiable_up_to_order k,X by ;
reconsider h = - v, v2 = v as Element of Funcs (X,REAL) ;
A15: h = (- 1) * v by ;
A16: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
now :: thesis: for x being object st x in dom h holds
h . x = - (v1 . x)
let x be object ; :: thesis: ( x in dom h implies h . x = - (v1 . x) )
assume x in dom h ; :: thesis: h . x = - (v1 . x)
then reconsider y = x as Element of X ;
h . x = (- 1) * (v2 . y) by ;
hence h . x = - (v1 . x) by A12; :: thesis: verum
end;
then - v = - v1 by ;
hence - v in Ck_Functions (k,X) by ; :: thesis: verum
end;
for a being Real
for u being Element of () st u in Ck_Functions (k,X) holds
a * u in Ck_Functions (k,X)
proof
let a be Real; :: thesis: for u being Element of () st u in Ck_Functions (k,X) holds
a * u in Ck_Functions (k,X)

let u be Element of (); :: thesis: ( u in Ck_Functions (k,X) implies a * u in Ck_Functions (k,X) )
assume A17: u in Ck_Functions (k,X) ; :: thesis: a * u in Ck_Functions (k,X)
consider u1 being PartFunc of (REAL m),REAL such that
A18: ( u1 = u & u1 is_continuously_differentiable_up_to_order k,X & dom u1 = X ) by A17;
A19: dom (a (#) u1) = X by ;
A20: a (#) u1 is_continuously_differentiable_up_to_order k,X by ;
reconsider h = a * u as Element of Funcs (X,REAL) ;
A21: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
for x being object st x in dom h holds
h . x = a * (u1 . x) by ;
then a * u = a (#) u1 by ;
hence a * u in Ck_Functions (k,X) by ; :: thesis: verum
end;
hence Ck_Functions (k,X) is additively-linearly-closed by ; :: thesis:
A22: for v, u being Element of () st v in Ck_Functions (k,X) & u in Ck_Functions (k,X) holds
v * u in Ck_Functions (k,X)
proof
let v, u be Element of (); :: thesis: ( v in Ck_Functions (k,X) & u in Ck_Functions (k,X) implies v * u in Ck_Functions (k,X) )
assume A23: ( v in Ck_Functions (k,X) & u in Ck_Functions (k,X) ) ; :: thesis: v * u in Ck_Functions (k,X)
consider v1 being PartFunc of (REAL m),REAL such that
A24: ( v1 = v & v1 is_continuously_differentiable_up_to_order k,X & dom v1 = X ) by A23;
consider u1 being PartFunc of (REAL m),REAL such that
A25: ( u1 = u & u1 is_continuously_differentiable_up_to_order k,X & dom u1 = X ) by A23;
A26: dom (v1 (#) u1) = (dom v1) /\ (dom u1) by VALUED_1:def 4
.= X by ;
A27: v1 (#) u1 is_continuously_differentiable_up_to_order k,X by ;
reconsider h = v * u as Element of Funcs (X,REAL) ;
A28: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
A29: (dom v1) /\ (dom u1) = X /\ X by ;
for x being object st x in dom h holds
h . x = (v1 . x) * (u1 . x) by ;
then v * u = v1 (#) u1 by ;
hence v * u in Ck_Functions (k,X) by ; :: thesis: verum
end;
set g = RealFuncUnit X;
dom () = X by FUNCT_2:def 1;
then reconsider g = RealFuncUnit X as PartFunc of (REAL m),REAL by RELSET_1:5;
A30: dom g = X by FUNCT_2:def 1;
g is_continuously_differentiable_up_to_order k,X by Th19;
then 1. () in Ck_Functions (k,X) by A30;
hence Ck_Functions (k,X) is multiplicatively-closed by ; :: thesis: verum