per cases ( n <= len p or not n <= len p ) ;

suppose A3: n <= len p ; :: thesis: p /^ n is Graph-yielding

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 A4: x in dom (p /^ n) ; :: thesis: (p /^ n) . x is _Graph
then reconsider i = x as Nat ;
n + i in dom p by A4, FINSEQ_5:26;
then p . (n + i) is _Graph by GLIB_000:def 53;
hence (p /^ n) . x is _Graph by A3, A4, RFINSEQ:def 1; :: thesis: verum

end;

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

end;

suppose not n <= len p ; :: thesis: p /^ n is Graph-yielding

hence p /^ n is Graph-yielding by RFINSEQ:def 1; :: thesis: verum

end;

end;