let G be Graph; :: thesis: for p being Path of G
for n, m being Element of NAT st 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m holds
p . n <> p . m
let p be Path of G; :: thesis: for n, m being Element of NAT st 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m holds
p . n <> p . m
let n, m be Element of NAT ; :: thesis: ( 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m implies p . n <> p . m )
assume ( 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m ) ; :: thesis: p . n <> p . m
then ( n in dom p & m in dom p & n <> m ) by FINSEQ_3:27;
hence p . n <> p . m by FUNCT_1:def 8; :: thesis: verum