let G be Graph; 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; 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; ( c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c implies vs1 = vs2 )
assume that
A1:
c <> {}
and
A2:
vs1 is_oriented_vertex_seq_of c
and
A3:
vs2 is_oriented_vertex_seq_of c
; vs1 = vs2
A4:
len vs1 = (len c) + 1
by A2;
A5:
len vs2 = (len c) + 1
by A3;
for n being Nat st 1 <= n & n <= len vs1 holds
vs1 . n = vs2 . n
proof
let n be
Nat;
( 1 <= n & n <= len vs1 implies vs1 . n = vs2 . n )
assume that A6:
1
<= n
and A7:
n <= len vs1
;
vs1 . n = vs2 . n
A8:
n <= (len c) + 1
by A2, A7;
per cases
( n < (len c) + 1 or n >= (len c) + 1 )
;
suppose
n < (len c) + 1
;
vs1 . n = vs2 . nthen A9:
n <= len c
by NAT_1:13;
then
c . n orientedly_joins vs1 /. n,
vs1 /. (n + 1)
by A2, A6;
then A10:
the
Source of
G . (c . n) = vs1 /. n
;
c . n orientedly_joins vs2 /. n,
vs2 /. (n + 1)
by A3, A6, A9;
then A11:
the
Source of
G . (c . n) = vs2 /. n
;
vs1 . n = vs1 /. n
by A6, A7, FINSEQ_4:15;
hence
vs1 . n = vs2 . n
by A4, A5, A6, A7, A10, A11, FINSEQ_4:15;
verum end; suppose
n >= (len c) + 1
;
vs1 . n = vs2 . nthen A12:
n = (len c) + 1
by A8, XXREAL_0:1;
then A13:
n - 1
= len c
;
A14:
0 + 1
<= len c
by A1, NAT_1:13;
then A15:
n - 1
= n -' 1
by A12, NAT_D:39;
A16:
n -' 1
= len c
by A13, A14, NAT_D:39;
then
c . (n -' 1) orientedly_joins vs1 /. (n -' 1),
vs1 /. ((n -' 1) + 1)
by A2, A14;
then A17:
the
Target of
G . (c . (n -' 1)) = vs1 /. ((n -' 1) + 1)
;
c . (n -' 1) orientedly_joins vs2 /. (n -' 1),
vs2 /. ((n -' 1) + 1)
by A3, A14, A16;
then A18:
the
Target of
G . (c . (n -' 1)) = vs2 /. ((n -' 1) + 1)
;
vs1 . n = vs1 /. n
by A6, A7, FINSEQ_4:15;
hence
vs1 . n = vs2 . n
by A4, A5, A6, A7, A15, A17, A18, FINSEQ_4:15;
verum end;
end;
hence
vs1 = vs2
by A4, A5, FINSEQ_1:14; verum