for th being real number st th in dom (cosec | [.(- (PI / 2)),0 .[) holds
cosec | [.(- (PI / 2)),0 .[ is_continuous_in th

proof

let th be real number ; :: thesis: ( th in dom (cosec | [.(- (PI / 2)),0 .[) implies cosec | [.(- (PI / 2)),0 .[ is_continuous_in th )
assume th in dom (cosec | [.(- (PI / 2)),0 .[) ; :: thesis: cosec | [.(- (PI / 2)),0 .[ is_continuous_in th
then A0: th in [.(- (PI / 2)),0 .[ by RELAT_1:86;
( - PI < th & th < 0 ) by A0, Lm3, XXREAL_1:4;
then ( (- PI ) + (2 * PI ) < th + (2 * PI ) & th + (2 * PI ) < 0 + (2 * PI ) ) by XREAL_1:10;
then th + (2 * PI ) in ].PI ,(2 * PI ).[ ;
then sin . (th + (2 * PI )) <> 0 by COMPTRIG:25;
then A1: sin . th <> 0 by SIN_COS:83;
AA: sin is_differentiable_in th by SIN_COS:69;
A2: cosec is_continuous_in th by A1, AA, FCONT_1:10, FDIFF_1:32;
( th in dom (cosec | [.(- (PI / 2)),0 .[) & ( for rseq being Real_Sequence st rng rseq c= dom (cosec | [.(- (PI / 2)),0 .[) & rseq is convergent & lim rseq = th holds
( (cosec | [.(- (PI / 2)),0 .[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0 .[) . th = lim ((cosec | [.(- (PI / 2)),0 .[) /* rseq) ) ) )

proof

now

let rseq be Real_Sequence; :: thesis: ( rng rseq c= dom (cosec | [.(- (PI / 2)),0 .[) & rseq is convergent & lim rseq = th implies ( (cosec | [.(- (PI / 2)),0 .[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0 .[) . th = lim ((cosec | [.(- (PI / 2)),0 .[) /* rseq) ) )
assume A3: ( rng rseq c= dom (cosec | [.(- (PI / 2)),0 .[) & rseq is convergent & lim rseq = th ) ; :: thesis: ( (cosec | [.(- (PI / 2)),0 .[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0 .[) . th = lim ((cosec | [.(- (PI / 2)),0 .[) /* rseq) )
A4: dom (cosec | [.(- (PI / 2)),0 .[) = [.(- (PI / 2)),0 .[ by Th3, RELAT_1:91;
then rng rseq c= dom cosec by A3, Th3, XBOOLE_1:1;
then A6: ( cosec /* rseq is convergent & cosec . th = lim (cosec /* rseq) ) by A2, A3, FCONT_1:def 1;
(cosec | [.(- (PI / 2)),0 .[) /* rseq = cosec /* rseq

proof

now

let n be Element of NAT ; :: thesis: ((cosec | [.(- (PI / 2)),0 .[) /* rseq) . n = (cosec /* rseq) . n
dom rseq = NAT by SEQ_1:3;
then rseq . n in rng rseq by FUNCT_1:def 5;
then A7: (cosec | [.(- (PI / 2)),0 .[) . (rseq . n) = cosec . (rseq . n) by A3, A4, FUNCT_1:72;
(cosec | [.(- (PI / 2)),0 .[) . (rseq . n) = ((cosec | [.(- (PI / 2)),0 .[) /* rseq) . n by A3, FUNCT_2:185;
hence ((cosec | [.(- (PI / 2)),0 .[) /* rseq) . n = (cosec /* rseq) . n by A3, A4, A7, Th3, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

hence (cosec | [.(- (PI / 2)),0 .[) /* rseq = cosec /* rseq by FUNCT_2:113; :: thesis: verum

end;

hence ( (cosec | [.(- (PI / 2)),0 .[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0 .[) . th = lim ((cosec | [.(- (PI / 2)),0 .[) /* rseq) ) by A0, A6, Lm19; :: thesis: verum

end;

hence ( th in dom (cosec | [.(- (PI / 2)),0 .[) & ( for rseq being Real_Sequence st rng rseq c= dom (cosec | [.(- (PI / 2)),0 .[) & rseq is convergent & lim rseq = th holds
( (cosec | [.(- (PI / 2)),0 .[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0 .[) . th = lim ((cosec | [.(- (PI / 2)),0 .[) /* rseq) ) ) ) by A0, Lm19; :: thesis: verum

end;

hence cosec | [.(- (PI / 2)),0 .[ is_continuous_in th by FCONT_1:def 1; :: thesis: verum

end;

hence cosec | [.(- (PI / 2)),0 .[ is continuous by FCONT_1:def 2; :: thesis: verum