let p be non empty Graph-yielding FinSequence; ( p . 1 is Tree-like & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st p . (n + 1) is addAdjVertex of p . n,v1,e,v2 ) implies p . (len p) is Tree-like )
assume that
A1:
p . 1 is Tree-like
and
A2:
for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st p . (n + 1) is addAdjVertex of p . n,v1,e,v2
; p . (len p) is Tree-like
defpred S1[ Nat] means ( $1 <= len p implies ex k being Element of dom p st
( $1 = k & p . k is Tree-like ) );
A3:
S1[1]
A4:
for m being non zero Nat st S1[m] holds
S1[m + 1]
proof
let m be non
zero Nat;
( S1[m] implies S1[m + 1] )
assume A5:
S1[
m]
;
S1[m + 1]
assume A6:
m + 1
<= len p
;
ex k being Element of dom p st
( m + 1 = k & p . k is Tree-like )
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
;
( m + 1 = k & p . k is Tree-like )
thus
m + 1
= k
;
p . k is Tree-like
(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
Tree-like )
by A5;
(m + 1) - 1
<= (len p) - 1
by A6, XREAL_1:9;
then consider v1,
e,
v2 being
object such that A8:
p . (k0 + 1) is
addAdjVertex of
p . k0,
v1,
e,
v2
by A2, A7;
thus
p . k is
Tree-like
by A7, A8;
verum
end;
A9:
for m being non zero Nat holds S1[m]
from NAT_1:sch 10(A3, A4);
consider k being Element of dom p such that
A10:
( len p = k & p . k is Tree-like )
by A9;
thus
p . (len p) is Tree-like
by A10; verum