let G be _Graph; :: thesis: for p being FinSequence of the_Vertices_of G
for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) holds
ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )
let p be FinSequence of the_Vertices_of G; :: thesis: for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) holds
ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )
let q be FinSequence of the_Edges_of G; :: thesis: ( len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) implies ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q ) )
assume that
A1: len p = 1 + (len q) and
A2: for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ; :: thesis: ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )
defpred S₁[ object , object ] means ex m being Nat st
( m = $1 & ( m is odd implies $2 = p . ((m + 1) div 2) ) & ( m is even implies $2 = q . (m div 2) ) );
A3: for k being Nat st k in Seg ((len p) + (len q)) holds
ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg ((len p) + (len q)) implies ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S₁[k,x] )
assume k in Seg ((len p) + (len q)) ; :: thesis: ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S₁[k,x]
then A4: ( 1 <= k & k <= (len p) + (len q) ) by FINSEQ_1:1;

per cases ( k is odd or k is even ) ;

suppose A5: k is odd ; :: thesis: ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S₁[k,x]

k + 0 <= ((len p) + (len q)) + 1 by A4, XREAL_1:7;
then A6: k <= 2 * (len p) by A1;
1 + 1 <= k + 1 by A5, ABIAN:12, XREAL_1:6;
then 1 <= (k + 1) div 2 by NAT_2:13;
then (k + 1) div 2 in dom p by A6, FINSEQ_3:25, NAT_2:25;
then p . ((k + 1) div 2) in rng p by FUNCT_1:3;
then reconsider x = p . ((k + 1) div 2) as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;
take x ; :: thesis: S₁[k,x]
take k ; :: thesis: ( k = k & ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus k = k ; :: thesis: ( ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus ( k is odd implies x = p . ((k + 1) div 2) ) ; :: thesis: ( k is even implies x = q . (k div 2) )
thus ( k is even implies x = q . (k div 2) ) by A5; :: thesis: verum

end;

suppose A7: k is even ; :: thesis: ex x being Element of (the_Vertices_of G) \/ (the_Edges_of G) st S₁[k,x]

A8: k - 1 = k -' 1 by A4, XREAL_1:233;
reconsider r = k - 1 as Nat by A8;
r <= (1 + (2 * (len q))) - 1 by A1, A4, XREAL_1:9;
then A9: (r + 1) div 2 <= len q by NAT_2:25;
2 <= k

proof

assume A10: k < 2 ; :: thesis: contradiction
consider s being Nat such that
A11: k = 2 * s by A7, ABIAN:def 2;
(2 * s) / 2 < (1 * 2) / 2 by A10, A11, XREAL_1:81;
then s = 0 by NAT_1:14;
hence contradiction by A4, A11; :: thesis: verum

end;

then 1 <= k div 2 by NAT_2:13;
then k div 2 in dom q by A9, FINSEQ_3:25;
then q . (k div 2) in rng q by FUNCT_1:3;
then reconsider x = q . (k div 2) as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;
take x ; :: thesis: S₁[k,x]
take k ; :: thesis: ( k = k & ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus k = k ; :: thesis: ( ( k is odd implies x = p . ((k + 1) div 2) ) & ( k is even implies x = q . (k div 2) ) )
thus ( k is odd implies x = p . ((k + 1) div 2) ) by A7; :: thesis: ( k is even implies x = q . (k div 2) )
thus ( k is even implies x = q . (k div 2) ) ; :: thesis: verum

end;

end;

end;

consider W being FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) such that
A12: dom W = Seg ((len p) + (len q)) and
A13: for k being Nat st k in Seg ((len p) + (len q)) holds
S₁[k,W . k] from FINSEQ_1:sch 5(A3);
A14: len W = (2 * (len q)) + 1 by A1, A12, FINSEQ_1:def 3;
A15: W . 1 in the_Vertices_of G

proof

1 + 0 <= 1 + ((len q) + (len q)) by XREAL_1:7;
then consider m being Nat such that
A16: m = 1 and
A17: ( m is odd implies W . 1 = p . ((m + 1) div 2) ) and
( m is even implies W . 1 = q . (m div 2) ) by A1, A13, FINSEQ_1:1;
A18: W . 1 = p . ((m + 1) div 2) by A16, A17
.= p . 1 by A16, NAT_2:3 ;
1 + 0 <= 1 + (len q) by XREAL_1:7;
then 1 in dom p by A1, FINSEQ_3:25;
then p . 1 in rng p by FUNCT_1:3;
hence W . 1 in the_Vertices_of G by A18; :: thesis: verum

end;

for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G

proof

let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G )
assume A19: n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G
set m = (n + 1) div 2;
1 + 1 <= n + 1 by ABIAN:12, XREAL_1:6;
then A20: 1 <= (n + 1) div 2 by NAT_2:13;
reconsider m = (n + 1) div 2 as Nat ;
A21: ( 1 + 0 <= n + 1 & 1 + 0 <= n + 2 ) by XREAL_1:7;
A22: n + 2 <= len W by A14, A19, GLIB_001:1;
( n + 0 <= n + 2 & n + 1 <= n + 2 ) by XREAL_1:7;
then ( n <= len W & n + 1 <= len W ) by A22, XXREAL_0:2;
then A23: ( n in dom W & n + 1 in dom W & n + 2 in dom W ) by A21, A22, ABIAN:12, FINSEQ_3:25;
A24: ((n + 2) + 1) div 2 = ((n + 1) + 2) div 2
.= m + 1 by NAT_2:14 ;
consider n0 being Nat such that
A25: n0 = n and
A26: ( n0 is odd implies W . n = p . ((n0 + 1) div 2) ) and
( n0 is even implies W . n = q . (n0 div 2) ) by A12, A13, A23;
consider n1 being Nat such that
A27: n1 = n + 1 and
( n1 is odd implies W . (n + 1) = p . ((n1 + 1) div 2) ) and
A28: ( n1 is even implies W . (n + 1) = q . (n1 div 2) ) by A12, A13, A23;
consider n2 being Nat such that
A29: n2 = n + 2 and
A30: ( n2 is odd implies W . (n + 2) = p . ((n2 + 1) div 2) ) and
( n2 is even implies W . (n + 2) = q . (n2 div 2) ) by A12, A13, A23;
A31: W . n = p . m by A25, A26;
A32: W . (n + 1) = q . m by A27, A28;
A33: W . (n + 2) = p . (m + 1) by A24, A29, A30;
A34: n + 2 <= ((len p) - 1) + (len p) by A1, A12, A22, FINSEQ_1:def 3;
(2 * (len p)) - 1 <= (2 * (len p)) - 0 by XREAL_1:13;
then n + 2 <= 2 * (len p) by A34, XXREAL_0:2;
then ((n + 2) + 1) div 2 <= len p by NAT_2:25;
then ((n + 1) + 2) div 2 <= len p ;
then m + 1 <= len p by NAT_2:14;
hence W . (n + 1) Joins W . n,W . (n + 2),G by A2, A20, A31, A32, A33; :: thesis: verum

end;

then reconsider W = W as Walk of G by A14, A15, GLIB_001:def 3;
take W ; :: thesis: ( W .vertexSeq() = p & W .edgeSeq() = q )
A35: 2 * (len (W .vertexSeq())) = (len W) + 1 by GLIB_001:def 14
.= ((len p) + (len q)) + 1 by A12, FINSEQ_1:def 3
.= 2 * (len p) by A1 ;
for k being Nat st 1 <= k & k <= len p holds
p . k = (W .vertexSeq()) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len p implies p . k = (W .vertexSeq()) . k )
assume A36: ( 1 <= k & k <= len p ) ; :: thesis: p . k = (W .vertexSeq()) . k
2 * k <= 2 * (len p) by A36, XREAL_1:64;
then A37: (2 * k) - 1 <= (((len p) + 1) + (len q)) - 1 by A1, XREAL_1:9;
2 * 1 <= 2 * k by A36, XREAL_1:64;
then A38: (1 + 1) - 1 <= (2 * k) - 1 by XREAL_1:9;
then (2 * k) - 1 in NAT by INT_1:3;
then consider m being Nat such that
A39: m = (2 * k) - 1 and
A40: ( m is odd implies W . ((2 * k) - 1) = p . ((m + 1) div 2) ) and
( m is even implies W . ((2 * k) - 1) = q . (m div 2) ) by A13, A37, A38, FINSEQ_1:1;
W . ((2 * k) - 1) = p . k by A39, A40, NAT_D:18;
hence p . k = (W .vertexSeq()) . k by A35, A36, GLIB_001:def 14; :: thesis: verum

