let X be set ; :: thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )
let f1, f2 be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f1 is_continuous_on X & f2 is_continuous_on X implies ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X ) )
assume A1: ( f1 is_continuous_on X & f2 is_continuous_on X ) ; :: thesis: ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )
then ( X c= dom f1 & X c= dom f2 ) ;
then A2: X c= (dom f1) /\ (dom f2) by XBOOLE_1:19;
then A3: X c= dom (f1 + f2) by CFUNCT_1:1;
now :: thesis: for s1 being Complex_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) )
let s1 be Complex_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
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )
A7: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A4, A5, A6, Th38;
then A8: (f1 /* s1) + (f2 /* s1) is convergent ;
A9: rng s1 c= (dom f1) /\ (dom f2) by A2, A4;
A10: lim s1 in dom (f1 + f2) by A3, A6;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A4, A5, A6, Th38;
then (f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A10, CFUNCT_1:1
.= lim ((f1 /* s1) + (f2 /* s1)) by A7, COMSEQ_2:14
.= lim ((f1 + f2) /* s1) by A9, Th7 ;
hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A8, Th7; :: thesis: verum
end;
hence f1 + f2 is_continuous_on X by A3, Th38; :: thesis: ( f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )
A11: X c= dom (f1 - f2) by A2, CFUNCT_1:2;
now :: thesis: for s1 being Complex_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) )
let s1 be Complex_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
A12: rng s1 c= X and
A13: s1 is convergent and
A14: lim s1 in X ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
A15: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A12, A13, A14, Th38;
then A16: (f1 /* s1) - (f2 /* s1) is convergent ;
A17: rng s1 c= (dom f1) /\ (dom f2) by A2, A12;
A18: lim s1 in dom (f1 - f2) by A11, A14;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A12, A13, A14, Th38;
then (f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A18, CFUNCT_1:2
.= lim ((f1 /* s1) - (f2 /* s1)) by A15, COMSEQ_2:26
.= lim ((f1 - f2) /* s1) by A17, Th7 ;
hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A17, A16, Th7; :: thesis: verum
end;
hence f1 - f2 is_continuous_on X by A11, Th38; :: thesis: f1 (#) f2 is_continuous_on X
A19: X c= dom (f1 (#) f2) by A2, CFUNCT_1:3;
now :: thesis: for s1 being Complex_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) )
let s1 be Complex_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
A20: rng s1 c= X and
A21: s1 is convergent and
A22: lim s1 in X ; :: thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) )
A23: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A20, A21, A22, Th38;
then A24: (f1 /* s1) (#) (f2 /* s1) is convergent ;
A25: rng s1 c= (dom f1) /\ (dom f2) by A2, A20;
A26: lim s1 in dom (f1 (#) f2) by A19, A22;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A20, A21, A22, Th38;
then (f1 (#) f2) /. (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by A26, CFUNCT_1:3
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A23, COMSEQ_2:30
.= lim ((f1 (#) f2) /* s1) by A25, Th7 ;
hence ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) ) by A25, A24, Th7; :: thesis: verum
end;
hence f1 (#) f2 is_continuous_on X by A19, Th38; :: thesis: verum