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 A1: ( g = g1 & f = f1 ) ; :: thesis: g1 + f1 = g + f

A2: dom (g + f) = (dom g) /\ (dom f) by VFUNCT_1:def 1

.= (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 1;

hence g1 + f1 = g + f by A3, A2, VFUNCT_1:def 1; :: thesis: verum

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 A1: ( g = g1 & f = f1 ) ; :: thesis: g1 + f1 = g + f

A2: dom (g + f) = (dom g) /\ (dom f) by VFUNCT_1:def 1

.= (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 1;

hence g1 + f1 = g + f by A3, A2, VFUNCT_1:def 1; :: thesis: verum