let f be sequence of REAL; :: thesis: for n being Nat holds f | n is XFinSequence
let n be Nat; :: thesis: f | n is XFinSequence
dom f = NAT by FUNCT_2:def 1;
then dom (f | (Segm n)) = Segm n ;
then ( f | n is finite & f | n is Sequence-like ) ;
hence f | n is XFinSequence ; :: thesis: verum