let X, Y be non empty set ; for V being RealNormSpace
for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
let V be RealNormSpace; for g, f being PartFunc of X, the carrier of V
for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
let g, f be PartFunc of X, the carrier of V; for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds
g1 - f1 = g - f
let g1, f1 be PartFunc of Y, the carrier of V; ( g = g1 & f = f1 implies g1 - f1 = g - f )
assume A1:
( g = g1 & f = f1 )
; g1 - f1 = g - f
A2: dom (g - f) =
(dom g) /\ (dom f)
by VFUNCT_1:def 2
.=
(dom g1) /\ (dom f1)
by A1
;
A3:
g - f is PartFunc of Y, the carrier of V
by A2, RELSET_1:5;
for c being Element of Y st c in dom (g - f) holds
(g - f) /. c = (g1 /. c) - (f1 /. c)
by A1, VFUNCT_1:def 2;
hence
g1 - f1 = g - f
by A3, A2, VFUNCT_1:def 2; verum