len p in dom p by FINSEQ_5:6;
hence p . (len p) is [Graph-like] ; :: thesis: verum