let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X being set
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_continuous_on X & f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X )
let X be set ; :: thesis: for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_continuous_on X & f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X )
let f1, f2 be PartFunc of CNS1,CNS2; :: thesis: ( f1 is_continuous_on X & f2 is_continuous_on X implies ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X ) )
assume that
A1: f1 is_continuous_on X and
A2: f2 is_continuous_on X ; :: thesis: ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X )
A3: X c= dom f1 by A1, Th62;
X c= dom f2 by A2, Th62;
then A4: X c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A5: X c= dom (f1 + f2) by VFUNCT_2:def 1;
A6: X c= dom (f1 - f2) by A4, VFUNCT_2:def 2;

now

let s1 be sequence of CNS1; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) )
assume A7: ( rng s1 c= X & s1 is convergent & lim s1 in X ) ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )
then A8: rng s1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:1;
A9: ( f1 /* s1 is convergent & f1 /. (lim s1) = lim (f1 /* s1) ) by A1, A7, Th62;
A10: ( f2 /* s1 is convergent & f2 /. (lim s1) = lim (f2 /* s1) ) by A2, A7, Th62;
then A11: (f1 /* s1) + (f2 /* s1) is convergent by A9, CLVECT_1:115;
(f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A5, A7, A9, A10, VFUNCT_2:def 1
.= lim ((f1 /* s1) + (f2 /* s1)) by A9, A10, CLVECT_1:121
.= lim ((f1 + f2) /* s1) by A8, Th44 ;
hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A8, A11, Th44; :: thesis: verum

end;

hence f1 + f2 is_continuous_on X by A5, Th62; :: thesis: f1 - f2 is_continuous_on X

now

let s1 be sequence of CNS1; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) )
assume A12: ( rng s1 c= X & s1 is convergent & lim s1 in X ) ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
then A13: rng s1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:1;
A14: ( f1 /* s1 is convergent & f1 /. (lim s1) = lim (f1 /* s1) ) by A1, A12, Th62;
A15: ( f2 /* s1 is convergent & f2 /. (lim s1) = lim (f2 /* s1) ) by A2, A12, Th62;
then A16: (f1 /* s1) - (f2 /* s1) is convergent by A14, CLVECT_1:116;
(f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A6, A12, A14, A15, VFUNCT_2:def 2
.= lim ((f1 /* s1) - (f2 /* s1)) by A14, A15, CLVECT_1:122
.= lim ((f1 - f2) /* s1) by A13, Th44 ;
hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A13, A16, Th44; :: thesis: verum

end;

hence f1 - f2 is_continuous_on X by A6, Th62; :: thesis: verum