let X be non empty set ; :: thesis: for Y being ComplexNormSpace

for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))

for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds

( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )

let Y be ComplexNormSpace; :: thesis: for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))

for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h 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 (C_NormSpace_of_BoundedFunctions (X,Y)); :: thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds

( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )

let f9, g9, h9 be bounded Function of X, the carrier of Y; :: thesis: ( f9 = f & g9 = g & h9 = h 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 ) ; :: thesis: ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )

for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))

for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds

( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )

let Y be ComplexNormSpace; :: thesis: for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))

for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h 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 (C_NormSpace_of_BoundedFunctions (X,Y)); :: thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds

( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )

let f9, g9, h9 be bounded Function of X, the carrier of Y; :: thesis: ( f9 = f & g9 = g & h9 = h 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 ) ; :: 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

then f - g = h + (g - g) by RLVECT_1:def 3;

then f - g = h + (0. (C_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15;

hence f - g = h by RLVECT_1:4; :: thesis: verum

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

then
f = h + g
by A1, Th20;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 by RLVECT_1:13; :: thesis: verum

end;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 by RLVECT_1:13; :: thesis: verum

then f - g = h + (g - g) by RLVECT_1:def 3;

then f - g = h + (0. (C_NormSpace_of_BoundedFunctions (X,Y))) 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 h9 . x = (f9 . x) - (g9 . x) )

hence
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
by A2; :: thesis: verumassume
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 h + g = f - (0. (C_NormSpace_of_BoundedFunctions (X,Y))) 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_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15;

then A4: h + g = f by RLVECT_1:13;

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

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

f9 . x = (h9 . x) + (g9 . x) by A1, A4, Th20;

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 by RLVECT_1:4; :: thesis: verum

end;f9 . x = (h9 . x) + (g9 . x) by A1, A4, Th20;

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 by RLVECT_1:4; :: thesis: verum