let X, Y be RealNormSpace; :: thesis: for Z being non empty open Subset of X
for n being non empty Nat holds Continuously_differentiable_Functions (Z,Y,n) is linearly-closed
let Z be non empty open Subset of X; :: thesis: for n being non empty Nat holds Continuously_differentiable_Functions (Z,Y,n) is linearly-closed
let n be non empty Nat; :: thesis: Continuously_differentiable_Functions (Z,Y,n) is linearly-closed
set W = Continuously_differentiable_Functions (Z,Y,n);
A0: n <> {} ;
then A1: 1 <= n by NAT_1:14;
A2: for v, u being VECTOR of (RealVectSpace (Z,Y)) st v in Continuously_differentiable_Functions (Z,Y,n) & u in Continuously_differentiable_Functions (Z,Y,n) holds
v + u in Continuously_differentiable_Functions (Z,Y,n)

proof

let v, u be VECTOR of (RealVectSpace (Z,Y)); :: thesis: ( v in Continuously_differentiable_Functions (Z,Y,n) & u in Continuously_differentiable_Functions (Z,Y,n) implies v + u in Continuously_differentiable_Functions (Z,Y,n) )
assume that
A3: v in Continuously_differentiable_Functions (Z,Y,n) and
A4: u in Continuously_differentiable_Functions (Z,Y,n) ; :: thesis: v + u in Continuously_differentiable_Functions (Z,Y,n)
consider f being PartFunc of X,Y such that
A5: ( f = v & dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) by A3;
consider g being PartFunc of X,Y such that
A6: ( g = u & dom g = Z & g is_differentiable_on n,Z & diff (g,n,Z) is_continuous_on Z ) by A4;
A7: dom (f + g) = (dom f) /\ (dom g) by VFUNCT_1:def 1
.= Z by A5, A6 ;
A8: v + u = f + g by A5, A6, Th3;
A9: f + g is_differentiable_on n,Z by A0, A5, A6, NAT_1:14, NDIFF_6:21;
diff ((f + g),n,Z) = (diff (f,n,Z)) + (diff (g,n,Z)) by A1, A5, A6, NDIFF_6:20;
then diff ((f + g),n,Z) is_continuous_on Z by A5, A6, NFCONT_1:25;
hence v + u in Continuously_differentiable_Functions (Z,Y,n) by A7, A8, A9; :: thesis: verum

end;

for a being Real
for v being VECTOR of (RealVectSpace (Z,Y)) st v in Continuously_differentiable_Functions (Z,Y,n) holds
a * v in Continuously_differentiable_Functions (Z,Y,n)

proof

let a be Real; :: thesis: for v being VECTOR of (RealVectSpace (Z,Y)) st v in Continuously_differentiable_Functions (Z,Y,n) holds
a * v in Continuously_differentiable_Functions (Z,Y,n)
let v be VECTOR of (RealVectSpace (Z,Y)); :: thesis: ( v in Continuously_differentiable_Functions (Z,Y,n) implies a * v in Continuously_differentiable_Functions (Z,Y,n) )
assume A10: v in Continuously_differentiable_Functions (Z,Y,n) ; :: thesis: a * v in Continuously_differentiable_Functions (Z,Y,n)
consider f being PartFunc of X,Y such that
A11: ( f = v & dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) by A10;
A12: dom (a (#) f) = Z by A11, VFUNCT_1:def 4;
A13: a * v = a (#) f by Th3, A11;
A14: a (#) f is_differentiable_on n,Z by A0, A11, NAT_1:14, NDIFF_6:25;
diff ((a (#) f),n,Z) = a (#) (diff (f,n,Z)) by A1, A11, NDIFF_6:24;
then diff ((a (#) f),n,Z) is_continuous_on Z by NFCONT_1:27, A11;
hence a * v in Continuously_differentiable_Functions (Z,Y,n) by A12, A13, A14; :: thesis: verum

end;

hence Continuously_differentiable_Functions (Z,Y,n) is linearly-closed by A2; :: thesis: verum