len p in dom p by FINSEQ_5:6;
hence ( p . (len p) is Function-like & p . (len p) is Relation-like ) ; :: thesis: verum