let IT1, IT2 be EdgeSeq of G; :: thesis: ( len W = (2 * (len IT1)) + 1 & ( for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = W . (2 * n) ) & len W = (2 * (len IT2)) + 1 & ( for n being Nat st 1 <= n & n <= len IT2 holds
IT2 . n = W . (2 * n) ) implies IT1 = IT2 )
assume that
A20: len W = (2 * (len IT1)) + 1 and
A21: for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = W . (2 * n) and
A22: len W = (2 * (len IT2)) + 1 and
A23: for n being Nat st 1 <= n & n <= len IT2 holds
IT2 . n = W . (2 * n) ; :: thesis: IT1 = IT2

A24: now :: thesis: for n being Nat st n in dom IT1 holds
IT1 . n = IT2 . n

let n be Nat; :: thesis: ( n in dom IT1 implies IT1 . n = IT2 . n )
assume A25: n in dom IT1 ; :: thesis: IT1 . n = IT2 . n
then A26: 1 <= n by FINSEQ_3:25;
A27: n <= len IT2 by A20, A22, A25, FINSEQ_3:25;
n <= len IT1 by A25, FINSEQ_3:25;
hence IT1 . n = W . (2 * n) by A21, A26
.= IT2 . n by A23, A26, A27 ;
:: thesis: verum

end;

dom IT1 = Seg (len IT2) by A20, A22, FINSEQ_1:def 3
.= dom IT2 by FINSEQ_1:def 3 ;
hence IT1 = IT2 by A24, FINSEQ_1:13; :: thesis: verum