A1: p | n = p | (Seg n) by FINSEQ_1:def 16;

now :: thesis: for x being object st x in dom (p | n) holds
(p | n) . x is _Graph

let x be object ; :: thesis: ( x in dom (p | n) implies (p | n) . x is _Graph )
assume A2: x in dom (p | n) ; :: thesis: (p | n) . x is _Graph
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then p . x is _Graph by GLIB_000:def 53;
hence (p | n) . x is _Graph by A1, A2, FUNCT_1:47; :: thesis: verum

end;

hence p | n is Graph-yielding by GLIB_000:def 53; :: thesis: verum