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

proof

assume 1 <= len p ; :: thesis: ex k being Element of dom p st
( 1 = k & p . k is simple )
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k ; :: thesis: ( 1 = k & p . k is simple )
thus ( 1 = k & p . k is simple ) 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 )
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 )
thus m + 1 = k ; :: thesis: p . k is simple
(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 ) by A5;
(m + 1) - 1 <= (len p) - 1 by A6, XREAL_1:9;
then consider v being object , V being set such that
A8: p . (k0 + 1) is addAdjVertexAll of p . k0,v,V by A2, A7;
thus p . k is simple 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 ) ;
hence p . (len p) is simple ; :: thesis: verum