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

proof

let th be Real; :: thesis: ( th in dom (cosec | [.(- (PI / 2)),0.[) implies cosec | [.(- (PI / 2)),0.[ is_continuous_in th )
assume A1: th in dom (cosec | [.(- (PI / 2)),0.[) ; :: thesis: cosec | [.(- (PI / 2)),0.[ is_continuous_in th
then A2: th in [.(- (PI / 2)),0.[ by RELAT_1:57;
then th < 0 by Lm3, XXREAL_1:4;
then A3: th + (2 * PI) < 0 + (2 * PI) by XREAL_1:8;
- PI < th by A2, Lm3, XXREAL_1:4;
then (- PI) + (2 * PI) < th + (2 * PI) by XREAL_1:8;
then th + (2 * PI) in ].PI,(2 * PI).[ by A3;
then sin . (th + (2 * PI)) <> 0 by COMPTRIG:9;
then A4: sin . th <> 0 by SIN_COS:78;
sin is_differentiable_in th by SIN_COS:64;
then A5: cosec is_continuous_in th by A4, FCONT_1:10, FDIFF_1:24;

now :: thesis: 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) )

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 that
A6: rng rseq c= dom (cosec | [.(- (PI / 2)),0.[) and
A7: ( 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) )
A8: dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ by Th3, RELAT_1:62;

now :: thesis: for n being Element of NAT holds ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . n

let n be Element of NAT ; :: thesis: ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . n
dom rseq = NAT by SEQ_1:1;
then rseq . n in rng rseq by FUNCT_1:def 3;
then A9: (cosec | [.(- (PI / 2)),0.[) . (rseq . n) = cosec . (rseq . n) by A6, A8, FUNCT_1:49;
(cosec | [.(- (PI / 2)),0.[) . (rseq . n) = ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n by A6, FUNCT_2:108;
hence ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . n by A6, A8, A9, Th3, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum

end;

then A10: (cosec | [.(- (PI / 2)),0.[) /* rseq = cosec /* rseq by FUNCT_2:63;
A11: rng rseq c= dom cosec by A6, A8, Th3;
then cosec . th = lim (cosec /* rseq) by A5, A7, FCONT_1:def 1;
hence ( (cosec | [.(- (PI / 2)),0.[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) ) by A1, A5, A7, A11, A10, Lm35, FCONT_1:def 1; :: 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