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

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