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 ( ( c <> {} & ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ) or ( c = {} & ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ) )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,
object ]
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
object 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(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
Nat st 1
<= n &
n <= len c holds
c . n orientedly_joins vs /. n,
vs /. (n + 1)
proof
let n be
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:1;
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:1;
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:15;
1
< n + 1
by A15, NAT_1:13;
then
the
Target of
G . (c . n) = vs /. (n + 1)
by A5, A17, A20, FINSEQ_4:15;
hence
c . n orientedly_joins vs /. n,
vs /. (n + 1)
by A21;
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:1;
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:1;
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:15;
1
< n + 1
by A15, NAT_1:13;
then
vs /. (n + 1) = p . (n + 1)
by A5, A23, FINSEQ_4:15;
then
the
Target of
G . (c . n) = vs /. (n + 1)
by A15, A22, A26, GRAPH_1:def 15;
hence
c . n orientedly_joins vs /. n,
vs /. (n + 1)
by A27;
verum end; end;
end; then
vs is_oriented_vertex_seq_of c
by A5;
hence
ex
vs being
FinSequence of the
carrier of
G st
vs is_oriented_vertex_seq_of c
;
verum end; end; end;
hence
ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
; verum