let x0 be Real; :: 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 :: thesis: for s1 being Real_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 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;
then A8: f2 /* s1 is convergent by A3, A5;
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;
then A10: f1 /* s1 is convergent by A2, A5;
then (f1 /* s1) + (f2 /* s1) is convergent by A8;
hence (f1 + f2) /* s1 is convergent by A6, RFUNCT_2:8; :: thesis: (f1 + f2) . x0 = lim ((f1 + f2) /* s1)
A11: f1 . x0 = lim (f1 /* s1) by A2, A5, A9;
A12: f2 . x0 = lim (f2 /* s1) by A3, A5, A7;
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:6
.= lim ((f1 + f2) /* s1) by A6, RFUNCT_2:8 ;
:: 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: for s1 being Real_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 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;
then A17: f2 /* s1 is convergent by A3, A14;
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;
then A19: f1 /* s1 is convergent by A2, A14;
then (f1 /* s1) - (f2 /* s1) is convergent by A17;
hence (f1 - f2) /* s1 is convergent by A15, RFUNCT_2:8; :: thesis: (f1 - f2) . x0 = lim ((f1 - f2) /* s1)
A20: f1 . x0 = lim (f1 /* s1) by A2, A14, A18;
A21: f2 . x0 = lim (f2 /* s1) by A3, A14, A16;
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:12
.= lim ((f1 - f2) /* s1) by A15, RFUNCT_2:8 ;
:: thesis: verum

end;

hence f1 - f2 is_continuous_in x0 ; :: 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;
then A25: f2 /* s1 is convergent by A3, A23;
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;
then A28: f1 /* s1 is convergent by A2, A23;
then (f1 /* s1) (#) (f2 /* s1) is convergent by A25;
hence (f1 (#) f2) /* s1 is convergent by A26, RFUNCT_2:8; :: thesis: (f1 (#) f2) . x0 = lim ((f1 (#) f2) /* s1)
A29: f1 . x0 = lim (f1 /* s1) by A2, A23, A27;
A30: f2 . x0 = lim (f2 /* s1) by A3, A23, A24;
thus (f1 (#) f2) . x0 = (f1 . x0) * (f2 . x0) by VALUED_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A28, A29, A25, A30, SEQ_2:15
.= lim ((f1 (#) f2) /* s1) by A26, RFUNCT_2:8 ; :: thesis: verum