set f = (P .vertexSeq()) | (P .length());

now :: thesis: for x1, x2 being object st x1 in dom ((P .vertexSeq()) | (P .length())) & x2 in dom ((P .vertexSeq()) | (P .length())) & ((P .vertexSeq()) | (P .length())) . x1 = ((P .vertexSeq()) | (P .length())) . x2 holds
not x1 <> x2

let x1, x2 be object ; :: thesis: ( x1 in dom ((P .vertexSeq()) | (P .length())) & x2 in dom ((P .vertexSeq()) | (P .length())) & ((P .vertexSeq()) | (P .length())) . x1 = ((P .vertexSeq()) | (P .length())) . x2 implies not x1 <> x2 )
A1: dom ((P .vertexSeq()) | (P .length())) = Seg (P .length()) by Lm1;
assume A2: ( x1 in dom ((P .vertexSeq()) | (P .length())) & x2 in dom ((P .vertexSeq()) | (P .length())) & ((P .vertexSeq()) | (P .length())) . x1 = ((P .vertexSeq()) | (P .length())) . x2 ) ; :: thesis: not x1 <> x2
then reconsider n1 = x1 as Nat ;
A3: ( 1 <= n1 & n1 <= P .length() ) by A1, A2, FINSEQ_1:1;
reconsider n2 = x2 as Nat by A2;
A4: ( 1 <= n2 & n2 <= P .length() ) by A1, A2, FINSEQ_1:1;
(P .length()) + 0 <= (P .length()) + 1 by XREAL_1:6;
then (P .length()) + 0 <= len (P .vertexSeq()) by GLIB_009:28;
then A5: ( n1 <= len (P .vertexSeq()) & n2 <= len (P .vertexSeq()) ) by A3, A4, XXREAL_0:2;
A6: ((P .vertexSeq()) | (P .length())) . n1 = ((P .vertexSeq()) | (Seg (P .length()))) . n1 by FINSEQ_1:def 16
.= (P .vertexSeq()) . n1 by A1, A2, FUNCT_1:49
.= P . ((2 * n1) - 1) by A3, A5, GLIB_001:def 14 ;
((P .vertexSeq()) | (P .length())) . n2 = ((P .vertexSeq()) | (Seg (P .length()))) . n2 by FINSEQ_1:def 16
.= (P .vertexSeq()) . n2 by A1, A2, FUNCT_1:49
.= P . ((2 * n2) - 1) by A4, A5, GLIB_001:def 14 ;
then A7: P . ((2 * n1) - 1) = P . ((2 * n2) - 1) by A2, A6;
( 2 * 1 <= 2 * n1 & 2 * 1 <= 2 * n2 ) by A3, A4, XREAL_1:64;
then ( 2 - 1 <= (2 * n1) - 1 & 2 - 1 <= (2 * n2) - 1 ) by XREAL_1:9;
then reconsider m1 = (2 * n1) - 1, m2 = (2 * n2) - 1 as Element of NAT by INT_1:3;
A8: ( 2 * n1 <= 2 * (P .length()) & 2 * n2 <= 2 * (P .length()) ) by A3, A4, XREAL_1:64;
(2 * (P .length())) + 0 <= (2 * (P .length())) + 2 by XREAL_1:6;
then ( 2 * n1 <= (2 * (P .length())) + 2 & 2 * n2 <= (2 * (P .length())) + 2 ) by A8, XXREAL_0:2;
then ( m1 <= ((2 * (P .length())) + 2) - 1 & m2 <= ((2 * (P .length())) + 2) - 1 ) by XREAL_1:9;
then ( m1 <= (2 * (P .length())) + 1 & m2 <= (2 * (P .length())) + 1 ) ;
then A9: ( m1 <= len P & m2 <= len P ) by GLIB_001:112;
assume x1 <> x2 ; :: thesis: contradiction

per cases then ( n1 < n2 or n2 < n1 ) by XXREAL_0:1;

suppose n1 < n2 ; :: thesis: contradiction

then 2 * n1 < 2 * n2 by XREAL_1:68;
then ( m1 < m2 & m2 <= len P ) by A9, XREAL_1:9;
then m2 = len P by A7, GLIB_001:def 28
.= (2 * (P .length())) + 1 by GLIB_001:112 ;
then (2 * (P .length())) + 2 <= (2 * (P .length())) + 0 by A8;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

then 2 * n2 < 2 * n1 by XREAL_1:68;
then ( m2 < m1 & m1 <= len P ) by A9, XREAL_1:9;
then m1 = len P by A7, GLIB_001:def 28
.= (2 * (P .length())) + 1 by GLIB_001:112 ;
then (2 * (P .length())) + 2 <= (2 * (P .length())) + 0 by A8;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

end;

end;

hence (P .vertexSeq()) | (P .length()) is one-to-one by FUNCT_1:def 4; :: thesis: verum