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

suppose A4: n <= len p ; :: thesis: p /^ n is non-trivial

now :: thesis: for x being object st x in dom (p /^ n) holds
ex G being _Graph st
( (p /^ n) . x = G & not G is _trivial )

let x be object ; :: thesis: ( x in dom (p /^ n) implies ex G being _Graph st
( (p /^ n) . x = G & not G is _trivial ) )
assume A5: x in dom (p /^ n) ; :: thesis: ex G being _Graph st
( (p /^ n) . x = G & not G is _trivial )
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 & not G is _trivial ) by GLIB_000:def 61;
take G = G; :: thesis: ( (p /^ n) . x = G & not G is _trivial )
thus ( (p /^ n) . x = G & not G is _trivial ) by A4, A5, A6, RFINSEQ:def 1; :: thesis: verum

end;

hence p /^ n is non-trivial by GLIB_000:def 61; :: thesis: verum

end;

suppose not n <= len p ; :: thesis: p /^ n is non-trivial

hence p /^ n is non-trivial by RFINSEQ:def 1; :: thesis: verum

end;

end;