let x0 be Complex; :: thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
let f1, f2 be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f1 is_continuous_in x0 & f2 is_continuous_in x0 implies ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) )
assume that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0 ; :: thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
A3: ( x0 in dom f1 & x0 in dom f2 ) by A1, A2;

now :: thesis: ( x0 in dom (f1 + f2) & ( for s1 being Complex_Sequence st rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 holds
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) ) )

x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def 4;
hence A4: x0 in dom (f1 + f2) by VALUED_1:def 1; :: thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 holds
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )
let s1 be Complex_Sequence; :: thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) )
assume that
A5: rng s1 c= dom (f1 + f2) and
A6: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )
A7: rng s1 c= (dom f1) /\ (dom f2) by A5, VALUED_1:def 1;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
then dom (f1 + f2) c= dom f2 by XBOOLE_1:17;
then A8: rng s1 c= dom f2 by A5;
then A9: f2 /* s1 is convergent by A2, A6;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
then dom (f1 + f2) c= dom f1 by XBOOLE_1:17;
then A10: rng s1 c= dom f1 by A5;
then A11: f1 /* s1 is convergent by A1, A6;
then (f1 /* s1) + (f2 /* s1) is convergent by A9;
hence (f1 + f2) /* s1 is convergent by A7, Th7; :: thesis: (f1 + f2) /. x0 = lim ((f1 + f2) /* s1)
A12: f1 /. x0 = lim (f1 /* s1) by A1, A6, A10;
A13: f2 /. x0 = lim (f2 /* s1) by A2, A6, A8;
thus (f1 + f2) /. x0 = (f1 /. x0) + (f2 /. x0) by A4, CFUNCT_1:1
.= lim ((f1 /* s1) + (f2 /* s1)) by A11, A12, A9, A13, COMSEQ_2:14
.= lim ((f1 + f2) /* s1) by A7, Th7 ; :: thesis: verum

end;

hence f1 + f2 is_continuous_in x0 ; :: thesis: ( f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )

now :: thesis: ( x0 in dom (f1 - f2) & ( for s1 being Complex_Sequence st rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) ) )

x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def 4;
hence A14: x0 in dom (f1 - f2) by CFUNCT_1:2; :: thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )
let s1 be Complex_Sequence; :: thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) )
assume that
A15: rng s1 c= dom (f1 - f2) and
A16: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )
A17: rng s1 c= (dom f1) /\ (dom f2) by A15, CFUNCT_1:2;
dom (f1 - f2) = (dom f1) /\ (dom f2) by CFUNCT_1:2;
then dom (f1 - f2) c= dom f2 by XBOOLE_1:17;
then A18: rng s1 c= dom f2 by A15;
then A19: f2 /* s1 is convergent by A2, A16;
dom (f1 - f2) = (dom f1) /\ (dom f2) by CFUNCT_1:2;
then dom (f1 - f2) c= dom f1 by XBOOLE_1:17;
then A20: rng s1 c= dom f1 by A15;
then A21: f1 /* s1 is convergent by A1, A16;
then (f1 /* s1) - (f2 /* s1) is convergent by A19;
hence (f1 - f2) /* s1 is convergent by A17, Th7; :: thesis: (f1 - f2) /. x0 = lim ((f1 - f2) /* s1)
A22: f1 /. x0 = lim (f1 /* s1) by A1, A16, A20;
A23: f2 /. x0 = lim (f2 /* s1) by A2, A16, A18;
thus (f1 - f2) /. x0 = (f1 /. x0) - (f2 /. x0) by A14, CFUNCT_1:2
.= lim ((f1 /* s1) - (f2 /* s1)) by A21, A22, A19, A23, COMSEQ_2:26
.= lim ((f1 - f2) /* s1) by A17, Th7 ; :: thesis: verum

end;

hence f1 - f2 is_continuous_in x0 ; :: thesis: f1 (#) f2 is_continuous_in x0
x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def 4;
hence A24: x0 in dom (f1 (#) f2) by VALUED_1:def 4; :: according to CFCONT_1:def 1 :: thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 holds
( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) )
let s1 be Complex_Sequence; :: thesis: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) ) )
assume that
A25: rng s1 c= dom (f1 (#) f2) and
A26: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) )
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4;
then dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17;
then A27: rng s1 c= dom f2 by A25;
then A28: f2 /* s1 is convergent by A2, A26;
A29: rng s1 c= (dom f1) /\ (dom f2) by A25, VALUED_1:def 4;
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4;
then dom (f1 (#) f2) c= dom f1 by XBOOLE_1:17;
then A30: rng s1 c= dom f1 by A25;
then A31: f1 /* s1 is convergent by A1, A26;
then (f1 /* s1) (#) (f2 /* s1) is convergent by A28;
hence (f1 (#) f2) /* s1 is convergent by A29, Th7; :: thesis: (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1)
A32: f1 /. x0 = lim (f1 /* s1) by A1, A26, A30;
A33: f2 /. x0 = lim (f2 /* s1) by A2, A26, A27;
thus (f1 (#) f2) /. x0 = (f1 /. x0) * (f2 /. x0) by A24, CFUNCT_1:3
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A31, A32, A28, A33, COMSEQ_2:30
.= lim ((f1 (#) f2) /* s1) by A29, Th7 ; :: thesis: verum