let e be Element of X; :: thesis: e is FinSequence-like
( X is empty or not X is empty ) ;
then ( e is empty or e in X ) by SUBSET_1:def 2;
hence e is FinSequence-like by Def19; :: thesis: verum