let e be Element of X; :: thesis: e is FinSequence-like
( X is empty or not X is empty ) ;
hence e is FinSequence-like by Def18, SUBSET_1:def 1; :: thesis: verum