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 A1: ( p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1 ) ; :: thesis: vs1 = vs2
then A2: len vs1 = (len p) + 1 by Def19
.= len vs2 by A1, Def19 ;

now

let k be Nat; :: thesis: ( 1 <= k & k <= len vs1 implies vs1 . b₁ = vs2 . b₁ )
assume A3: ( 1 <= k & k <= len vs1 ) ; :: thesis: vs1 . b₁ = vs2 . b₁

per cases ( k = len vs1 or k <> len vs1 ) ;

suppose k = len vs1 ; :: thesis: vs1 . b₁ = vs2 . b₁

then A4: k = (len p) + 1 by A1, Def19;
hence vs1 . k = the Target of G . (p . (len p)) by A1, Def19
.= vs2 . k by A1, A4, Def19 ;
:: thesis: verum

end;

suppose k <> len vs1 ; :: thesis: vs1 . b₁ = vs2 . b₁

then k < len vs1 by A3, XXREAL_0:1;
then k + 1 <= len vs1 by INT_1:20;
then k + 1 <= (len p) + 1 by A1, Def19;
then A5: k <= len p by XREAL_1:8;
hence vs1 . k = the Source of G . (p . k) by A1, A3, Def19
.= vs2 . k by A1, A3, A5, Def19 ;
:: thesis: verum

end;

end;

end;

hence vs1 = vs2 by A2, FINSEQ_1:18; :: thesis: verum