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)
proof
let v,
u be
Element of
(RAlgebra X);
( 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) )
;
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;
verum
end;
then A9:
Ck_Functions (k,X) is add-closed
by IDEAL_1:def 1;
A10:
for v being Element of (RAlgebra X) st v in Ck_Functions (k,X) holds
- v in Ck_Functions (k,X)
proof
let v be
Element of
(RAlgebra X);
( v in Ck_Functions (k,X) implies - v in Ck_Functions (k,X) )
assume A11:
v in Ck_Functions (
k,
X)
;
- 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;
then
- v = - v1
by A12, A16, VALUED_1:9;
hence
- v in Ck_Functions (
k,
X)
by A14, A13;
verum
end;
for a being Real
for u being Element of (RAlgebra X) st u in Ck_Functions (k,X) holds
a * u in Ck_Functions (k,X)
proof
let a be
Real;
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);
( u in Ck_Functions (k,X) implies a * u in Ck_Functions (k,X) )
assume A17:
u in Ck_Functions (
k,
X)
;
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;
verum
end;
hence
Ck_Functions (k,X) is additively-linearly-closed
by A9, A10, C0SP1:def 1, C0SP1:def 10; Ck_Functions (k,X) is multiplicatively-closed
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
let v,
u be
Element of
(RAlgebra X);
( 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) )
;
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;
verum
end;
set g = RealFuncUnit 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; verum