let X be non empty closed_interval Subset of REAL; :: thesis:
let Y be RealNormSpace; :: thesis:
let f, g, h be VECTOR of (R_VectorSpace_of_ContinuousFunctions (X,Y)); :: thesis:
A1: R_VectorSpace_of_ContinuousFunctions (X,Y) is Subspace of R_VectorSpace_of_BoundedFunctions (X,Y) by RSSPACE:11;
then reconsider f1 = f as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) by A1, RLSUB_1:10;
reconsider g1 = g as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) by A1, RLSUB_1:10;
let f9, g9, h9 be continuous PartFunc of REAL,Y; :: thesis:
assume A2: ( f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X ) ; :: thesis:
reconsider f90 = f1, g90 = g1, h90 = h1 as bounded Function of X,Y by RSSPACE4:def 5;

A3: now :: thesis:

assume A4: h = f + g ; :: thesis:
let x be Element of X; :: thesis:
A5: h1 = f1 + g1 by A1, A4, RLSUB_1:13;
thus h9 /. x = h90 . x by A2, PARTFUN1:def 6
.= (f90 /. x) + (g90 /. x) by A5, RSSPACE4:8
.= (f9 /. x) + (g9 /. x) by A2 ; :: thesis:

end;

now :: thesis:

assume A6: for x being Element of X holds h9 /. x = (f9 /. x) + (g9 /. x) ; :: thesis:

now :: thesis:

let x be Element of X; :: thesis:
thus h90 . x = h9 /. x by A2, PARTFUN1:def 6
.= (f90 /. x) + (g90 /. x) by A2, A6
.= (f90 . x) + (g90 . x) ; :: thesis:

end;

then h1 = f1 + g1 by RSSPACE4:8;
hence h = f + g by A1, RLSUB_1:13; :: thesis:

end;

hence ( h = f + g iff for x being Element of X holds h9 /. x = (f9 /. x) + (g9 /. x) ) by A3; :: thesis: