let G be Graph; :: thesis: for p being Path of G
for n, m being 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 Nat st 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m holds
p . n <> p . m
let n, m be Nat; :: thesis: ( 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m implies p . n <> p . m )
assume that
A1: ( 1 <= n & n <= len p & 1 <= m & m <= len p ) and
A2: n <> m ; :: thesis: p . n <> p . m
( n in dom p & m in dom p ) by A1, FINSEQ_3:25;
hence p . n <> p . m by A2, FUNCT_1:def 4; :: thesis: verum