let X, Y be set ; :: thesis: for fs being FinSequence of X
for fss being Subset of fs holds fss | Y is Subset of fs
let fs be FinSequence of X; :: thesis: for fss being Subset of fs holds fss | Y is Subset of fs
let fss be Subset of fs; :: thesis: fss | Y is Subset of fs
consider k being Nat such that
A1: dom fss c= Seg k by FINSEQ_1:def 12;
reconsider f = fss | Y as FinSubsequence ;
f c= fss by RELAT_1:88;
hence fss | Y is Subset of fs by XBOOLE_1:1; :: thesis: verum