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

proof

let th be Real; :: thesis: ( th in dom (cosec | ].0,(PI / 2).]) implies cosec | ].0,(PI / 2).] is_continuous_in th )
A1: sin is_differentiable_in th by SIN_COS:64;
assume A2: th in dom (cosec | ].0,(PI / 2).]) ; :: thesis: cosec | ].0,(PI / 2).] is_continuous_in th
then th in ].0,(PI / 2).] by RELAT_1:57;
then sin . th <> 0 by Lm4, COMPTRIG:7;
then A3: cosec is_continuous_in th by A1, FCONT_1:10, FDIFF_1:24;

now :: thesis: for rseq being Real_Sequence st rng rseq c= dom (cosec | ].0,(PI / 2).]) & rseq is convergent & lim rseq = th holds
( (cosec | ].0,(PI / 2).]) /* rseq is convergent & (cosec | ].0,(PI / 2).]) . th = lim ((cosec | ].0,(PI / 2).]) /* rseq) )

let rseq be Real_Sequence; :: thesis: ( rng rseq c= dom (cosec | ].0,(PI / 2).]) & rseq is convergent & lim rseq = th implies ( (cosec | ].0,(PI / 2).]) /* rseq is convergent & (cosec | ].0,(PI / 2).]) . th = lim ((cosec | ].0,(PI / 2).]) /* rseq) ) )
assume that
A4: rng rseq c= dom (cosec | ].0,(PI / 2).]) and
A5: ( rseq is convergent & lim rseq = th ) ; :: thesis: ( (cosec | ].0,(PI / 2).]) /* rseq is convergent & (cosec | ].0,(PI / 2).]) . th = lim ((cosec | ].0,(PI / 2).]) /* rseq) )
A6: dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] by Th4, RELAT_1:62;

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

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

end;

then A8: (cosec | ].0,(PI / 2).]) /* rseq = cosec /* rseq by FUNCT_2:63;
A9: rng rseq c= dom cosec by A4, A6, Th4;
then cosec . th = lim (cosec /* rseq) by A3, A5, FCONT_1:def 1;
hence ( (cosec | ].0,(PI / 2).]) /* rseq is convergent & (cosec | ].0,(PI / 2).]) . th = lim ((cosec | ].0,(PI / 2).]) /* rseq) ) by A2, A3, A5, A9, A8, Lm36, FCONT_1:def 1; :: thesis: verum

end;

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

end;

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