W1 .vertices() c= dom (F _V)
by Def35;
then A1:
rng (W1 .vertexSeq()) c= dom (F _V)
by GLIB_001:def 16;
then reconsider p = (F _V) * (W1 .vertexSeq()) as FinSequence by FINSEQ_1:16;
rng p c= the_Vertices_of G2
by RELAT_1:def 19;
then reconsider p = p as FinSequence of the_Vertices_of G2 by FINSEQ_1:def 4;
W1 .edges() c= dom (F _E)
by Def35;
then A2:
rng (W1 .edgeSeq()) c= dom (F _E)
by GLIB_001:def 17;
then reconsider q = (F _E) * (W1 .edgeSeq()) as FinSequence by FINSEQ_1:16;
rng q c= the_Edges_of G2
by RELAT_1:def 19;
then reconsider q = q as FinSequence of the_Edges_of G2 by FINSEQ_1:def 4;
A3: 2 * (len p) =
2 * (len (W1 .vertexSeq()))
by A1, FINSEQ_2:29
.=
(len W1) + 1
by GLIB_001:def 14
.=
((2 * (len (W1 .edgeSeq()))) + 1) + 1
by GLIB_001:def 15
.=
((2 * (len q)) + 1) + 1
by A2, FINSEQ_2:29
.=
2 * ((len q) + 1)
;
for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G2
proof
let n be
Element of
NAT ;
( 1 <= n & n + 1 <= len p implies q . n Joins p . n,p . (n + 1),G2 )
assume A4:
( 1
<= n &
n + 1
<= len p )
;
q . n Joins p . n,p . (n + 1),G2
then A5:
n <= len q
by A3, XREAL_1:6;
n + 0 <= n + 1
by XREAL_1:6;
then A6:
n <= len p
by A4, XXREAL_0:2;
then A7:
n in dom p
by A4, FINSEQ_3:25;
A8:
1
+ 0 <= n + 1
by XREAL_1:7;
then A9:
n + 1
in dom p
by A4, FINSEQ_3:25;
n in dom q
by A4, A5, FINSEQ_3:25;
then A10:
(
n in dom (W1 .vertexSeq()) &
(W1 .vertexSeq()) . n in dom (F _V) &
n + 1
in dom (W1 .vertexSeq()) &
(W1 .vertexSeq()) . (n + 1) in dom (F _V) &
n in dom (W1 .edgeSeq()) &
(W1 .edgeSeq()) . n in dom (F _E) )
by A7, A9, FUNCT_1:11;
(
n <= len (W1 .edgeSeq()) &
n <= len (W1 .vertexSeq()) &
n + 1
<= len (W1 .vertexSeq()) )
by A1, A2, A4, A5, A6, FINSEQ_2:29;
then A11:
(
(W1 .edgeSeq()) . n = W1 . (2 * n) &
(W1 .vertexSeq()) . n = W1 . ((2 * n) - 1) &
(W1 .vertexSeq()) . (n + 1) = W1 . ((2 * (n + 1)) - 1) )
by A4, A8, GLIB_001:def 14, GLIB_001:def 15;
2
* 1
<= 2
* n
by A4, XREAL_1:64;
then
2
- 1
<= (2 * n) - 1
by XREAL_1:9;
then reconsider m =
(2 * n) - 1 as
Element of
NAT by INT_1:3;
2
* (n + 1) <= 2
* (len p)
by A4, XREAL_1:64;
then
(2 * n) + 2
<= ((2 * (len p)) - 2) + 2
;
then
m <= ((2 * (len p)) - 2) - 1
by XREAL_1:6, XREAL_1:9;
then
m <= ((2 * (len (W1 .vertexSeq()))) - 2) - 1
by A1, FINSEQ_2:29;
then A12:
m <= (((len W1) + 1) - 2) - 1
by GLIB_001:def 14;
(len W1) - 2
< (len W1) - 0
by XREAL_1:15;
then
m < len W1
by A12, XXREAL_0:2;
then A13:
W1 . (m + 1) Joins W1 . m,
W1 . (m + 2),
G1
by GLIB_001:def 3;
(F _E) . ((W1 .edgeSeq()) . n) Joins (F _V) . ((W1 .vertexSeq()) . n),
(F _V) . ((W1 .vertexSeq()) . (n + 1)),
G2
by A10, A11, A13, Th4;
then
q . n Joins (F _V) . ((W1 .vertexSeq()) . n),
(F _V) . ((W1 .vertexSeq()) . (n + 1)),
G2
by A10, FUNCT_1:13;
then
q . n Joins p . n,
(F _V) . ((W1 .vertexSeq()) . (n + 1)),
G2
by A10, FUNCT_1:13;
hence
q . n Joins p . n,
p . (n + 1),
G2
by A10, FUNCT_1:13;
verum
end;
then consider W2 being Walk of G2 such that
A14:
( W2 .vertexSeq() = p & W2 .edgeSeq() = q )
by A3, GLIB_009:27;
take
W2
; ( (F _V) * (W1 .vertexSeq()) = W2 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = W2 .edgeSeq() )
thus
( (F _V) * (W1 .vertexSeq()) = W2 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = W2 .edgeSeq() )
by A14; verum