let G be Graph; :: thesis: for c being oriented Chain of G ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
let c be oriented Chain of G; :: thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
now per cases
( c <> {} or c = {} )
;
case
c <> {}
;
:: thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of cthen A1:
len c <> 0
;
defpred S1[
Nat,
set ]
means ( ( $1
= (len c) + 1 implies $2
= the
Target of
G . (c . (len c)) ) & ( $1
<> (len c) + 1 implies $2
= the
Source of
G . (c . $1) ) );
A3:
for
k being
Nat st
k in Seg ((len c) + 1) holds
ex
x being
set st
S1[
k,
x]
ex
p being
FinSequence st
(
dom p = Seg ((len c) + 1) & ( for
k being
Nat st
k in Seg ((len c) + 1) holds
S1[
k,
p . k] ) )
from FINSEQ_1:sch 1(A3);
then consider p being
FinSequence such that A4:
(
dom p = Seg ((len c) + 1) & ( for
k being
Nat st
k in Seg ((len c) + 1) holds
( (
k = (len c) + 1 implies
p . k = the
Target of
G . (c . (len c)) ) & (
k <> (len c) + 1 implies
p . k = the
Source of
G . (c . k) ) ) ) )
;
A5:
len p = (len c) + 1
by A4, FINSEQ_1:def 3;
rng p c= the
carrier of
G
then reconsider vs =
p as
FinSequence of the
carrier of
G by FINSEQ_1:def 4;
for
n being
Element of
NAT st 1
<= n &
n <= len c holds
c . n orientedly_joins vs /. n,
vs /. (n + 1)
proof
let n be
Element of
NAT ;
:: thesis: ( 1 <= n & n <= len c implies c . n orientedly_joins vs /. n,vs /. (n + 1) )
assume A13:
( 1
<= n &
n <= len c )
;
:: thesis: c . n orientedly_joins vs /. n,vs /. (n + 1)
per cases
( n = len c or n <> len c )
;
suppose A14:
n = len c
;
:: thesis: c . n orientedly_joins vs /. n,vs /. (n + 1)then A15:
n < (len c) + 1
by NAT_1:13;
then
n in Seg ((len c) + 1)
by A13, FINSEQ_1:3;
then A16:
p . n = the
Source of
G . (c . n)
by A4, A15;
1
< n + 1
by A13, NAT_1:13;
then
n + 1
in Seg ((len c) + 1)
by A14, FINSEQ_1:3;
then A17:
p . (n + 1) = the
Target of
G . (c . (len c))
by A4, A14;
A18:
the
Source of
G . (c . n) = vs /. n
by A5, A13, A15, A16, FINSEQ_4:24;
1
< n + 1
by A13, NAT_1:13;
then
the
Target of
G . (c . n) = vs /. (n + 1)
by A5, A14, A17, FINSEQ_4:24;
hence
c . n orientedly_joins vs /. n,
vs /. (n + 1)
by A18, Def1;
:: thesis: verum end; suppose
n <> len c
;
:: thesis: c . n orientedly_joins vs /. n,vs /. (n + 1)then A19:
n < len c
by A13, XXREAL_0:1;
then
n + 1
<= len c
by NAT_1:13;
then A20:
n + 1
< (len c) + 1
by NAT_1:13;
A21:
n < (len c) + 1
by A13, NAT_1:13;
then
n in Seg ((len c) + 1)
by A13, FINSEQ_1:3;
then A22:
p . n = the
Source of
G . (c . n)
by A4, A21;
1
< n + 1
by A13, NAT_1:13;
then
n + 1
in Seg ((len c) + 1)
by A20, FINSEQ_1:3;
then A23:
p . (n + 1) = the
Source of
G . (c . (n + 1))
by A4, A20;
A24:
the
Source of
G . (c . n) = vs /. n
by A5, A13, A21, A22, FINSEQ_4:24;
1
< n + 1
by A13, NAT_1:13;
then
vs /. (n + 1) = p . (n + 1)
by A5, A20, FINSEQ_4:24;
then
the
Target of
G . (c . n) = vs /. (n + 1)
by A13, A19, A23, GRAPH_1:def 13;
hence
c . n orientedly_joins vs /. n,
vs /. (n + 1)
by A24, Def1;
:: thesis: verum end;
end; then
vs is_oriented_vertex_seq_of c
by A5, Def5;
hence
ex
vs being
FinSequence of the
carrier of
G st
vs is_oriented_vertex_seq_of c
;
:: thesis: verum end;
hence
ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
; :: thesis: verum