set v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2));
A3: not (G -VSet (rng c1)) /\ (G -VSet (rng c2)) is empty by A1;
then A4: the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) in (G -VSet (rng c1)) /\ (G -VSet (rng c2)) ;
A5: the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) in G -VSet (rng c1) by A3, XBOOLE_0:def 4;
A6: the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) in G -VSet (rng c2) by A3, XBOOLE_0:def 4;
reconsider v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) as Vertex of G by A4;
reconsider Rotated2 = { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c2 & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } as non empty Subset of (G -CycleSet) by A6, Th52;
set r2 = Rotate (c2,v);
Rotate (c2,v) = the Element of Rotated2 by A6, Def9;
then Rotate (c2,v) in Rotated2 ;
then consider c99 being Element of G -CycleSet such that
A7: Rotate (c2,v) = c99 and
A8: rng c99 = rng c2 and
A9: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c99 & vs . 1 = v ) ;
consider vs2 being FinSequence of the carrier of G such that
A10: vs2 is_vertex_seq_of c99 and
A11: vs2 . 1 = v by A9;
reconsider c92 = c99 as cyclic Path of G by Def8;
A12: Rotate (c2,v) = c92 by A7;
not rng c2 is empty by A6, Th16;
then not c99 is empty by A8;
then 0 + 1 < (len c99) + 1 by XREAL_1:6;
then A13: 1 < len vs2 by A10;
A14: vs2 is_vertex_seq_of c92 by A10;
reconsider Rotated1 = { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c1 & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } as non empty Subset of (G -CycleSet) by A5, Th52;
set r1 = Rotate (c1,v);
Rotate (c1,v) = the Element of Rotated1 by A5, Def9;
then Rotate (c1,v) in Rotated1 ;
then consider c9 being Element of G -CycleSet such that
A15: Rotate (c1,v) = c9 and
A16: rng c9 = rng c1 and
A17: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ;
reconsider c91 = c9 as cyclic Path of G by Def8;
consider vs1 being FinSequence of the carrier of G such that
A18: vs1 is_vertex_seq_of c9 and
A19: vs1 . 1 = v by A17;
vs1 is_vertex_seq_of c91 by A18;
then A20: vs1 . 1 = vs1 . (len vs1) by MSSCYC_1:6;
set vs12 = vs1 ^' vs2;
len vs1 = (len c9) + 1 by A18;
then 1 <= len vs1 by NAT_1:11;
then A21: (vs1 ^' vs2) . 1 = vs1 . 1 by FINSEQ_6:140
.= vs2 . (len vs2) by A19, A11, A14, MSSCYC_1:6
.= (vs1 ^' vs2) . (len (vs1 ^' vs2)) by A13, FINSEQ_6:142 ;
A22: Rotate (c1,v) = c91 by A15;
then reconsider c = (Rotate (c1,v)) ^ (Rotate (c2,v)) as Path of G by A2, A16, A8, A18, A19, A10, A11, A20, A12, Th6;
vs1 ^' vs2 is_vertex_seq_of c by A18, A19, A10, A11, A20, A22, A12, GRAPH_2:44;
then c is cyclic by A21;
then reconsider c = c as Element of G -CycleSet by Def8;
take c ; :: thesis: ex v being Vertex of G st
( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & c = (Rotate (c1,v)) ^ (Rotate (c2,v)) )
take v ; :: thesis: ( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & c = (Rotate (c1,v)) ^ (Rotate (c2,v)) )
thus ( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & c = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) ; :: thesis: verum