let p be non empty Graph-yielding FinSequence; :: thesis: ( p . 1 is simple & p . 1 is connected & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty set st p . (n + 1) is addAdjVertexAll of p . n,v,V ) implies ( p . (len p) is simple & p . (len p) is connected ) )
assume that
A1: ( p . 1 is simple & p . 1 is connected ) and
A2: for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty set st p . (n + 1) is addAdjVertexAll of p . n,v,V ; :: thesis: ( p . (len p) is simple & p . (len p) is connected )
defpred S₁[ Nat] means ( $1 <= len p implies ex k being Element of dom p st
( $1 = k & p . k is simple & p . k is connected ) );
A3: S₁[1]

proof

assume 1 <= len p ; :: thesis: ex k being Element of dom p st
( 1 = k & p . k is simple & p . k is connected )
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k ; :: thesis: ( 1 = k & p . k is simple & p . k is connected )
thus ( 1 = k & p . k is simple & p . k is connected ) by A1; :: thesis: verum

end;

A4: for m being non zero Nat st S₁[m] holds
S₁[m + 1]

proof

let m be non zero Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
assume A6: m + 1 <= len p ; :: thesis: ex k being Element of dom p st
( m + 1 = k & p . k is simple & p . k is connected )
0 + 1 <= m + 1 by XREAL_1:6;
then reconsider k = m + 1 as Element of dom p by A6, FINSEQ_3:25;
take k ; :: thesis: ( m + 1 = k & p . k is simple & p . k is connected )
thus m + 1 = k ; :: thesis: ( p . k is simple & p . k is connected )
(m + 1) - 1 <= (len p) - 0 by A6, XREAL_1:13;
then consider k0 being Element of dom p such that
A7: ( m = k0 & p . k0 is simple & p . k0 is connected ) by A5;
(m + 1) - 1 <= (len p) - 1 by A6, XREAL_1:9;
then consider v being object , V being non empty set such that
A8: p . (k0 + 1) is addAdjVertexAll of p . k0,v,V by A2, A7;
thus ( p . k is simple & p . k is connected ) by A7, A8; :: thesis: verum

end;

for m being non zero Nat holds S₁[m] from NAT_1:sch 10(A3, A4);
then ex k being Element of dom p st
( len p = k & p . k is simple & p . k is connected ) ;
hence ( p . (len p) is simple & p . (len p) is connected ) ; :: thesis: verum