let x be Element of Funcs (a,X); :: thesis: x is T-Sequence-like
dom x = a by FUNCT_2:92;
hence x is T-Sequence-like by ORDINAL1:def 7; :: thesis: verum