let X be non empty set ; :: thesis:
let f, g, h be Function of X,COMPLEX; :: thesis:
let F, G, H be Point of (C_Normed_Algebra_of_BoundedFunctions X); :: thesis:
assume A1: ( f = F & g = G & h = H ) ; :: thesis:

A2: now :: thesis:

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

now :: thesis:

let x be Element of X; :: thesis:
h . x = (f . x) - (g . x) by A3;
hence (h . x) + (g . x) = f . x ; :: thesis:

end;

then F = H + G by A1, Th22;
then F - G = H + (G - G) by RLVECT_1:def 3;
then F - G = H + (0. (C_Normed_Algebra_of_BoundedFunctions X)) by RLVECT_1:15;
hence F - G = H by RLVECT_1:4; :: thesis:

end;

now :: thesis:

assume H = F - G ; :: thesis:
then H + G = F - (G - G) by RLVECT_1:29;
then H + G = F - (0. (C_Normed_Algebra_of_BoundedFunctions X)) by RLVECT_1:15;
then A4: H + G = F by RLVECT_1:13;

now :: thesis:

let x be Element of X; :: thesis:
f . x = (h . x) + (g . x) by A1, A4, Th22;
hence (f . x) - (g . x) = h . x ; :: thesis:

end;

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

end;

hence ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) by A2; :: thesis: