let X be ComplexUnitarySpace; :: thesis: for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
let seq, seq1 be sequence of X; :: thesis: ( seq is bounded & seq1 is subsequence of seq implies seq1 is bounded )
assume that
A1: seq is bounded and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is bounded
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def 17;
consider M1 being Real such that
A4: M1 > 0 and
A5: for n being Nat holds ||.(seq . n).|| <= M1 by A1;
take M = M1; :: according to CLVECT_2:def 10 :: 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
n in NAT by ORDINAL1:def 12;
then seq1 . n = seq . (Nseq . n) by A3, FUNCT_2:15;
hence ||.(seq1 . n).|| <= M by A5; :: thesis: verum

end;

hence ( M > 0 & ( for n being Nat holds ||.(seq1 . n).|| <= M ) ) by A4; :: thesis: verum