let X be set ; :: thesis: for f1, f2 being PartFunc of COMPLEX ,COMPLEX st f1 is_continuous_on X & f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )
let f1, f2 be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( f1 is_continuous_on X & f2 is_continuous_on X implies ( f1 + f2 is_continuous_on X & 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 & f1 (#) f2 is_continuous_on X )
A3: X c= dom f1 by A1, Th60;
X c= dom f2 by A2, Th60;
then A4: X c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A5: X c= dom (f1 + f2) by CFUNCT_1:3;
A6: X c= dom (f1 - f2) by A4, CFUNCT_1:4;
A7: X c= dom (f1 (#) f2) by A4, CFUNCT_1:5;

now

let s1 be Complex_Sequence; :: 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 A8: ( 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 A9: rng s1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:1;
A10: ( f1 /* s1 is convergent & f1 /. (lim s1) = lim (f1 /* s1) ) by A1, A8, Th60;
A11: ( f2 /* s1 is convergent & f2 /. (lim s1) = lim (f2 /* s1) ) by A2, A8, Th60;
then A12: (f1 /* s1) + (f2 /* s1) is convergent by A10, COMSEQ_2:13;
(f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A5, A8, A10, A11, CFUNCT_1:3
.= lim ((f1 /* s1) + (f2 /* s1)) by A10, A11, COMSEQ_2:14
.= lim ((f1 + f2) /* s1) by A9, Th18 ;
hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A12, Th18; :: thesis: verum

end;

hence f1 + f2 is_continuous_on X by A5, Th60; :: thesis: ( f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )

now

let s1 be Complex_Sequence; :: 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 A13: ( 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 A14: rng s1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:1;
A15: ( f1 /* s1 is convergent & f1 /. (lim s1) = lim (f1 /* s1) ) by A1, A13, Th60;
A16: ( f2 /* s1 is convergent & f2 /. (lim s1) = lim (f2 /* s1) ) by A2, A13, Th60;
then A17: (f1 /* s1) - (f2 /* s1) is convergent by A15, COMSEQ_2:25;
(f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A6, A13, A15, A16, CFUNCT_1:4
.= lim ((f1 /* s1) - (f2 /* s1)) by A15, A16, COMSEQ_2:26
.= lim ((f1 - f2) /* s1) by A14, Th18 ;
hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A14, A17, Th18; :: thesis: verum

end;

hence f1 - f2 is_continuous_on X by A6, Th60; :: thesis: f1 (#) f2 is_continuous_on X

now

let s1 be Complex_Sequence; :: 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 A18: ( 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 A19: rng s1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:1;
A20: ( f1 /* s1 is convergent & f1 /. (lim s1) = lim (f1 /* s1) ) by A1, A18, Th60;
A21: ( f2 /* s1 is convergent & f2 /. (lim s1) = lim (f2 /* s1) ) by A2, A18, Th60;
then A22: (f1 /* s1) (#) (f2 /* s1) is convergent by A20, COMSEQ_2:29;
(f1 (#) f2) /. (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by A7, A18, A20, A21, CFUNCT_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A20, A21, COMSEQ_2:30
.= lim ((f1 (#) f2) /* s1) by A19, Th18 ;
hence ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) ) by A19, A22, Th18; :: thesis: verum

end;

hence f1 (#) f2 is_continuous_on X by A7, Th60; :: thesis: verum