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

now :: thesis: for x being object st x in dom (p | n) holds
ex G being _Graph st
( (p | n) . x = G & G is acyclic )

let x be object ; :: thesis: ( x in dom (p | n) implies ex G being _Graph st
( (p | n) . x = G & G is acyclic ) )
assume A2: x in dom (p | n) ; :: thesis: ex G being _Graph st
( (p | n) . x = G & G is acyclic )
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: ( p . x = G & G is acyclic ) by GLIB_002:def 13;
take G = G; :: thesis: ( (p | n) . x = G & G is acyclic )
thus ( (p | n) . x = G & G is acyclic ) by A1, A3, A2, FUNCT_1:47; :: thesis: verum

end;

hence p | n is acyclic by GLIB_002:def 13; :: thesis: verum