let G be Graph; :: thesis: for vs1, vs2 being FinSequence of the carrier of G
for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds
vs1 = vs2
let vs1, vs2 be FinSequence of the carrier of G; :: thesis: for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds
vs1 = vs2
let c be oriented Chain of G; :: thesis: ( c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c implies vs1 = vs2 )
assume A1:
( c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c )
; :: thesis: vs1 = vs2
then A2:
( len vs1 = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds
c . n orientedly_joins vs1 /. n,vs1 /. (n + 1) ) )
by Def5;
A3:
( len vs2 = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds
c . n orientedly_joins vs2 /. n,vs2 /. (n + 1) ) )
by A1, Def5;
for n being Nat st 1 <= n & n <= len vs1 holds
vs1 . n = vs2 . n
proof
let n be
Nat;
:: thesis: ( 1 <= n & n <= len vs1 implies vs1 . n = vs2 . n )
assume A4:
( 1
<= n &
n <= len vs1 )
;
:: thesis: vs1 . n = vs2 . n
then A5:
n <= (len c) + 1
by A1, Def5;
A6:
n in NAT
by ORDINAL1:def 13;
per cases
( n < (len c) + 1 or n >= (len c) + 1 )
;
suppose
n < (len c) + 1
;
:: thesis: vs1 . n = vs2 . nthen A7:
n <= len c
by NAT_1:13;
then
c . n orientedly_joins vs1 /. n,
vs1 /. (n + 1)
by A1, A4, A6, Def5;
then A8:
( the
Source of
G . (c . n) = vs1 /. n & the
Target of
G . (c . n) = vs1 /. (n + 1) )
by Def1;
c . n orientedly_joins vs2 /. n,
vs2 /. (n + 1)
by A1, A4, A6, A7, Def5;
then A9:
( the
Source of
G . (c . n) = vs2 /. n & the
Target of
G . (c . n) = vs2 /. (n + 1) )
by Def1;
vs1 . n = vs1 /. n
by A4, FINSEQ_4:24;
hence
vs1 . n = vs2 . n
by A2, A3, A4, A8, A9, FINSEQ_4:24;
:: thesis: verum end; suppose
n >= (len c) + 1
;
:: thesis: vs1 . n = vs2 . nthen A10:
n = (len c) + 1
by A5, XXREAL_0:1;
then A11:
n - 1
= len c
;
0 <> len c
by A1;
then
0 < len c
;
then A12:
0 + 1
<= len c
by NAT_1:13;
then A13:
n - 1
= n -' 1
by A10, NAT_D:39;
A14:
( 1
<= n -' 1 &
n -' 1
= len c )
by A11, A12, NAT_D:39;
then
c . (n -' 1) orientedly_joins vs1 /. (n -' 1),
vs1 /. ((n -' 1) + 1)
by A1, Def5;
then A15:
( the
Source of
G . (c . (n -' 1)) = vs1 /. (n -' 1) & the
Target of
G . (c . (n -' 1)) = vs1 /. ((n -' 1) + 1) )
by Def1;
c . (n -' 1) orientedly_joins vs2 /. (n -' 1),
vs2 /. ((n -' 1) + 1)
by A1, A14, Def5;
then A16:
( the
Source of
G . (c . (n -' 1)) = vs2 /. (n -' 1) & the
Target of
G . (c . (n -' 1)) = vs2 /. ((n -' 1) + 1) )
by Def1;
vs1 . n = vs1 /. n
by A4, FINSEQ_4:24;
hence
vs1 . n = vs2 . n
by A2, A3, A4, A13, A15, A16, FINSEQ_4:24;
:: thesis: verum end;
end;
hence
vs1 = vs2
by A2, A3, FINSEQ_1:18; :: thesis: verum