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 ;

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

hence
p = q
by A3, FINSEQ_1:14; :: thesis: verump . 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;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