let G be Graph; :: thesis: for m being Element of NAT
for p being cyclic Path of G holds ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G
let m be Element of NAT ; :: thesis: for p being cyclic Path of G holds ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G
let p be cyclic Path of G; :: thesis: ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G

per cases ( m = 0 or ( 1 <= m & len p = m ) or ( 1 <= m & len p < m ) or ( 1 <= m & m < len p ) ) by NAT_1:14, XXREAL_0:1;

suppose A1: m = 0 ; :: thesis: ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G

0 <= len p ;
then (len (1,m -cut p)) + 1 = 0 + 1 by A1, Lm1;
then A2: 1,m -cut p = {} ;
(m + 1),(len p) -cut p = p by A1, GRAPH_2:7;
hence ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G by A2, FINSEQ_1:47; :: thesis: verum

end;

suppose A3: ( 1 <= m & len p = m ) ; :: thesis: ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G

1 <= m + 1 by NAT_1:12;
then (len ((m + 1),(len p) -cut p)) + (m + 1) = (len p) + 1 by A3, Lm1;
then (m + 1),(len p) -cut p = {} by A3;
then ((m + 1),(len p) -cut p) ^ (1,m -cut p) = 1,m -cut p by FINSEQ_1:47
.= p by A3, GRAPH_2:7 ;
hence ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G ; :: thesis: verum

end;

suppose A4: ( 1 <= m & len p < m ) ; :: thesis: ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G

m <= m + 1 by NAT_1:11;
then len p < m + 1 by A4, XXREAL_0:2;
then A5: (m + 1),(len p) -cut p = {} by GRAPH_2:def 1;
1,m -cut p = {} by A4, GRAPH_2:def 1;
then ((m + 1),(len p) -cut p) ^ (1,m -cut p) = {} by A5, FINSEQ_1:47;
hence ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G by Th12, GRAPH_1:14; :: thesis: verum

end;

suppose A6: ( 1 <= m & m < len p ) ; :: thesis: ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G

set n1 = m;
set n = m + 1;
A7: 1 <= m + 1 by A6, NAT_1:13;
reconsider r1 = 1,m -cut p, r2 = (m + 1),(len p) -cut p as Path of G by Th8;
consider vs being FinSequence of the carrier of G such that
A8: vs is_vertex_seq_of p by GRAPH_2:36;
reconsider vs1 = 1,(m + 1) -cut vs, vs2 = (m + 1),(len vs) -cut vs as FinSequence of the carrier of G ;
A9: m + 1 <= len p by A6, NAT_1:13;
A10: len vs = (len p) + 1 by A8, GRAPH_2:def 7;
then A11: vs2 is_vertex_seq_of r2 by A7, A9, A8, GRAPH_2:45;
len p <= (len p) + 1 by NAT_1:11;
then A12: m + 1 <= len vs by A9, A10, XXREAL_0:2;
then A13: m + 1 < (len vs) + 1 by NAT_1:13;
(len vs1) + 1 = (m + 1) + 1 by A7, A12, GRAPH_2:def 1;
then A14: 1 < len vs1 by A6, NAT_1:13;
A15: vs1 is_vertex_seq_of r1 by A6, A8, GRAPH_2:45;
len vs <= (len vs) + 1 by NAT_1:11;
then m + 1 <= (len vs) + 1 by A12, XXREAL_0:2;
then (len vs2) + (m + 1) = (len vs) + 1 by A7, Lm1;
then 1 + (m + 1) <= (len vs2) + (m + 1) by A13, NAT_1:13;
then A16: 1 <= len vs2 by XREAL_1:8;
reconsider vs9 = vs2 ^' vs1 as FinSequence of the carrier of G ;
set r = r2 ^ r1;
A17: vs . (len vs) = vs . 1 by A8, MSSCYC_1:6;
A18: ( vs1 . 1 = vs . 1 & vs2 . (len vs2) = vs . (len vs) ) by A7, A12, GRAPH_2:12;
then reconsider r = r2 ^ r1 as Chain of G by A17, A15, A11, GRAPH_2:46;
A19: vs9 is_vertex_seq_of r by A17, A15, A11, A18, GRAPH_2:47;
p = r1 ^ r2 by A6, GRAPH_2:9;
then rng r1 misses rng r2 by FINSEQ_3:98;
then reconsider r = r as Path of G by A17, A15, A11, A18, Th9;
( vs1 . (len vs1) = vs . (m + 1) & vs2 . 1 = vs . (m + 1) ) by A7, A12, GRAPH_2:12;
then vs9 . 1 = vs1 . (len vs1) by A16, GRAPH_2:14
.= vs9 . (len vs9) by A14, GRAPH_2:16 ;
then r is cyclic Path of G by A19, MSSCYC_1:def 2;
hence ((m + 1),(len p) -cut p) ^ (1,m -cut p) is cyclic Path of G ; :: thesis: verum

end;

end;