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

proof

assume 1 <= len p ; :: thesis: ex k being Element of dom p st
( 1 = k & p . k is _finite )
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k ; :: thesis: ( 1 = k & p . k is _finite )
thus ( 1 = k & p . k is _finite ) 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 _finite )
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 _finite )
thus m + 1 = k ; :: thesis: p . k is _finite
(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 _finite ) by A5;
(m + 1) - 1 <= (len p) - 1 by A6, XREAL_1:9;

per cases then ( ex v being object st p . (k0 + 1) is addVertex of p . k0,v or ex v1, e, v2 being object st p . (k0 + 1) is addEdge of p . k0,v1,e,v2 ) by A2, A7;

suppose ex v being object st p . (k0 + 1) is addVertex of p . k0,v ; :: thesis: p . k is _finite

hence p . k is _finite by A7; :: thesis: verum

end;

suppose ex v1, e, v2 being object st p . (k0 + 1) is addEdge of p . k0,v1,e,v2 ; :: thesis: p . k is _finite

hence p . k is _finite by A7; :: thesis: verum

end;

end;

end;

A8: for m being non zero Nat holds S₁[m] from NAT_1:sch 10(A3, A4);
consider k being Element of dom p such that
A9: ( len p = k & p . k is _finite ) by A8;
thus p . (len p) is _finite by A9; :: thesis: verum