end;

hence W .vertexSeq() = p by A35, FINSEQ_1:def 18; :: thesis: W .edgeSeq() = q
A41: (2 * (len (W .edgeSeq()))) + 1 = (2 * (len q)) + 1 by A14, GLIB_001:def 15;
for k being Nat st 1 <= k & k <= len q holds
q . k = (W .edgeSeq()) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len q implies q . k = (W .edgeSeq()) . k )
assume A42: ( 1 <= k & k <= len q ) ; :: thesis: q . k = (W .edgeSeq()) . k
then A43: (W .edgeSeq()) . k = W . (2 * k) by A41, GLIB_001:def 15;
2 * k <= 2 * (len q) by A42, XREAL_1:64;
then A44: (2 * k) + 0 <= ((len q) + (len q)) + 1 by XREAL_1:7;
1 * 1 <= 2 * k by A42, XREAL_1:66;
then consider m being Nat such that
A45: m = 2 * k and
( m is odd implies W . (2 * k) = p . ((m + 1) div 2) ) and
A46: ( m is even implies W . (2 * k) = q . (m div 2) ) by A1, A13, A44, FINSEQ_1:1;
thus q . k = (W .edgeSeq()) . k by A43, A45, A46, NAT_D:18; :: thesis: verum

end;

hence W .edgeSeq() = q by A41, FINSEQ_1:def 18; :: thesis: verum