let G be oriented Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs implies p = q )
assume A1:
( p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs )
; :: thesis: p = q
then A2: (len p) + 1 =
len vs
by Def19
.=
(len q) + 1
by A1, Def19
;
now let k be
Nat;
:: thesis: ( 1 <= k & k <= len p implies p . k = q . k )assume A3:
( 1
<= k &
k <= len p )
;
:: thesis: p . k = q . kthen A4: the
Source of
G . (p . k) =
vs . k
by A1, Def19
.=
the
Source of
G . (q . k)
by A1, A2, A3, Def19
;
A5: the
Target of
G . (p . k) =
vs . (k + 1)
by A1, A3, Def19
.=
the
Target of
G . (q . k)
by A1, A2, A3, Def19
;
(
p . k in the
carrier' of
G &
q . k in the
carrier' of
G )
by A2, A3, Th2;
hence
p . k = q . k
by A4, A5, GRAPH_1:def 5;
:: thesis: verum end;
hence
p = q
by A2, FINSEQ_1:18; :: thesis: verum