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 that
A1:
p is_oriented_edge_seq_of vs
and
A2:
q is_oriented_edge_seq_of vs
; :: thesis: p = q
A3: (len p) + 1 =
len vs
by A1, Def19
.=
(len q) + 1
by A2, Def19
;
now let k be
Nat;
:: thesis: ( 1 <= k & k <= len p implies p . k = q . k )assume A4:
( 1
<= k &
k <= len p )
;
:: thesis: 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;
:: thesis: verum end;
hence
p = q
by A3, FINSEQ_1:18; :: thesis: verum