let X, Y be RealNormSpace; :: thesis: for Z being non empty open Subset of X
for n being non empty Nat
for v, u being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let Z be non empty open Subset of X; :: thesis: for n being non empty Nat
for v, u being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let n be non empty Nat; :: thesis: for v, u being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let v, u be VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)); :: thesis: for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let f, g be PartFunc of X,Y; :: thesis: for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let a be Real; :: thesis: ( dom f = Z & dom g = Z & v = f & u = g implies ( v + u = f + g & a * v = a (#) f ) )
assume A1: ( dom f = Z & dom g = Z & v = f & u = g ) ; :: thesis: ( v + u = f + g & a * v = a (#) f )
A2: RVectSp_Continuously_differentiable_Funcs (Z,Y,n) is Subspace of RealVectSpace (Z,Y) by Th5, RSSPACE:11;
reconsider v1 = v, u1 = u as VECTOR of (RealVectSpace (Z,Y)) by TARSKI:def 3;
thus v + u = v1 + u1 by RLSUB_1:13, A2
.= f + g by Th3, A1 ; :: thesis: a * v = a (#) f
thus a * v = a * v1 by RLSUB_1:14, A2
.= a (#) f by Th3, A1 ; :: thesis: verum