let CNS be ComplexNormSpace; for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of RNS,CNS st f1 is_continuous_on X & f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 )
let RNS be RealNormSpace; for X, X1 being set
for f1, f2 being PartFunc of RNS,CNS st f1 is_continuous_on X & f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 )
let X, X1 be set ; for f1, f2 being PartFunc of RNS,CNS st f1 is_continuous_on X & f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 )
let f1, f2 be PartFunc of RNS,CNS; ( f1 is_continuous_on X & f2 is_continuous_on X1 implies ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) )
assume
( f1 is_continuous_on X & f2 is_continuous_on X1 )
; ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 )
then
( f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 )
by Th58, XBOOLE_1:17;
hence
( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 )
by Th64; verum