let E be set ; :: thesis: ( E is empty implies E is T-Sequence-like )
assume E is empty ; :: thesis: E is T-Sequence-like
then proj1 E = {} ;
hence E is T-Sequence-like by Def7; :: thesis: verum