let c be FinSequence; :: thesis: ( c is Chain of G iff ( c is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of c ) )

hereby :: thesis: ( c is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of c implies c is Chain of G )

assume A1: c is Chain of G ; :: thesis: ( c is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of c )
then consider p being FinSequence such that
A2: len p = (len c) + 1 and
A3: for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G and
A4: for n being Element of NAT st 1 <= n & n <= len c holds
ex x', y' being Element of the carrier of G st
( x' = p . n & y' = p . (n + 1) & c . n joins x',y' ) by GRAPH_1:def 12;

now

let i be Nat; :: thesis: ( i in dom p implies p . i in the carrier of G )
A5: i in NAT by ORDINAL1:def 13;
assume i in dom p ; :: thesis: p . i in the carrier of G
then ( 1 <= i & i <= len p ) by FINSEQ_3:27;
hence p . i in the carrier of G by A3, A5; :: thesis: verum

end;

then reconsider p = p as FinSequence of the carrier of G by FINSEQ_2:14;
thus c is FinSequence of the carrier' of G by A1; :: thesis: ex p being FinSequence of the carrier of G st p is_vertex_seq_of c
take p = p; :: thesis: p is_vertex_seq_of c
thus p is_vertex_seq_of c :: thesis: verum

proof

thus len p = (len c) + 1 by A2; :: according to GRAPH_2:def 7 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len c or c . b₁ joins p /. b₁,p /. (b₁ + 1) )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not n <= len c or c . n joins p /. n,p /. (n + 1) )
assume A6: ( 1 <= n & n <= len c ) ; :: thesis: c . n joins p /. n,p /. (n + 1)
then ( 1 <= n + 1 & n <= len p & n + 1 <= len p ) by A2, NAT_1:12, XREAL_1:8;
then A7: ( p /. n = p . n & p /. (n + 1) = p . (n + 1) ) by A6, FINSEQ_4:24;
ex x', y' being Element of the carrier of G st
( x' = p . n & y' = p . (n + 1) & c . n joins x',y' ) by A4, A6;
hence c . n joins p /. n,p /. (n + 1) by A7; :: thesis: verum

end;

end;

assume A8: c is FinSequence of the carrier' of G ; :: thesis: ( for p being FinSequence of the carrier of G holds not p is_vertex_seq_of c or c is Chain of G )
given p being FinSequence of the carrier of G such that A9: p is_vertex_seq_of c ; :: thesis: c is Chain of G

hereby :: according to GRAPH_1:def 12 :: thesis: ex b₁ being set st
( len b₁ = (len c) + 1 & ( for b₂ being Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or b₁ . b₂ in the carrier of G ) ) & ( for b₂ being Element of NAT holds
( not 1 <= b₂ or not b₂ <= len c or ex b₃, b₄ being Element of the carrier of G st
( b₃ = b₁ . b₂ & b₄ = b₁ . (b₂ + 1) & c . b₂ joins b₃,b₄ ) ) ) )

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len c implies c . n in the carrier' of G )
assume ( 1 <= n & n <= len c ) ; :: thesis: c . n in the carrier' of G
then n in dom c by FINSEQ_3:27;
then ( c . n in rng c & rng c c= the carrier' of G ) by A8, FINSEQ_1:def 4, FUNCT_1:def 5;
hence c . n in the carrier' of G ; :: thesis: verum

end;

take p ; :: thesis: ( len p = (len c) + 1 & ( for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len p or p . b₁ in the carrier of G ) ) & ( for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len c or ex b₂, b₃ being Element of the carrier of G st
( b₂ = p . b₁ & b₃ = p . (b₁ + 1) & c . b₁ joins b₂,b₃ ) ) ) )
thus A10: len p = (len c) + 1 by A9, GRAPH_2:def 7; :: thesis: ( ( for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len p or p . b₁ in the carrier of G ) ) & ( for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len c or ex b₂, b₃ being Element of the carrier of G st
( b₂ = p . b₁ & b₃ = p . (b₁ + 1) & c . b₁ joins b₂,b₃ ) ) ) )

hereby :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len c or ex b₂, b₃ being Element of the carrier of G st
( b₂ = p . b₁ & b₃ = p . (b₁ + 1) & c . b₁ joins b₂,b₃ ) )

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len p implies p . n in the carrier of G )
assume ( 1 <= n & n <= len p ) ; :: thesis: p . n in the carrier of G
then n in dom p by FINSEQ_3:27;
then ( p . n in rng p & rng p c= the carrier of G ) by FINSEQ_1:def 4, FUNCT_1:def 5;
hence p . n in the carrier of G ; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( not 1 <= n or not n <= len c or ex b₁, b₂ being Element of the carrier of G st
( b₁ = p . n & b₂ = p . (n + 1) & c . n joins b₁,b₂ ) )
assume A11: ( 1 <= n & n <= len c ) ; :: thesis: ex b₁, b₂ being Element of the carrier of G st
( b₁ = p . n & b₂ = p . (n + 1) & c . n joins b₁,b₂ )
take x' = p /. n; :: thesis: ex b₁ being Element of the carrier of G st
( x' = p . n & b₁ = p . (n + 1) & c . n joins x',b₁ )
take y' = p /. (n + 1); :: thesis: ( x' = p . n & y' = p . (n + 1) & c . n joins x',y' )
( 1 <= n + 1 & n <= len p & n + 1 <= len p ) by A10, A11, NAT_1:12, XREAL_1:8;
hence ( x' = p . n & y' = p . (n + 1) ) by A11, FINSEQ_4:24; :: thesis: c . n joins x',y'
thus c . n joins x',y' by A9, A11, GRAPH_2:def 7; :: thesis: verum