let G be Graph; for pe being FinSequence of the carrier' of G st len pe = 1 holds
pe is oriented Simple Chain of G
let pe be FinSequence of the carrier' of G; ( len pe = 1 implies pe is oriented Simple Chain of G )
set p = pe;
set v1 = the Source of G . (pe . 1);
set v2 = the Target of G . (pe . 1);
assume A2:
len pe = 1
; pe is oriented Simple Chain of G
then
1 in dom pe
by FINSEQ_3:25;
then reconsider v1 = the Source of G . (pe . 1), v2 = the Target of G . (pe . 1) as Element of G by FINSEQ_2:11, FUNCT_2:5;
set vs = <*v1,v2*>;
A3:
len <*v1,v2*> = (len pe) + 1
by A2, FINSEQ_1:44;
A4:
now for n being Nat st 1 <= n & n <= len pe holds
ex v1, v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )let n be
Nat;
( 1 <= n & n <= len pe implies ex v1, v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 ) )assume
( 1
<= n &
n <= len pe )
;
ex v1, v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )then A5:
n = 1
by A2, XXREAL_0:1;
take v1 =
v1;
ex v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )take v2 =
v2;
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )thus
(
v1 = <*v1,v2*> . n &
v2 = <*v1,v2*> . (n + 1) )
by A5, FINSEQ_1:44;
pe . n joins v1,v2thus
pe . n joins v1,
v2
by A5, GRAPH_1:def 12;
verum end;
A6:
len <*v1,v2*> = 2
by FINSEQ_1:44;
A7:
now for n, m being Nat st 1 <= n & n < m & m <= len <*v1,v2*> & <*v1,v2*> . n = <*v1,v2*> . m holds
( n = 1 & m = len <*v1,v2*> )let n,
m be
Nat;
( 1 <= n & n < m & m <= len <*v1,v2*> & <*v1,v2*> . n = <*v1,v2*> . m implies ( n = 1 & m = len <*v1,v2*> ) )assume that A8:
1
<= n
and A9:
n < m
and A10:
m <= len <*v1,v2*>
and
<*v1,v2*> . n = <*v1,v2*> . m
;
( n = 1 & m = len <*v1,v2*> )
n < 1
+ 1
by A6, A9, A10, XXREAL_0:2;
then
n <= 1
by NAT_1:13;
hence
n = 1
by A8, XXREAL_0:1;
m = len <*v1,v2*>
1
< m
by A8, A9, XXREAL_0:2;
then
1
+ 1
< m + 1
by XREAL_1:8;
then
2
<= m
by NAT_1:13;
hence
m = len <*v1,v2*>
by A6, A10, XXREAL_0:1;
verum end;
A14:
for n being Nat st 1 <= n & n < len pe holds
not the Source of G . (pe . (n + 1)) <> the Target of G . (pe . n)
by A2;
now for n being Nat st 1 <= n & n <= len pe holds
pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1)let n be
Nat;
( 1 <= n & n <= len pe implies pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1) )assume
( 1
<= n &
n <= len pe )
;
pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1)then A15:
n = 1
by A2, XXREAL_0:1;
(
<*v1,v2*> /. 1
= v1 &
<*v1,v2*> /. (1 + 1) = v2 )
by FINSEQ_4:17;
hence
pe . n orientedly_joins <*v1,v2*> /. n,
<*v1,v2*> /. (n + 1)
by A15, GRAPH_4:def 1;
verum end;
then
<*v1,v2*> is_oriented_vertex_seq_of pe
by A3, GRAPH_4:def 5;
hence
pe is oriented Simple Chain of G
by A3, A7, A1, A11, A4, A14, GRAPH_1:def 14, GRAPH_1:def 15, GRAPH_4:def 7; verum