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;
dom (fss | Y) c= dom fss by RELAT_1:89;
then dom (fss | Y) c= Seg k by A1, XBOOLE_1:1;
then reconsider f = fss | Y as FinSubsequence by FINSEQ_1:def 12;
( f c= fss & fss c= fs ) by RELAT_1:88;
hence fss | Y is Subset of fs by XBOOLE_1:1; :: thesis: verum