:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received November 9, 2012

:: Copyright (c) 2012-2018 Association of Mizar Users

definition

let m be non zero Element of NAT ;

let f be PartFunc of (REAL m),REAL;

let k be Nat;

let Z be set ;

end;
let f be PartFunc of (REAL m),REAL;

let k be Nat;

let Z be set ;

pred f is_continuously_differentiable_up_to_order k,Z means :: CKSPACE1:def 1

( Z c= dom f & f is_partial_differentiable_up_to_order k,Z & ( for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds

f `partial| (Z,I) is_continuous_on Z ) );

( Z c= dom f & f is_partial_differentiable_up_to_order k,Z & ( for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds

f `partial| (Z,I) is_continuous_on Z ) );

:: deftheorem defines is_continuously_differentiable_up_to_order CKSPACE1:def 1 :

for m being non zero Element of NAT

for f being PartFunc of (REAL m),REAL

for k being Nat

for Z being set holds

( f is_continuously_differentiable_up_to_order k,Z iff ( Z c= dom f & f is_partial_differentiable_up_to_order k,Z & ( for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds

f `partial| (Z,I) is_continuous_on Z ) ) );

for m being non zero Element of NAT

for f being PartFunc of (REAL m),REAL

for k being Nat

for Z being set holds

( f is_continuously_differentiable_up_to_order k,Z iff ( Z c= dom f & f is_partial_differentiable_up_to_order k,Z & ( for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds

f `partial| (Z,I) is_continuous_on Z ) ) );

theorem Th1: :: CKSPACE1:1

for m being non zero Element of NAT

for Z being set

for I being non empty FinSequence of NAT

for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,I holds

dom (f `partial| (Z,I)) = Z

for Z being set

for I being non empty FinSequence of NAT

for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,I holds

dom (f `partial| (Z,I)) = Z

proof end;

theorem Th2: :: CKSPACE1:2

for m being non zero Element of NAT

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds

