let G be _Graph; :: thesis: for P being Path of G holds dom ((P .vertexSeq()) | (P .length())) = Seg (P .length())
let P be Path of G; :: thesis: dom ((P .vertexSeq()) | (P .length())) = Seg (P .length())
A1: (P .length()) + 0 <= (P .length()) + 1 by XREAL_1:6;
thus dom ((P .vertexSeq()) | (P .length())) = dom ((P .vertexSeq()) | (Seg (P .length()))) by FINSEQ_1:def 15
.= (dom (P .vertexSeq())) /\ (Seg (P .length())) by RELAT_1:61
.= (Seg (len (P .vertexSeq()))) /\ (Seg (P .length())) by FINSEQ_1:def 3
.= (Seg ((P .length()) + 1)) /\ (Seg (P .length())) by GLIB_009:28
.= Seg (P .length()) by A1, FINSEQ_1:7 ; :: thesis: verum