( x in dom f or x nin dom f ) ;
then ( f . x in X ^omega or f . x = <%> X ) by FUNCT_1:def 2, FUNCT_1:102;
hence ( f . x is Sequence-like & f . x is finite & f . x is Function-like & f . x is Relation-like ) ; :: thesis: verum