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

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

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

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

end;

hence p /^ n is connected by GLIB_002:def 12; :: thesis: verum

end;

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

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

end;

end;