let X be non empty set ; :: thesis: for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) 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 Function of X,REAL ; :: thesis: for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) 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 (R_Normed_Algebra_of_BoundedFunctions X); :: 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 A1: ( f = F & g = G & 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. (R_Normed_Algebra_of_BoundedFunctions X)) 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, A5, ThB22;
hence (f . x) - (g . x) = h . x ; :: 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;
hence (h . x) + (g . x) = f . x ; :: thesis: verum

end;

then F = H + G by A1, ThB22;
then F - G = H + (G - G) by RLVECT_1:def 6;
then F - G = H + (0. (R_Normed_Algebra_of_BoundedFunctions X)) 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