let seq1 be subsequence of seq; :: thesis: seq1 is bounded
consider Nseq being increasing sequence of NAT such that
A1: seq1 = seq * Nseq by VALUED_0:def 17;
consider M1 being Real such that
A2: M1 > 0 and
A3: for n being Nat holds ||.(seq . n).|| <= M1 by Def3;
take M = M1; :: according to BHSP_3:def 3 :: thesis: ( M > 0 & ( for n being Nat holds ||.(seq1 . n).|| <= M ) )
now :: thesis: for n being Nat holds ||.(seq1 . n).|| <= M
let n be Nat; :: thesis: ||.(seq1 . n).|| <= M
A4: n in NAT by ORDINAL1:def 12;
seq1 . n = seq . (Nseq . n) by A1, FUNCT_2:15, A4;
hence ||.(seq1 . n).|| <= M by A3; :: thesis: verum
end;
hence ( M > 0 & ( for n being Nat holds ||.(seq1 . n).|| <= M ) ) by A2; :: thesis: verum