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
.= (len q) + 1 by A2 ;

now :: thesis: for k being Nat st 1 <= k & k <= len p holds
p . k = q . k

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 . k
then A5: the Target of G . (p . k) = vs . (k + 1) by A1
.= the Target of G . (q . k) by A2, A3, A4 ;
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
.= the Source of G . (q . k) by A2, A3, A4 ;
hence p . k = q . k by A5, A6, GRAPH_1:def 7; :: thesis: verum

end;

hence p = q by A3, FINSEQ_1:14; :: thesis: verum