let G be oriented Graph; for vs being FinSequence
for p, q being oriented Chain of G st p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs holds
p = q
let vs be FinSequence; for p, q being oriented Chain of G st p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs holds
p = q
let p, q be oriented Chain of G; ( p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs implies p = q )
assume that
A1:
p is_oriented_edge_seq_of vs
and
A2:
q is_oriented_edge_seq_of vs
; p = q
A3: (len p) + 1 =
len vs
by A1, Def19
.=
(len q) + 1
by A2, Def19
;
now let k be
Nat;
( 1 <= k & k <= len p implies p . k = q . k )assume A4:
( 1
<= k &
k <= len p )
;
p . k = q . kthen A5: the
Target of
G . (p . k) =
vs . (k + 1)
by A1, Def19
.=
the
Target of
G . (q . k)
by A2, A3, A4, Def19
;
A6:
(
p . k in the
carrier' of
G &
q . k in the
carrier' of
G )
by A3, A4, Th2;
the
Source of
G . (p . k) =
vs . k
by A1, A4, Def19
.=
the
Source of
G . (q . k)
by A2, A3, A4, Def19
;
hence
p . k = q . k
by A5, A6, GRAPH_1:def 5;
verum end;
hence
p = q
by A3, FINSEQ_1:18; verum