let n be non zero Nat; :: thesis:
let P1, P2 be n -vertex Path-like _Graph; :: thesis:
consider P7 being vertex-distinct Path of P1 such that
A1: ( P7 .vertices() = the_Vertices_of P1 & P7 .edges() = the_Edges_of P1 ) and
( Endvertices P1 = {(P7 .first()),(P7 .last())} iff not P1 is _trivial ) and
( P7 is trivial iff P1 is _trivial ) and
( P7 is closed iff P1 is _trivial ) and
P7 is minlength by Th31;
consider P8 being vertex-distinct Path of P2 such that
A4: ( P8 .vertices() = the_Vertices_of P2 & P8 .edges() = the_Edges_of P2 ) and
( Endvertices P2 = {(P8 .first()),(P8 .last())} iff not P2 is _trivial ) and
( P8 is trivial iff P2 is _trivial ) and
( P8 is closed iff P2 is _trivial ) and
P8 is minlength by Th31;
set p1 = P7 .vertexSeq() ;
set p2 = P8 .vertexSeq() ;
( P1 .order() = n & P2 .order() = n ) by GLIB_013:def 3;
then A7: card (the_Vertices_of P1) = card (the_Vertices_of P2) ;
set f = (P8 .vertexSeq()) * ((P7 .vertexSeq()) ");
A8: card (P8 .vertexSeq()) = card (dom (P8 .vertexSeq())) by CARD_1:62
.= card (the_Vertices_of P2) by A4, CARD_1:70
.= card (dom (P7 .vertexSeq())) by A1, A7, CARD_1:70
.= card (P7 .vertexSeq()) by CARD_1:62 ;
A9: dom (P8 .vertexSeq()) = Seg (len (P8 .vertexSeq())) by FINSEQ_1:def 3
.= dom (P7 .vertexSeq()) by A8, FINSEQ_1:def 3 ;
then A10: dom (P8 .vertexSeq()) = rng ((P7 .vertexSeq()) ") by FUNCT_1:33;
then A11: dom ((P8 .vertexSeq()) * ((P7 .vertexSeq()) ")) = dom ((P7 .vertexSeq()) ") by RELAT_1:27
.= the_Vertices_of P1 by A1, FUNCT_1:33 ;
A12: len (P7 .vertexSeq()) = len (P8 .vertexSeq()) by A9, FINSEQ_3:29;
A13: rng ((P8 .vertexSeq()) * ((P7 .vertexSeq()) ")) = the_Vertices_of P2 by A4, A10, RELAT_1:28;
then reconsider f = (P8 .vertexSeq()) * ((P7 .vertexSeq()) ") as Function of (the_Vertices_of P1),(the_Vertices_of P2) by A11, FUNCT_2:1;

now :: thesis:

let v, w, e be object ; :: thesis:
assume A14: ( v in dom f & w in dom f & e Joins v,w,P1 ) ; :: thesis:
then A15: v in P7 .vertices() by A1;
A16: w in P7 .vertices() by A1, A14;
consider n being odd Element of NAT such that
A17: ( n <= len P7 & P7 . n = v ) by A15, GLIB_001:87;
consider m being odd Element of NAT such that
A18: ( m <= len P7 & P7 . m = w ) by A16, GLIB_001:87;
set i = (n + 1) div 2;
set j = (m + 1) div 2;
A19: ( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (P7 .vertexSeq()) ) by A17, GLIB_001:68;
then A20: (P7 .vertexSeq()) . ((n + 1) div 2) = v by A17, GLIB_001:def 14;
A21: (n + 1) div 2 in dom (P7 .vertexSeq()) by A19, FINSEQ_3:25;
A22: f . v = (P8 .vertexSeq()) . (((P7 .vertexSeq()) ") . v) by A14, FUNCT_1:12
.= (P8 .vertexSeq()) . ((n + 1) div 2) by A20, A21, FUNCT_1:34
.= P8 . n by A12, A19, GLIB_001:def 14 ;
A23: ( (2 * ((m + 1) div 2)) - 1 = m & 1 <= (m + 1) div 2 & (m + 1) div 2 <= len (P7 .vertexSeq()) ) by A18, GLIB_001:68;
then A24: (P7 .vertexSeq()) . ((m + 1) div 2) = w by A18, GLIB_001:def 14;
A25: (m + 1) div 2 in dom (P7 .vertexSeq()) by A23, FINSEQ_3:25;
A26: f . w = (P8 .vertexSeq()) . (((P7 .vertexSeq()) ") . w) by A14, FUNCT_1:12
.= (P8 .vertexSeq()) . ((m + 1) div 2) by A24, A25, FUNCT_1:34
.= P8 . m by A12, A23, GLIB_001:def 14 ;
( 2 * (len (P7 .vertexSeq())) = (len P7) + 1 & 2 * (len (P8 .vertexSeq())) = (len P8) + 1 ) by GLIB_001:def 14;
then A27: len P7 = len P8 by A12;
e in P7 .edges() by A1, A14, GLIB_000:def 13;
then consider k being odd Element of NAT such that
A28: ( k < len P7 & P7 . (k + 1) = e ) by GLIB_001:100;
A29: ( k <= len P7 & k + 2 <= len P7 ) by A28, CHORD:4;
e Joins P7 . k,P7 . (k + 2),P1 by A28, GLIB_001:def 3;

per cases by A17, A18, A14, GLIB_000:15;

suppose ( P7 . k = P7 . n & P7 . (k + 2) = P7 . m ) ; :: thesis:

then ( k = n & k + 2 = m ) by A17, A18, A29, GLIB_001:def 29;
then A30: n + 2 = m ;
A31: n < len P8

proof

assume n >= len P8 ; :: thesis:
then A32: n + 2 >= (len P7) + 2 by A27, XREAL_1:6;
m + 2 <= (len P7) + 2 by A18, XREAL_1:6;
then m + 0 >= m + 2 by A30, A32, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis:

end;

reconsider e9 = P8 . (n + 1) as object ;
take e9 = e9; :: thesis:
e9 Joins f . v,P8 . (n + 2),P2 by A22, A31, GLIB_001:def 3;
hence e9 Joins f . v,f . w,P2 by A30, A26; :: thesis:

end;

suppose ( P7 . k = P7 . m & P7 . (k + 2) = P7 . n ) ; :: thesis:

then ( k = m & k + 2 = n ) by A17, A18, A29, GLIB_001:def 29;
then A33: m + 2 = n ;
A34: m < len P8

proof

assume m >= len P8 ; :: thesis:
then A35: m + 2 >= (len P7) + 2 by A27, XREAL_1:6;
n + 2 <= (len P7) + 2 by A17, XREAL_1:6;
then n + 0 >= n + 2 by A33, A35, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis:

end;

reconsider e9 = P8 . (m + 1) as object ;
take e9 = e9; :: thesis:
e9 Joins P8 . m,P8 . (m + 2),P2 by A34, GLIB_001:def 3;
hence e9 Joins f . v,f . w,P2 by A26, A33, A22, GLIB_000:14; :: thesis:

end;

then reconsider f = f as PVertexMapping of P1,P2 by GLIB_011:1;

now :: thesis:

per cases by A39, A40, A36, GLIB_000:15;

suppose ( P8 . k = P8 . n & P8 . (k + 2) = P8 . m ) ; :: thesis:

then ( k = n & k + 2 = m ) by A39, A40, A51, GLIB_001:def 29;
then A52: n + 2 = m ;
A53: n < len P7

proof

assume n >= len P7 ; :: thesis:
then A54: n + 2 >= (len P8) + 2 by A49, XREAL_1:6;
m + 2 <= (len P8) + 2 by A40, XREAL_1:6;
then m + 0 >= m + 2 by A52, A54, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis:

end;

reconsider e = P7 . (n + 1) as object ;
take e = e; :: thesis:
e Joins P7 . n,P7 . (n + 2),P1 by A53, GLIB_001:def 3;
hence e Joins v,w,P1 by A44, A52, A48; :: thesis:

end;

suppose ( P8 . k = P8 . m & P8 . (k + 2) = P8 . n ) ; :: thesis:

then ( k = m & k + 2 = n ) by A39, A40, A51, GLIB_001:def 29;
then A55: m + 2 = n ;
A56: m < len P7

proof

assume m >= len P7 ; :: thesis:
then A57: m + 2 >= (len P8) + 2 by A49, XREAL_1:6;
n + 2 <= (len P8) + 2 by A39, XREAL_1:6;
then n + 0 >= n + 2 by A55, A57, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis:

end;

reconsider e = P7 . (m + 1) as object ;
take e = e; :: thesis:
e Joins P7 . m,P7 . (m + 2),P1 by A56, GLIB_001:def 3;
hence e Joins v,w,P1 by A48, A55, A44, GLIB_000:14; :: thesis:

end;

then A58: f is continuous by GLIB_011:2;
( f is total & f is onto ) by A13, FUNCT_2:def 3;
hence P2 is P1 -isomorphic by A58, GLIB_011:49; :: thesis: