let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for F, G, H being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for f, g, h being Function of S,T st f = F & g = G & h = H holds
( H = F - G iff for x being Element of S holds h . x = (f . x) - (g . x) )
let T be NormedLinearTopSpace; :: thesis: for F, G, H being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for f, g, h being Function of S,T st f = F & g = G & h = H holds
( H = F - G iff for x being Element of S holds h . x = (f . x) - (g . x) )
let F, G, H be Point of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: for f, g, h being Function of S,T st f = F & g = G & h = H holds
( H = F - G iff for x being Element of S holds h . x = (f . x) - (g . x) )
let f, g, h be Function of S,T; :: thesis: ( f = F & g = G & h = H implies ( H = F - G iff for x being Element of S 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 S holds h . x = (f . x) - (g . x) )
A2: now :: thesis: ( H = F - G implies for x being Element of S holds h . x = (f . x) - (g . x) )
assume H = F - G ; :: thesis: for x being Element of S holds h . x = (f . x) - (g . x)
then H + G = F - (G - G) by RLVECT_1:29;
then A3: H + G = F - (0. (R_NormSpace_of_ContinuousFunctions (S,T))) by RLVECT_1:15;
now :: thesis: for x being Element of S holds (f . x) - (g . x) = h . x
let x be Element of S; :: thesis: (f . x) - (g . x) = h . x
(f . x) - (g . x) = ((h . x) + (g . x)) - (g . x) by A1, A3, Th44;
hence (f . x) - (g . x) = h . x by RLVECT_4:1; :: thesis: verum
end;
hence for x being Element of S holds h . x = (f . x) - (g . x) ; :: thesis: verum
end;
now :: thesis: ( ( for x being Element of S holds h . x = (f . x) - (g . x) ) implies F - G = H )
assume A4: for x being Element of S holds h . x = (f . x) - (g . x) ; :: thesis: F - G = H
now :: thesis: for x being Element of S holds (h . x) + (g . x) = f . x
let x be Element of S; :: thesis: (h . x) + (g . x) = f . x
h . x = (f . x) - (g . x) by A4;
hence (h . x) + (g . x) = f . x by RLVECT_4:1; :: thesis: verum
end;
then F = H + G by A1, Th44;
then F - G = H + (G - G) by RLVECT_1:def 3;
then F - G = H + (0. (R_NormSpace_of_ContinuousFunctions (S,T))) by RLVECT_1:15;
hence F - G = H ; :: thesis: verum
end;
hence ( H = F - G iff for x being Element of S holds h . x = (f . x) - (g . x) ) by A2; :: thesis: verum