let x0 be real number ; :: thesis: for f1, f2 being PartFunc of REAL,REAL st x0 in (dom f1) /\ (dom f2) & 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 REAL,REAL; :: thesis: ( x0 in (dom f1) /\ (dom f2) & 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 A1: x0 in (dom f1) /\ (dom f2) ; :: thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in x0 or ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in x0 ; :: thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )

now

let s1 be Real_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
A4: rng s1 c= dom (f1 + f2) and
A5: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . x0 = lim ((f1 + f2) /* s1) )
A6: rng s1 c= (dom f1) /\ (dom f2) by A4, 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 A7: rng s1 c= dom f2 by A4, XBOOLE_1:1;
then A8: f2 /* s1 is convergent by A3, A5, Def1;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
then dom (f1 + f2) c= dom f1 by XBOOLE_1:17;
then A9: rng s1 c= dom f1 by A4, XBOOLE_1:1;
then A10: f1 /* s1 is convergent by A2, A5, Def1;
then (f1 /* s1) + (f2 /* s1) is convergent by A8, SEQ_2:19;
hence (f1 + f2) /* s1 is convergent by A6, RFUNCT_2:23; :: thesis: (f1 + f2) . x0 = lim ((f1 + f2) /* s1)
A11: f1 . x0 = lim (f1 /* s1) by A2, A5, A9, Def1;
A12: f2 . x0 = lim (f2 /* s1) by A3, A5, A7, Def1;
x0 in dom (f1 + f2) by A1, VALUED_1:def 1;
hence (f1 + f2) . x0 = (f1 . x0) + (f2 . x0) by VALUED_1:def 1
.= lim ((f1 /* s1) + (f2 /* s1)) by A10, A11, A8, A12, SEQ_2:20
.= lim ((f1 + f2) /* s1) by A6, RFUNCT_2:23 ;
:: thesis: verum

end;

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

now

let s1 be Real_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
A13: rng s1 c= dom (f1 - f2) and
A14: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . x0 = lim ((f1 - f2) /* s1) )
A15: rng s1 c= (dom f1) /\ (dom f2) by A13, VALUED_1:12;
dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
then dom (f1 - f2) c= dom f2 by XBOOLE_1:17;
then A16: rng s1 c= dom f2 by A13, XBOOLE_1:1;
then A17: f2 /* s1 is convergent by A3, A14, Def1;
dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
then dom (f1 - f2) c= dom f1 by XBOOLE_1:17;
then A18: rng s1 c= dom f1 by A13, XBOOLE_1:1;
then A19: f1 /* s1 is convergent by A2, A14, Def1;
then (f1 /* s1) - (f2 /* s1) is convergent by A17, SEQ_2:25;
hence (f1 - f2) /* s1 is convergent by A15, RFUNCT_2:23; :: thesis: (f1 - f2) . x0 = lim ((f1 - f2) /* s1)
A20: f1 . x0 = lim (f1 /* s1) by A2, A14, A18, Def1;
A21: f2 . x0 = lim (f2 /* s1) by A3, A14, A16, Def1;
x0 in dom (f1 - f2) by A1, VALUED_1:12;
hence (f1 - f2) . x0 = (f1 . x0) - (f2 . x0) by VALUED_1:13
.= lim ((f1 /* s1) - (f2 /* s1)) by A19, A20, A17, A21, SEQ_2:26
.= lim ((f1 - f2) /* s1) by A15, RFUNCT_2:23 ;
:: thesis: verum

end;

hence f1 - f2 is_continuous_in x0 by Def1; :: thesis: f1 (#) f2 is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: 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
A22: rng s1 c= dom (f1 (#) f2) and
A23: ( 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 A24: rng s1 c= dom f2 by A22, XBOOLE_1:1;
then A25: f2 /* s1 is convergent by A3, A23, Def1;
A26: rng s1 c= (dom f1) /\ (dom f2) by A22, 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 A27: rng s1 c= dom f1 by A22, XBOOLE_1:1;
then A28: f1 /* s1 is convergent by A2, A23, Def1;
then (f1 /* s1) (#) (f2 /* s1) is convergent by A25, SEQ_2:28;
hence (f1 (#) f2) /* s1 is convergent by A26, RFUNCT_2:23; :: thesis: (f1 (#) f2) . x0 = lim ((f1 (#) f2) /* s1)
A29: f1 . x0 = lim (f1 /* s1) by A2, A23, A27, Def1;
A30: f2 . x0 = lim (f2 /* s1) by A3, A23, A24, Def1;
thus (f1 (#) f2) . x0 = (f1 . x0) * (f2 . x0) by VALUED_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A28, A29, A25, A30, SEQ_2:29
.= lim ((f1 (#) f2) /* s1) by A26, RFUNCT_2:23 ; :: thesis: verum