let G be Graph; :: thesis: for vs1, vs2 being FinSequence
for p being oriented Chain of G st p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1 holds
vs1 = vs2
let vs1, vs2 be FinSequence; :: thesis: for p being oriented Chain of G st p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1 holds
vs1 = vs2
let p be oriented Chain of G; :: thesis: ( p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1 implies vs1 = vs2 )
assume that
A1: p is_oriented_edge_seq_of vs1 and
A2: p is_oriented_edge_seq_of vs2 and
A3: len p >= 1 ; :: thesis: vs1 = vs2
A4: now :: thesis: for k being Nat st 1 <= k & k <= len vs1 holds
vs1 . k = vs2 . k
let k be Nat; :: thesis: ( 1 <= k & k <= len vs1 implies vs1 . b1 = vs2 . b1 )
assume that
A5: 1 <= k and
A6: k <= len vs1 ; :: thesis: vs1 . b1 = vs2 . b1
per cases ( k = len vs1 or k <> len vs1 ) ;
suppose k = len vs1 ; :: thesis: vs1 . b1 = vs2 . b1
then A7: k = (len p) + 1 by A1;
hence vs1 . k = the Target of G . (p . (len p)) by A1, A3
.= vs2 . k by A2, A3, A7 ;
:: thesis: verum
end;
suppose k <> len vs1 ; :: thesis: vs1 . b1 = vs2 . b1
then k < len vs1 by A6, XXREAL_0:1;
then k + 1 <= len vs1 by INT_1:7;
then k + 1 <= (len p) + 1 by A1;
then A8: k <= len p by XREAL_1:6;
hence vs1 . k = the Source of G . (p . k) by A1, A5
.= vs2 . k by A2, A5, A8 ;
:: thesis: verum
end;
end;
end;
len vs1 = (len p) + 1 by A1
.= len vs2 by A2 ;
hence vs1 = vs2 by A4, FINSEQ_1:14; :: thesis: verum