let X, X1 be set ; :: thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX 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 & f1 (#) f2 is_continuous_on X /\ X1 )
let f1, f2 be PartFunc of COMPLEX,COMPLEX; :: thesis: ( 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 & f1 (#) f2 is_continuous_on X /\ X1 ) )
assume ( f1 is_continuous_on X & f2 is_continuous_on X1 ) ; :: thesis: ( f1 + f2 is_continuous_on X /\ 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 Th41, XBOOLE_1:17;
hence ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) by Th43; :: thesis: verum