let G be Graph; :: thesis: for m being 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 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, FINSEQ_6:133;
hence (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G by A2, FINSEQ_1:34; :: 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:34
.= p by A3, FINSEQ_6:133 ;
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 FINSEQ_6:def 4;
(1,m) -cut p = {} by A4, FINSEQ_6:def 4;
then (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) = {} by A5, FINSEQ_1:34;
hence (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G by Th7, 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 Th5;
consider vs being FinSequence of the carrier of G such that
A8: vs is_vertex_seq_of p by GRAPH_2:33;
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;
A11: vs2 is_vertex_seq_of r2 by A7, A9, A8, GRAPH_2:42;
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, FINSEQ_6:def 4;
then A14: 1 < len vs1 by A6, NAT_1:13;
A15: vs1 is_vertex_seq_of r1 by A6, A8, GRAPH_2:42;
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:6;
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, FINSEQ_6:138;
then reconsider r = r2 ^ r1 as Chain of G by A17, A15, A11, GRAPH_2:43;
A19: vs9 is_vertex_seq_of r by A17, A15, A11, A18, GRAPH_2:44;
p = r1 ^ r2 by A6, FINSEQ_6:135;
then rng r1 misses rng r2 by FINSEQ_3:91;
then reconsider r = r as Path of G by A17, A15, A11, A18, Th6;
( vs1 . (len vs1) = vs . (m + 1) & vs2 . 1 = vs . (m + 1) ) by A7, A12, FINSEQ_6:138;
then vs9 . 1 = vs1 . (len vs1) by A16, FINSEQ_6:140
.= vs9 . (len vs9) by A14, FINSEQ_6:142 ;
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;