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) )
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 that
A1: f' = f and
A2: g' = g and
A3: h' = h ; :: thesis: ( h = f - g iff for x being Element of X holds h' . x = (f' . x) - (g' . x) )

A4: now

assume h = f - g ; :: thesis: for x being Element of X holds h' . x = (f' . x) - (g' . x)
then h + g = f - (g - g) by RLVECT_1:43;
then h + g = f - (0. (C_NormSpace_of_BoundedFunctions X,Y)) by RLVECT_1:28;
then A5: h + g = f by RLVECT_1:26;

now

let x be Element of X; :: thesis: (f' . x) - (g' . x) = h' . x
f' . x = (h' . x) + (g' . x) by A1, A2, A3, A5, Th23;
then (f' . x) - (g' . x) = (h' . x) + ((g' . x) - (g' . x)) by RLVECT_1:def 6;
then (f' . x) - (g' . x) = (h' . x) + (0. Y) by RLVECT_1:28;
hence (f' . x) - (g' . x) = h' . x by RLVECT_1:10; :: thesis: verum

end;

hence for x being Element of X holds h' . x = (f' . x) - (g' . x) ; :: thesis: verum

end;

now

assume A6: for x being Element of X holds h' . x = (f' . x) - (g' . x) ; :: thesis: f - g = h

now

let x be Element of X; :: thesis: (h' . x) + (g' . x) = f' . x
h' . x = (f' . x) - (g' . x) by A6;
then (h' . x) + (g' . x) = (f' . x) - ((g' . x) - (g' . x)) by RLVECT_1:43;
then (h' . x) + (g' . x) = (f' . x) - (0. Y) by RLVECT_1:28;
hence (h' . x) + (g' . x) = f' . x by RLVECT_1:26; :: thesis: verum

end;

then f = h + g by A1, A2, A3, Th23;
then f - g = h + (g - g) by RLVECT_1:def 6;
then f - g = h + (0. (C_NormSpace_of_BoundedFunctions X,Y)) by RLVECT_1:28;
hence f - g = h by RLVECT_1:10; :: thesis: verum

end;

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