let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f9, g9, h9 being continuous PartFunc of REAL,Y st f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X holds
( h = f - g iff for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) )
let Y be RealNormSpace; :: thesis: for f, g, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f9, g9, h9 being continuous PartFunc of REAL,Y st f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X holds
( h = f - g iff for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) )
let f, g, h be Point of (R_NormSpace_of_ContinuousFunctions (X,Y)); :: thesis: for f9, g9, h9 being continuous PartFunc of REAL,Y st f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X holds
( h = f - g iff for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) )
let f9, g9, h9 be continuous PartFunc of REAL,Y; :: thesis: ( f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X implies ( h = f - g iff for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) ) )
assume A1: ( f9 = f & g9 = g & h9 = h & dom f9 = X & dom g9 = X & dom h9 = X ) ; :: thesis: ( h = f - g iff for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) )

A2: now :: thesis: ( ( for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) ) implies f - g = h )

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

now :: thesis: for x being Element of X holds (h9 /. x) + (g9 /. x) = f9 /. x

let x be Element of X; :: thesis: (h9 /. x) + (g9 /. x) = f9 /. x
h9 /. x = (f9 /. x) - (g9 /. x) by A3;
then (h9 /. x) + (g9 /. x) = (f9 /. x) - ((g9 /. x) - (g9 /. x)) by RLVECT_1:29;
then (h9 /. x) + (g9 /. x) = (f9 /. x) - (0. Y) by RLVECT_1:15;
hence (h9 /. x) + (g9 /. x) = f9 /. x ; :: thesis: verum

end;

then f = h + g by A1, Th15;
then f - g = h + (g - g) by RLVECT_1:def 3;
then f - g = h + (0. (R_NormSpace_of_ContinuousFunctions (X,Y))) by RLVECT_1:5;
hence f - g = h ; :: thesis: verum

end;

now :: thesis: ( h = f - g implies for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) )

assume h = f - g ; :: thesis: for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x)
then h + g = f - (g - g) by RLVECT_1:29;
then A4: h + g = f - (0. (R_NormSpace_of_ContinuousFunctions (X,Y))) by RLVECT_1:5;

now :: thesis: for x being Element of X holds (f9 /. x) - (g9 /. x) = h9 /. x

let x be Element of X; :: thesis: (f9 /. x) - (g9 /. x) = h9 /. x
f9 /. x = (h9 /. x) + (g9 /. x) by A1, A4, Th15;
then (f9 /. x) - (g9 /. x) = (h9 /. x) + ((g9 /. x) - (g9 /. x)) by RLVECT_1:def 3;
then (f9 /. x) - (g9 /. x) = (h9 /. x) + (0. Y) by RLVECT_1:15;
hence (f9 /. x) - (g9 /. x) = h9 /. x ; :: thesis: verum

end;

hence for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) ; :: thesis: verum

end;

hence ( h = f - g iff for x being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) ) by A2; :: thesis: verum