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

.= dom IT2 by FINSEQ_1:def 3 ;

hence IT1 = IT2 by A24, FINSEQ_1:13; :: thesis: verum

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

dom IT1 =
Seg (len IT2)
by A20, A22, FINSEQ_1:def 3
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;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

.= dom IT2 by FINSEQ_1:def 3 ;

hence IT1 = IT2 by A24, FINSEQ_1:13; :: thesis: verum