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 Nat st 1 <= n & n <= len p holds
p . n in the carrier of G and
A4: for n being Nat st 1 <= n & n <= len c holds
ex x9, y9 being Element of the carrier of G st
( x9 = p . n & y9 = p . (n + 1) & c . n joins x9,y9 ) by GRAPH_1:def 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

now :: thesis: for i being Nat st i in dom p holds
p . i in the carrier of G

let i be Nat; :: thesis: ( i in dom p implies p . i in the carrier of G )
assume i in dom p ; :: thesis: p . i in the carrier of G
then A5: ( 1 <= i & i <= len p ) by FINSEQ_3:25;
thus 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:12;
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 2 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len c or c . b₁ joins p /. b₁,p /. (b₁ + 1) )
let n be Nat; :: thesis: ( not 1 <= n or not n <= len c or c . n joins p /. n,p /. (n + 1) )
assume that
A6: 1 <= n and
A7: n <= len c ; :: thesis: c . n joins p /. n,p /. (n + 1)
n + 1 <= len p by A2, A7, XREAL_1:6;
then A8: p /. (n + 1) = p . (n + 1) by FINSEQ_4:15, NAT_1:12;
( n <= len p & ex x9, y9 being Element of the carrier of G st
( x9 = p . n & y9 = p . (n + 1) & c . n joins x9,y9 ) ) by A2, A4, A6, A7, NAT_1:12;
hence c . n joins p /. n,p /. (n + 1) by A6, A8, FINSEQ_4:15; :: thesis: verum

end;

end;

assume A9: 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 A10: p is_vertex_seq_of c ; :: thesis: c is Chain of G

hereby :: according to GRAPH_1:def 14 :: thesis: ex b₁ being set st
( len b₁ = (len c) + 1 & ( for b₂ being set holds
( not 1 <= b₂ or not b₂ <= len b₁ or b₁ . b₂ in the carrier of G ) ) & ( for b₂ being set 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 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:25;
then A11: c . n in rng c by FUNCT_1:def 3;
rng c c= the carrier' of G by A9, FINSEQ_1:def 4;
hence c . n in the carrier' of G by A11; :: thesis: verum

end;

take p ; :: thesis: ( len p = (len c) + 1 & ( for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len p or p . b₁ in the carrier of G ) ) & ( for b₁ being set 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 A12: len p = (len c) + 1 by A10; :: thesis: ( ( for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len p or p . b₁ in the carrier of G ) ) & ( for b₁ being set 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 set 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 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:25;
then A13: p . n in rng p by FUNCT_1:def 3;
rng p c= the carrier of G by FINSEQ_1:def 4;
hence p . n in the carrier of G by A13; :: thesis: verum

end;

let n be 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 that
A14: 1 <= n and
A15: 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 x9 = p /. n; :: thesis: ex b₁ being Element of the carrier of G st
( x9 = p . n & b₁ = p . (n + 1) & c . n joins x9,b₁ )
take y9 = p /. (n + 1); :: thesis: ( x9 = p . n & y9 = p . (n + 1) & c . n joins x9,y9 )
( n <= len p & n + 1 <= len p ) by A12, A15, NAT_1:12, XREAL_1:6;
hence ( x9 = p . n & y9 = p . (n + 1) ) by A14, FINSEQ_4:15, NAT_1:12; :: thesis: c . n joins x9,y9
thus c . n joins x9,y9 by A10, A14, A15; :: thesis: verum