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
reconsider f = fss | Y as FinSubsequence ;
f c= fss by RELAT_1:59;
hence fss | Y is Subset of fs by XBOOLE_1:1; :: thesis: verum