let X, Y be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( g = g1 & f = f1 implies g1 - f1 = g - f )
assume AS: ( g = g1 & f = f1 ) ; :: thesis: g1 - f1 = g - f
P0: dom (g - f) = (dom g) /\ (dom f) by VFUNCT_1:def 2
.= (dom g1) /\ (dom f1) by AS ;
P1: g - f is PartFunc of Y,the carrier of V by RELSET_1:13, P0;
for c being Element of Y st c in dom (g - f) holds
(g - f) /. c = (g1 /. c) - (f1 /. c) by VFUNCT_1:def 2, AS;
hence g1 - f1 = g - f by P1, P0, VFUNCT_1:def 2; :: thesis: verum