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