let X be non empty set ; :: thesis:
let Y be RealNormSpace; :: thesis:
let f, g, h be VECTOR of (R_VectorSpace_of_BoundedFunctions X,Y); :: thesis:
let f', g', h' be bounded Function of X,the carrier of Y; :: thesis:
assume that
A1: f' = f and
A2: g' = g and
A3: h' = h ; :: thesis:
A4: R_VectorSpace_of_BoundedFunctions X,Y is Subspace of RealVectSpace X,Y by Th7, RSSPACE:13;
then reconsider f1 = f as VECTOR of (RealVectSpace X,Y) by RLSUB_1:18;
reconsider g1 = g as VECTOR of (RealVectSpace X,Y) by A4, RLSUB_1:18;
reconsider h1 = h as VECTOR of (RealVectSpace X,Y) by A4, RLSUB_1:18;

A5: now

assume A6: h = f + g ; :: thesis:
let x be Element of X; :: thesis:
h1 = f1 + g1 by A4, A6, RLSUB_1:21;
hence h' . x = (f' . x) + (g' . x) by A1, A2, A3, LOPBAN_1:14; :: thesis:

end;

now

assume for x being Element of X holds h' . x = (f' . x) + (g' . x) ; :: thesis:
then h1 = f1 + g1 by A1, A2, A3, LOPBAN_1:14;
hence h = f + g by A4, RLSUB_1:21; :: thesis:

end;

hence ( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) ) by A5; :: thesis: