let X be set ; :: thesis: for fs being FinSequence of X holds fs is Subset of fs
let fs be FinSequence of X; :: thesis: fs is Subset of fs
reconsider fs' = fs as FinSubsequence by FINSEQ_1:68;
fs' c= fs ;
hence fs is Subset of fs ; :: thesis: verum