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 = { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & 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 Th52;
Rotate (c,v) = the Element of Rotated by A1, Def9;
then Rotate (c,v) in Rotated ;
then ex c9 being Element of G -CycleSet st
( Rotate (c,v) = c9 & rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) ;
hence rng (Rotate (c,v)) = rng c ; :: thesis: verum