let X be set ; :: thesis: for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds

( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous ) )

assume A1: X c= (dom f1) /\ (dom f2) ; :: thesis: ( not f1 | X is continuous or not f2 | X is continuous or ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous ) )

assume A2: ( f1 | X is continuous & f2 | X is continuous ) ; :: thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )

A3: ( X c= dom f1 & X c= dom f2 ) by A1, XBOOLE_1:18;

A17: X c= dom (f1 - f2) by A1, VALUED_1:12;

X c= dom (f1 (#) f2) by A1, VALUED_1:def 4;

hence (f1 (#) f2) | X is continuous by A4, Th13; :: thesis: verum

( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous ) )

assume A1: X c= (dom f1) /\ (dom f2) ; :: thesis: ( not f1 | X is continuous or not f2 | X is continuous or ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous ) )

assume A2: ( f1 | X is continuous & f2 | X is continuous ) ; :: thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )

A3: ( X c= dom f1 & X c= dom f2 ) by A1, XBOOLE_1:18;

A4: now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) )

A10:
X c= dom (f1 + f2)
by A1, VALUED_1:def 1;( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) )

let s1 be Real_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 that

A5: rng s1 c= X and

A6: ( s1 is convergent & lim s1 in X ) ; :: thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) )

A7: rng s1 c= (dom f1) /\ (dom f2) by A1, A5;

A8: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A5, A6, Th13;

then A9: (f1 /* s1) (#) (f2 /* s1) is convergent ;

( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A5, A6, Th13;

then (f1 (#) f2) . (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by VALUED_1:5

.= lim ((f1 /* s1) (#) (f2 /* s1)) by A8, SEQ_2:15

.= lim ((f1 (#) f2) /* s1) by A7, RFUNCT_2:8 ;

hence ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) by A7, A9, RFUNCT_2:8; :: thesis: verum

end;assume that

A5: rng s1 c= X and

A6: ( s1 is convergent & lim s1 in X ) ; :: thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) )

A7: rng s1 c= (dom f1) /\ (dom f2) by A1, A5;

A8: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A5, A6, Th13;

then A9: (f1 /* s1) (#) (f2 /* s1) is convergent ;

( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A5, A6, Th13;

then (f1 (#) f2) . (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by VALUED_1:5

.= lim ((f1 /* s1) (#) (f2 /* s1)) by A8, SEQ_2:15

.= lim ((f1 (#) f2) /* s1) by A7, RFUNCT_2:8 ;

hence ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) by A7, A9, RFUNCT_2:8; :: thesis: verum

now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) )

hence
(f1 + f2) | X is continuous
by A10, Th13; :: thesis: ( (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) )

let s1 be Real_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 that

A11: rng s1 c= X and

A12: s1 is convergent and

A13: lim s1 in X ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) )

A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A11, A12, A13, Th13;

then A15: (f1 /* s1) + (f2 /* s1) is convergent ;

A16: rng s1 c= (dom f1) /\ (dom f2) by A1, A11;

( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A11, A12, A13, Th13;

then (f1 + f2) . (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A10, A13, VALUED_1:def 1

.= lim ((f1 /* s1) + (f2 /* s1)) by A14, SEQ_2:6

.= lim ((f1 + f2) /* s1) by A16, RFUNCT_2:8 ;

hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) by A16, A15, RFUNCT_2:8; :: thesis: verum

end;assume that

A11: rng s1 c= X and

A12: s1 is convergent and

A13: lim s1 in X ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) )

A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A11, A12, A13, Th13;

then A15: (f1 /* s1) + (f2 /* s1) is convergent ;

A16: rng s1 c= (dom f1) /\ (dom f2) by A1, A11;

( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A11, A12, A13, Th13;

then (f1 + f2) . (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A10, A13, VALUED_1:def 1

.= lim ((f1 /* s1) + (f2 /* s1)) by A14, SEQ_2:6

.= lim ((f1 + f2) /* s1) by A16, RFUNCT_2:8 ;

hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) by A16, A15, RFUNCT_2:8; :: thesis: verum

A17: X c= dom (f1 - f2) by A1, VALUED_1:12;

now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )

hence
(f1 - f2) | X is continuous
by A17, Th13; :: thesis: (f1 (#) f2) | X is continuous ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )

let s1 be Real_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 that

A18: rng s1 c= X and

A19: s1 is convergent and

A20: lim s1 in X ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )

A21: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A18, A19, A20, Th13;

then A22: (f1 /* s1) - (f2 /* s1) is convergent ;

A23: rng s1 c= (dom f1) /\ (dom f2) by A1, A18;

( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A18, A19, A20, Th13;

then (f1 - f2) . (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A17, A20, VALUED_1:13

.= lim ((f1 /* s1) - (f2 /* s1)) by A21, SEQ_2:12

.= lim ((f1 - f2) /* s1) by A23, RFUNCT_2:8 ;

hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) by A23, A22, RFUNCT_2:8; :: thesis: verum

end;assume that

A18: rng s1 c= X and

A19: s1 is convergent and

A20: lim s1 in X ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )

A21: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A18, A19, A20, Th13;

then A22: (f1 /* s1) - (f2 /* s1) is convergent ;

A23: rng s1 c= (dom f1) /\ (dom f2) by A1, A18;

( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A18, A19, A20, Th13;

then (f1 - f2) . (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A17, A20, VALUED_1:13

.= lim ((f1 /* s1) - (f2 /* s1)) by A21, SEQ_2:12

.= lim ((f1 - f2) /* s1) by A23, RFUNCT_2:8 ;

hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) by A23, A22, RFUNCT_2:8; :: thesis: verum

X c= dom (f1 (#) f2) by A1, VALUED_1:def 4;

hence (f1 (#) f2) | X is continuous by A4, Th13; :: thesis: verum