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 Z: 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 A1: ( f1 is_continuous_in x0 & 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

A4: x0 in dom (f1 + f2) by Z, VALUED_1:def 1;
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 A5: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . x0 = lim ((f1 + f2) /* s1) )
then A6: rng s1 c= (dom f1) /\ (dom f2) by VALUED_1:def 1;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
then dom (f1 + f2) c= dom f1 by XBOOLE_1:17;
then rng s1 c= dom f1 by A5, XBOOLE_1:1;
then A7: ( f1 /* s1 is convergent & f1 . x0 = lim (f1 /* s1) ) by A1, A5, Def1;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
then dom (f1 + f2) c= dom f2 by XBOOLE_1:17;
then rng s1 c= dom f2 by A5, XBOOLE_1:1;
then A8: ( f2 /* s1 is convergent & f2 . x0 = lim (f2 /* s1) ) by A1, A5, Def1;
then (f1 /* s1) + (f2 /* s1) is convergent by A7, SEQ_2:19;
hence (f1 + f2) /* s1 is convergent by A6, RFUNCT_2:23; :: thesis: (f1 + f2) . x0 = lim ((f1 + f2) /* s1)
thus (f1 + f2) . x0 = (f1 . x0) + (f2 . x0) by A4, VALUED_1:def 1
.= lim ((f1 /* s1) + (f2 /* s1)) by A7, A8, 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

A9: x0 in dom (f1 - f2) by Z, VALUED_1:12;
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 A10: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . x0 = lim ((f1 - f2) /* s1) )
then A11: rng s1 c= (dom f1) /\ (dom f2) by VALUED_1:12;
dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
then dom (f1 - f2) c= dom f1 by XBOOLE_1:17;
then rng s1 c= dom f1 by A10, XBOOLE_1:1;
then A12: ( f1 /* s1 is convergent & f1 . x0 = lim (f1 /* s1) ) by A1, A10, Def1;
dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
then dom (f1 - f2) c= dom f2 by XBOOLE_1:17;
then rng s1 c= dom f2 by A10, XBOOLE_1:1;
then A13: ( f2 /* s1 is convergent & f2 . x0 = lim (f2 /* s1) ) by A1, A10, Def1;
then (f1 /* s1) - (f2 /* s1) is convergent by A12, SEQ_2:25;
hence (f1 - f2) /* s1 is convergent by A11, RFUNCT_2:23; :: thesis: (f1 - f2) . x0 = lim ((f1 - f2) /* s1)
thus (f1 - f2) . x0 = (f1 . x0) - (f2 . x0) by A9, VALUED_1:13
.= lim ((f1 /* s1) - (f2 /* s1)) by A12, A13, SEQ_2:26
.= lim ((f1 - f2) /* s1) by A11, 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 A14: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . x0 = lim ((f1 (#) f2) /* s1) )
then A15: rng s1 c= (dom f1) /\ (dom f2) by 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 rng s1 c= dom f1 by A14, XBOOLE_1:1;
then A16: ( f1 /* s1 is convergent & f1 . x0 = lim (f1 /* s1) ) by A1, A14, Def1;
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4;
then dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17;
then rng s1 c= dom f2 by A14, XBOOLE_1:1;
then A17: ( f2 /* s1 is convergent & f2 . x0 = lim (f2 /* s1) ) by A1, A14, Def1;
then (f1 /* s1) (#) (f2 /* s1) is convergent by A16, SEQ_2:28;
hence (f1 (#) f2) /* s1 is convergent by A15, RFUNCT_2:23; :: thesis: (f1 (#) f2) . x0 = lim ((f1 (#) f2) /* s1)
thus (f1 (#) f2) . x0 = (f1 . x0) * (f2 . x0) by VALUED_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A16, A17, SEQ_2:29
.= lim ((f1 (#) f2) /* s1) by A15, RFUNCT_2:23 ; :: thesis: verum