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

suppose A4: n <= len p ; :: thesis: p /^ n is acyclic

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 A5: x in dom (p /^ n) ; :: thesis: ex G being _Graph st
( (p /^ n) . x = G & G is acyclic )
then reconsider i = x as Nat ;
n + i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: ( p . (n + i) = 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 A4, A5, A6, RFINSEQ:def 1; :: thesis: verum

end;

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

end;

suppose not n <= len p ; :: thesis: p /^ n is acyclic

hence p /^ n is acyclic by RFINSEQ:def 1; :: thesis: verum

end;

end;