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

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

end;

end;