let X be non empty set ; :: thesis: for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )
let Y be ComplexNormSpace; :: thesis: for f, g, h being Point of (C_NormSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )
let f, g, h be Point of (C_NormSpace_of_BoundedFunctions X,Y); :: thesis: for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )
reconsider f1 = f, g1 = g, h1 = h as VECTOR of (C_VectorSpace_of_BoundedFunctions X,Y) ;
A1: ( h = f + g iff h1 = f1 + g1 ) ;
let f', g', h' be bounded Function of X,the carrier of Y; :: thesis: ( f' = f & g' = g & h' = h implies ( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) ) )
assume ( f' = f & g' = g & h' = h ) ; :: thesis: ( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )
hence ( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) ) by A1, Th11; :: thesis: verum