set W = Ck_Functions (k,X);

set V = RAlgebra X;

A1: RAlgebra X is RealLinearSpace by C0SP1:7;

for v, u being Element of (RAlgebra X) st v in Ck_Functions (k,X) & u in Ck_Functions (k,X) holds

v + u in Ck_Functions (k,X)

A10: for v being Element of (RAlgebra X) st v in Ck_Functions (k,X) holds

- v in Ck_Functions (k,X)

for u being Element of (RAlgebra X) st u in Ck_Functions (k,X) holds

a * u in Ck_Functions (k,X)

A22: for v, u being Element of (RAlgebra X) st v in Ck_Functions (k,X) & u in Ck_Functions (k,X) holds

v * u in Ck_Functions (k,X)

dom (RealFuncUnit X) = 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. (RAlgebra X) in Ck_Functions (k,X) by A30;

hence Ck_Functions (k,X) is multiplicatively-closed by A22, C0SP1:def 4; :: thesis: verum

set V = RAlgebra X;

A1: RAlgebra X is RealLinearSpace by C0SP1:7;

for v, u being Element of (RAlgebra X) st v in Ck_Functions (k,X) & u in Ck_Functions (k,X) holds

v + u in Ck_Functions (k,X)

proof

then A9:
Ck_Functions (k,X) is add-closed
by IDEAL_1:def 1;
let v, u be Element of (RAlgebra X); :: 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 A3, A4, FUNCSDOM:1;

then v + u = v1 + u1 by A8, A7, VALUED_1:def 1;

hence v + u in Ck_Functions (k,X) by A6, A3, A4, A5; :: thesis: verum

end;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 A3, A4, FUNCSDOM:1;

then v + u = v1 + u1 by A8, A7, VALUED_1:def 1;

hence v + u in Ck_Functions (k,X) by A6, A3, A4, A5; :: thesis: verum

A10: for v being Element of (RAlgebra X) st v in Ck_Functions (k,X) holds

- v in Ck_Functions (k,X)

proof

for a being Real
let v be Element of (RAlgebra X); :: 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 VALUED_1:def 5, A12;

A14: - v1 is_continuously_differentiable_up_to_order k,X by A12, Th5;

reconsider h = - v, v2 = v as Element of Funcs (X,REAL) ;

A15: h = (- 1) * v by A1, RLVECT_1:16;

A16: ex f being Function st

( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;

hence - v in Ck_Functions (k,X) by A14, A13; :: thesis: verum

end;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 VALUED_1:def 5, A12;

A14: - v1 is_continuously_differentiable_up_to_order k,X by A12, Th5;

reconsider h = - v, v2 = v as Element of Funcs (X,REAL) ;

A15: h = (- 1) * v by A1, RLVECT_1:16;

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)

then
- v = - v1
by A12, A16, VALUED_1:9;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 A15, FUNCSDOM:4;

hence h . x = - (v1 . x) by A12; :: thesis: verum

end;assume x in dom h ; :: thesis: h . x = - (v1 . x)

then reconsider y = x as Element of X ;

h . x = (- 1) * (v2 . y) by A15, FUNCSDOM:4;

hence h . x = - (v1 . x) by A12; :: thesis: verum

hence - v in Ck_Functions (k,X) by A14, A13; :: thesis: verum

for u being Element of (RAlgebra X) st u in Ck_Functions (k,X) holds

a * u in Ck_Functions (k,X)

proof

hence
Ck_Functions (k,X) is additively-linearly-closed
by A9, A10, C0SP1:def 1, C0SP1:def 10; :: thesis: Ck_Functions (k,X) is multiplicatively-closed
let a be Real; :: thesis: for u being Element of (RAlgebra X) st u in Ck_Functions (k,X) holds

a * u in Ck_Functions (k,X)

let u be Element of (RAlgebra X); :: 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 A18, VALUED_1:def 5;

A20: a (#) u1 is_continuously_differentiable_up_to_order k,X by A18, Th5;

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 A18, FUNCSDOM:4;

then a * u = a (#) u1 by A18, A21, VALUED_1:def 5;

hence a * u in Ck_Functions (k,X) by A20, A19; :: thesis: verum

end;a * u in Ck_Functions (k,X)

let u be Element of (RAlgebra X); :: 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 A18, VALUED_1:def 5;

A20: a (#) u1 is_continuously_differentiable_up_to_order k,X by A18, Th5;

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 A18, FUNCSDOM:4;

then a * u = a (#) u1 by A18, A21, VALUED_1:def 5;

hence a * u in Ck_Functions (k,X) by A20, A19; :: thesis: verum

A22: for v, u being Element of (RAlgebra X) st v in Ck_Functions (k,X) & u in Ck_Functions (k,X) holds

v * u in Ck_Functions (k,X)

proof

set g = RealFuncUnit X;
let v, u be Element of (RAlgebra X); :: 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 A24, A25 ;

A27: v1 (#) u1 is_continuously_differentiable_up_to_order k,X by A24, A25, Th11;

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 A25, A24;

for x being object st x in dom h holds

h . x = (v1 . x) * (u1 . x) by A24, A25, FUNCSDOM:2;

then v * u = v1 (#) u1 by A29, A28, VALUED_1:def 4;

hence v * u in Ck_Functions (k,X) by A27, A26; :: thesis: verum

end;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 A24, A25 ;

A27: v1 (#) u1 is_continuously_differentiable_up_to_order k,X by A24, A25, Th11;

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 A25, A24;

for x being object st x in dom h holds

h . x = (v1 . x) * (u1 . x) by A24, A25, FUNCSDOM:2;

then v * u = v1 (#) u1 by A29, A28, VALUED_1:def 4;

hence v * u in Ck_Functions (k,X) by A27, A26; :: thesis: verum

dom (RealFuncUnit X) = 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. (RAlgebra X) in Ck_Functions (k,X) by A30;

hence Ck_Functions (k,X) is multiplicatively-closed by A22, C0SP1:def 4; :: thesis: verum