let X, Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds
( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
let C be non empty set ; :: thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds
( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
let V be RealNormSpace; :: thesis: for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds
( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
let f1, f2 be PartFunc of C,V; :: thesis: ( f1 | X is V8() & f2 | Y is V8() implies ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() ) )
assume that
A1: f1 | X is V8() and
A2: f2 | Y is V8() ; :: thesis: ( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )
consider r1 being VECTOR of V such that
A3: for c being Element of C st c in X /\ (dom f1) holds
f1 /. c = r1 by A1, PARTFUN2:35;
consider r2 being VECTOR of V such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
f2 /. c = r2 by A2, PARTFUN2:35;
now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds
(f1 + f2) /. c = r1 + r2
let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) /. c = r1 + r2 )
assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; :: thesis: (f1 + f2) /. c = r1 + r2
then A6: c in X /\ Y by XBOOLE_0:def 4;
then A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1 + f2) by A5, XBOOLE_0:def 4;
then A9: c in (dom f1) /\ (dom f2) by Def1;
then c in dom f1 by XBOOLE_0:def 4;
then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def 4;
A11: c in Y by A6, XBOOLE_0:def 4;
c in dom f2 by A9, XBOOLE_0:def 4;
then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def 4;
thus (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by A8, Def1
.= r1 + (f2 /. c) by A3, A10
.= r1 + r2 by A4, A12 ; :: thesis: verum
end;
hence (f1 + f2) | (X /\ Y) is V8() by PARTFUN2:35; :: thesis: (f1 - f2) | (X /\ Y) is V8()
now :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 - f2)) holds
(f1 - f2) /. c = r1 - r2
let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) /. c = r1 - r2 )
assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; :: thesis: (f1 - f2) /. c = r1 - r2
then A14: c in X /\ Y by XBOOLE_0:def 4;
then A15: c in X by XBOOLE_0:def 4;
A16: c in dom (f1 - f2) by A13, XBOOLE_0:def 4;
then A17: c in (dom f1) /\ (dom f2) by Def2;
then c in dom f1 by XBOOLE_0:def 4;
then A18: c in X /\ (dom f1) by A15, XBOOLE_0:def 4;
A19: c in Y by A14, XBOOLE_0:def 4;
c in dom f2 by A17, XBOOLE_0:def 4;
then A20: c in Y /\ (dom f2) by A19, XBOOLE_0:def 4;
thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A16, Def2
.= r1 - (f2 /. c) by A3, A18
.= r1 - r2 by A4, A20 ; :: thesis: verum
end;
hence (f1 - f2) | (X /\ Y) is V8() by PARTFUN2:35; :: thesis: verum