let X, Y be RealNormSpace; :: thesis: for Z being non empty open Subset of X
for n being non empty Nat holds 0. (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) = Z --> (0. Y)
let Z be non empty open Subset of X; :: thesis: for n being non empty Nat holds 0. (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) = Z --> (0. Y)
let n be non empty Nat; :: thesis: 0. (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) = Z --> (0. Y)
A1: 0. (RealVectSpace (Z,Y)) = Z --> (0. Y) ;
RVectSp_Continuously_differentiable_Funcs (Z,Y,n) is Subspace of RealVectSpace (Z,Y) by Th5, RSSPACE:11;
hence 0. (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) = Z --> (0. Y) by A1, RLSUB_1:11; :: thesis: verum