let k, m be Nat; :: thesis: ( 1 <= k & k <= m implies ( 0 < (x_r-seq m) . k & (x_r-seq m) . k < PI / 2 ) )
set f = x_r-seq m;
A1: rng (x_r-seq m) c= ].0,(PI / 2).[ by Th20;
A2: len (x_r-seq m) = m by Th19;
assume ( 1 <= k & k <= m ) ; :: thesis: ( 0 < (x_r-seq m) . k & (x_r-seq m) . k < PI / 2 )
then k in dom (x_r-seq m) by A2, FINSEQ_3:25;
then (x_r-seq m) . k in rng (x_r-seq m) by FUNCT_1:def 3;
hence ( 0 < (x_r-seq m) . k & (x_r-seq m) . k < PI / 2 ) by A1, XXREAL_1:4; :: thesis: verum