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, Def5;
A5:
len vs2 = (len c) + 1
by A3, Def5;
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, Def5;
A9:
n in NAT
by ORDINAL1:def 13;
per cases
( n < (len c) + 1 or n >= (len c) + 1 )
;
suppose
n < (len c) + 1
;
vs1 . n = vs2 . nthen A10:
n <= len c
by NAT_1:13;
then
c . n orientedly_joins vs1 /. n,
vs1 /. (n + 1)
by A2, A6, A9, Def5;
then A11:
the
Source of
G . (c . n) = vs1 /. n
by Def1;
c . n orientedly_joins vs2 /. n,
vs2 /. (n + 1)
by A3, A6, A9, A10, Def5;
then A12:
the
Source of
G . (c . n) = vs2 /. n
by Def1;
vs1 . n = vs1 /. n
by A6, A7, FINSEQ_4:24;
hence
vs1 . n = vs2 . n
by A4, A5, A6, A7, A11, A12, FINSEQ_4:24;
verum end; suppose
n >= (len c) + 1
;
vs1 . n = vs2 . nthen A13:
n = (len c) + 1
by A8, XXREAL_0:1;
then A14:
n - 1
= len c
;
A15:
0 + 1
<= len c
by A1, NAT_1:13;
then A16:
n - 1
= n -' 1
by A13, NAT_D:39;
A17:
n -' 1
= len c
by A14, A15, NAT_D:39;
then
c . (n -' 1) orientedly_joins vs1 /. (n -' 1),
vs1 /. ((n -' 1) + 1)
by A2, A15, Def5;
then A18:
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 A3, A15, A17, Def5;
then A19:
the
Target of
G . (c . (n -' 1)) = vs2 /. ((n -' 1) + 1)
by Def1;
vs1 . n = vs1 /. n
by A6, A7, FINSEQ_4:24;
hence
vs1 . n = vs2 . n
by A4, A5, A6, A7, A16, A18, A19, FINSEQ_4:24;
verum end;
end;
hence
vs1 = vs2
by A4, A5, FINSEQ_1:18; verum