theorem Th9: :: GRAPH_3:9

for G being Graph
for p being Path of G
for m being Nat st m + 1 in dom p holds
( len ((((m + 1),(len p)) -cut p) ^ ((1,m) -cut p)) = len p & rng ((((m + 1),(len p)) -cut p) ^ ((1,m) -cut p)) = rng p & ((((m + 1),(len p)) -cut p) ^ ((1,m) -cut p)) . 1 = p . (m + 1) )