( f is_continuously_differentiable_up_to_order 1,X iff ( f is_differentiable_on X & ( for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds

( f is_continuously_differentiable_up_to_order 1,X iff ( f is_differentiable_on X & ( for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )

proof end;

theorem Th3: :: CKSPACE1:3

for m being non zero Element of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL st X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X holds

f is_continuous_on X

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL st X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X holds

f is_continuous_on X

proof end;

theorem Th4: :: CKSPACE1:4

for m being non zero Element of NAT

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

proof end;

theorem Th5: :: CKSPACE1:5

for m being non zero Element of NAT

for k being Element of NAT

for X being non empty Subset of (REAL m)

for r being Real

for f being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & X is open holds

r (#) f is_continuously_differentiable_up_to_order k,X

for k being Element of NAT

for X being non empty Subset of (REAL m)

for r being Real

for f being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & X is open holds

r (#) f is_continuously_differentiable_up_to_order k,X

proof end;

theorem :: CKSPACE1:6

for m being non zero Element of NAT

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f - g is_continuously_differentiable_up_to_order k,X

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f - g is_continuously_differentiable_up_to_order k,X

proof end;

theorem Th7: :: CKSPACE1:7

for m being non zero Element of NAT

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds

f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I)

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds

f `partial| (Z,(G ^ I)) = (f `partial| (Z,G)) `partial| (Z,I)

proof end;

theorem :: CKSPACE1:8

for m being non zero Element of NAT

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds

( f `partial| (Z,(G ^ I)) is_continuous_on Z iff (f `partial| (Z,G)) `partial| (Z,I) is_continuous_on Z ) by Th7;

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds

( f `partial| (Z,(G ^ I)) is_continuous_on Z iff (f `partial| (Z,G)) `partial| (Z,I) is_continuous_on Z ) by Th7;

theorem Th9: :: CKSPACE1:9

for m being non zero Element of NAT

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for i, j being Nat

for I being non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds

f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for i, j being Nat

for I being non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds

f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z

proof end;

theorem Th10: :: CKSPACE1:10

for m being non zero Element of NAT

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for i, j being Nat st f is_continuously_differentiable_up_to_order i,Z & j <= i holds

f is_continuously_differentiable_up_to_order j,Z by PDIFF_9:84, XXREAL_0:2;

for Z being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for i, j being Nat st f is_continuously_differentiable_up_to_order i,Z & j <= i holds

f is_continuously_differentiable_up_to_order j,Z by PDIFF_9:84, XXREAL_0:2;

theorem Th11: :: CKSPACE1:11

for m being non zero Element of NAT

for Z being non empty Subset of (REAL m) st Z is open holds

for k being Element of NAT

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,Z & g is_continuously_differentiable_up_to_order k,Z holds

f (#) g is_continuously_differentiable_up_to_order k,Z

for Z being non empty Subset of (REAL m) st Z is open holds

for k being Element of NAT

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,Z & g is_continuously_differentiable_up_to_order k,Z holds

f (#) g is_continuously_differentiable_up_to_order k,Z

proof end;

theorem Th12: :: CKSPACE1:12

for m being non zero Element of NAT

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d holds

for x being Element of REAL m st x in X holds

( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d holds

for x being Element of REAL m st x in X holds

( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )

proof end;

theorem Th13: :: CKSPACE1:13

for m being non zero Element of NAT

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d holds

for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d holds

for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

proof end;

theorem Th14: :: CKSPACE1:14

for m being non zero Element of NAT

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d holds

( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds

(f `| X) /. x = (REAL m) --> 0 ) )

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d holds

( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds

(f `| X) /. x = (REAL m) --> 0 ) )

proof end;

theorem Th15: :: CKSPACE1:15

for m being non zero Element of NAT

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

proof end;

theorem Th16: :: CKSPACE1:16

for m being non zero Element of NAT

for i being Element of NAT

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d & 1 <= i & i <= m holds

f `partial| (X,i) = X --> 0

for i being Element of NAT

for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d & 1 <= i & i <= m holds

f `partial| (X,i) = X --> 0

proof end;

Lm1: for m being non zero Element of NAT

for I being non empty FinSequence of NAT

for i being Element of NAT st rng I c= Seg m & i <= (len I) - 1 holds

( 1 <= I /. (i + 1) & I /. (i + 1) <= m )

proof end;

Lm2: for m being non zero Element of NAT

for I being non empty FinSequence of NAT

for i being Element of NAT st rng I c= Seg m & 1 <= i & i <= len I holds

( 1 <= I /. i & I /. i <= m )

proof end;

theorem Th17: :: CKSPACE1:17

for m being non zero Element of NAT

for I being non empty FinSequence of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg m holds

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

for I being non empty FinSequence of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg m holds

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

proof end;

theorem Th18: :: CKSPACE1:18

for m being non zero Element of NAT

for I being non empty FinSequence of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg m holds

( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )

for I being non empty FinSequence of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg m holds

( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )

proof end;

theorem Th19: :: CKSPACE1:19

for m being non zero Element of NAT

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d holds

f is_continuously_differentiable_up_to_order k,X

for k being Element of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d holds

f is_continuously_differentiable_up_to_order k,X

proof end;

registration

let m be non zero Element of NAT ;

correctness

existence

ex b_{1} being non empty Subset of (REAL m) st b_{1} is open ;

end;
correctness

existence

ex b

proof end;

definition

let m be non zero Element of NAT ;

let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

coherence

{ f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } is non empty Subset of (RAlgebra X);

end;
let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

func Ck_Functions (k,X) -> non empty Subset of (RAlgebra X) equals :: CKSPACE1:def 2

{ f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ;

correctness { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ;

coherence

{ f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } is non empty Subset of (RAlgebra X);

proof end;

:: deftheorem defines Ck_Functions CKSPACE1:def 2 :

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 Ck_Functions (k,X) = { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ;

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 Ck_Functions (k,X) = { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ;

registration

let m be non zero Element of NAT ;

let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

coherence

( Ck_Functions (k,X) is additively-linearly-closed & Ck_Functions (k,X) is multiplicatively-closed )

end;
let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

coherence

( Ck_Functions (k,X) is additively-linearly-closed & Ck_Functions (k,X) is multiplicatively-closed )

proof end;

definition

let m be non zero Element of NAT ;

let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

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))) #) is Subalgebra of RAlgebra X by C0SP1:6;

end;
let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

func R_Algebra_of_Ck_Functions (k,X) -> Subalgebra of RAlgebra X equals :: CKSPACE1:def 3

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))) #);

coherence 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))) #);

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))) #) is Subalgebra of RAlgebra X by C0SP1:6;

:: 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))) #);

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))) #);

registration

let m be non zero Element of NAT ;

let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

( R_Algebra_of_Ck_Functions (k,X) is Abelian & R_Algebra_of_Ck_Functions (k,X) is add-associative & R_Algebra_of_Ck_Functions (k,X) is right_zeroed & R_Algebra_of_Ck_Functions (k,X) is right_complementable & R_Algebra_of_Ck_Functions (k,X) is vector-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is scalar-unital & R_Algebra_of_Ck_Functions (k,X) is commutative & R_Algebra_of_Ck_Functions (k,X) is associative & R_Algebra_of_Ck_Functions (k,X) is right_unital & R_Algebra_of_Ck_Functions (k,X) is right-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is vector-associative )

end;
let k be Element of NAT ;

let X be non empty open Subset of (REAL m);

cluster R_Algebra_of_Ck_Functions (k,X) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital right-distributive right_unital associative commutative vector-associative ;

coherence ( R_Algebra_of_Ck_Functions (k,X) is Abelian & R_Algebra_of_Ck_Functions (k,X) is add-associative & R_Algebra_of_Ck_Functions (k,X) is right_zeroed & R_Algebra_of_Ck_Functions (k,X) is right_complementable & R_Algebra_of_Ck_Functions (k,X) is vector-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is scalar-unital & R_Algebra_of_Ck_Functions (k,X) is commutative & R_Algebra_of_Ck_Functions (k,X) is associative & R_Algebra_of_Ck_Functions (k,X) is right_unital & R_Algebra_of_Ck_Functions (k,X) is right-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is vector-associative )

proof end;

theorem :: CKSPACE1:20

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 st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

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 st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

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) )

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) )

proof end;

theorem :: CKSPACE1:22

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 st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

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 st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem :: CKSPACE1:23

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 0. (R_Algebra_of_Ck_Functions (k,X)) = X --> 0

for k being Element of NAT

for X being non empty open Subset of (REAL m) holds 0. (R_Algebra_of_Ck_Functions (k,X)) = X --> 0

proof end;

theorem :: CKSPACE1:24

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 1_ (R_Algebra_of_Ck_Functions (k,X)) = X --> 1

for k being Element of NAT

for X being non empty open Subset of (REAL m) holds 1_ (R_Algebra_of_Ck_Functions (k,X)) = X --> 1

proof end;