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

fs c= fs ;

hence fs is Subset of fs ; :: thesis: verum

let fs be FinSequence of X; :: thesis: fs is Subset of fs

fs c= fs ;

hence fs is Subset of fs ; :: thesis: verum