let X be RealNormSpace; :: thesis: for f, g, h being Point of (DualSp X) holds

( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )

let f, g, h be Point of (DualSp X); :: thesis: ( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )

reconsider f9 = f, g9 = g, h9 = h as Lipschitzian linear-Functional of X by Def9;

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

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

hence h = f - g ; :: thesis: verum

( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )

let f, g, h be Point of (DualSp X); :: thesis: ( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )

reconsider f9 = f, g9 = g, h9 = h as Lipschitzian linear-Functional of X by Def9;

hereby :: thesis: ( ( for x being VECTOR of X holds h . x = (f . x) - (g . x) ) implies h = f - g )

assume A2:
for x being VECTOR of X holds h . x = (f . x) - (g . x)
; :: thesis: h = f - gassume
h = f - g
; :: thesis: for x being VECTOR of X holds h . x = (f . x) - (g . x)

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

then A11: h + g = f - (0. (DualSp X)) by RLVECT_1:15;

end;then h + g = f - (g - g) by RLVECT_1:29;

then A11: h + g = f - (0. (DualSp X)) by RLVECT_1:15;

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

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

f9 . x = (h9 . x) + (g9 . x) by A11, Th35;

hence (f9 . x) - (g9 . x) = h9 . x ; :: thesis: verum

end;f9 . x = (h9 . x) + (g9 . x) by A11, Th35;

hence (f9 . x) - (g9 . x) = h9 . x ; :: thesis: verum

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

then
f = h + g
by Th35;let x be VECTOR of X; :: thesis: (h9 . x) + (g9 . x) = f9 . x

h9 . x = (f9 . x) - (g9 . x) by A2;

hence (h9 . x) + (g9 . x) = f9 . x ; :: thesis: verum

end;h9 . x = (f9 . x) - (g9 . x) by A2;

hence (h9 . x) + (g9 . x) = f9 . x ; :: thesis: verum

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

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

hence h = f - g ; :: thesis: verum