let X be non empty set ; :: thesis:
let Y be ComplexNormSpace; :: thesis:
let f, g, h be VECTOR of (C_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: C_VectorSpace_of_BoundedFunctions X,Y is Subspace of ComplexVectSpace X,Y by Th8, CSSPACE:13;
then reconsider f1 = f as VECTOR of (ComplexVectSpace X,Y) by CLVECT_1:30;
reconsider g1 = g as VECTOR of (ComplexVectSpace X,Y) by A4, CLVECT_1:30;
reconsider h1 = h as VECTOR of (ComplexVectSpace X,Y) by A4, CLVECT_1:30;

A5: now

assume A6: h = f + g ; :: thesis:
let x be Element of X; :: thesis:
h1 = f1 + g1 by A4, A6, CLVECT_1:33;
hence h' . x = (f' . x) + (g' . x) by A1, A2, A3, CLOPBAN1:12; :: 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, CLOPBAN1:12;
hence h = f + g by A4, CLVECT_1:33; :: thesis:

end;

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