let G be Graph; :: thesis: for c being Element of G -CycleSet
for v being Vertex of G st v in G -VSet (rng c) holds
rng (Rotate c,v) = rng c
let c be Element of G -CycleSet ; :: thesis: for v being Vertex of G st v in G -VSet (rng c) holds
rng (Rotate c,v) = rng c
let v be Vertex of G; :: thesis: ( v in G -VSet (rng c) implies rng (Rotate c,v) = rng c )
assume A1: v in G -VSet (rng c) ; :: thesis: rng (Rotate c,v) = rng c
then reconsider Rotated = { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } as non empty Subset of (G -CycleSet ) by Th57;
Rotate c,v = choose Rotated by A1, Def9;
then Rotate c,v in Rotated ;
then consider c' being Element of G -CycleSet such that
A2: ( Rotate c,v = c' & rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) ;
thus rng (Rotate c,v) = rng c by A2; :: thesis: verum