let G be Graph; 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; ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
now per cases
( c <> {} or c = {} )
;
case A1:
c <> {}
;
ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of cdefpred 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) ) );
A2:
for
k being
Nat st
k in Seg ((len c) + 1) holds
ex
x being
set st
S1[
k,
x]
proof
let k be
Nat;
( k in Seg ((len c) + 1) implies ex x being set st S1[k,x] )
assume
k in Seg ((len c) + 1)
;
ex x being set st S1[k,x]
hence
ex
x being
set st
S1[
k,
x]
;
verum
end;
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(A2);
then consider p being
FinSequence such that A3:
dom p = Seg ((len c) + 1)
and A4:
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 A3, 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 ;
( 1 <= n & n <= len c implies c . n orientedly_joins vs /. n,vs /. (n + 1) )
assume that A15:
1
<= n
and A16:
n <= len c
;
c . n orientedly_joins vs /. n,vs /. (n + 1)
per cases
( n = len c or n <> len c )
;
suppose A17:
n = len c
;
c . n orientedly_joins vs /. n,vs /. (n + 1)then A18:
n < (len c) + 1
by NAT_1:13;
then
n in Seg ((len c) + 1)
by A15, FINSEQ_1:3;
then A19:
p . n = the
Source of
G . (c . n)
by A4, A18;
1
< n + 1
by A15, NAT_1:13;
then
n + 1
in Seg ((len c) + 1)
by A17, FINSEQ_1:3;
then A20:
p . (n + 1) = the
Target of
G . (c . (len c))
by A4, A17;
A21:
the
Source of
G . (c . n) = vs /. n
by A5, A15, A18, A19, FINSEQ_4:24;
1
< n + 1
by A15, NAT_1:13;
then
the
Target of
G . (c . n) = vs /. (n + 1)
by A5, A17, A20, FINSEQ_4:24;
hence
c . n orientedly_joins vs /. n,
vs /. (n + 1)
by A21, Def1;
verum end; suppose
n <> len c
;
c . n orientedly_joins vs /. n,vs /. (n + 1)then A22:
n < len c
by A16, XXREAL_0:1;
then
n + 1
<= len c
by NAT_1:13;
then A23:
n + 1
< (len c) + 1
by NAT_1:13;
A24:
n < (len c) + 1
by A16, NAT_1:13;
then
n in Seg ((len c) + 1)
by A15, FINSEQ_1:3;
then A25:
p . n = the
Source of
G . (c . n)
by A4, A24;
1
< n + 1
by A15, NAT_1:13;
then
n + 1
in Seg ((len c) + 1)
by A23, FINSEQ_1:3;
then A26:
p . (n + 1) = the
Source of
G . (c . (n + 1))
by A4, A23;
A27:
the
Source of
G . (c . n) = vs /. n
by A5, A15, A24, A25, FINSEQ_4:24;
1
< n + 1
by A15, NAT_1:13;
then
vs /. (n + 1) = p . (n + 1)
by A5, A23, FINSEQ_4:24;
then
the
Target of
G . (c . n) = vs /. (n + 1)
by A15, A22, A26, GRAPH_1:def 13;
hence
c . n orientedly_joins vs /. n,
vs /. (n + 1)
by A27, Def1;
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
;
verum end;
hence
ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
; verum