let X be non empty set ; :: thesis: for f, g, h being Function of X,COMPLEX

for F, G, H being Point of (C_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,COMPLEX; :: thesis: for F, G, H being Point of (C_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 (C_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) )

for F, G, H being Point of (C_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,COMPLEX; :: thesis: for F, G, H being Point of (C_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 (C_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) )

A2: now :: thesis: ( ( for x being Element of X holds h . x = (f . x) - (g . x) ) implies F - G = H )

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

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: verum

end;now :: thesis: for x being Element of X holds (h . x) + (g . x) = f . x

then
F = H + G
by A1, Th22;let x be Element of X; :: thesis: (h . x) + (g . x) = f . x

h . x = (f . x) - (g . x) by A3;

hence (h . x) + (g . x) = f . x ; :: thesis: verum

end;h . x = (f . x) - (g . x) by A3;

hence (h . x) + (g . x) = f . x ; :: thesis: verum

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: verum

now :: thesis: ( H = F - G implies 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 A2; :: thesis: verumassume
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: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;

end;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: for x being Element of X holds (f . x) - (g . x) = h . x

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

f . x = (h . x) + (g . x) by A1, A4, Th22;

hence (f . x) - (g . x) = h . x ; :: thesis: verum

end;f . x = (h . x) + (g . x) by A1, A4, Th22;

hence (f . x) - (g . x) = h . x ; :: thesis: verum