( GoB (Rotate (f,p)) = GoB f & f is_sequence_on GoB f ) by Th28, GOBOARD5:def 5;
hence Rotate (f,p) is_sequence_on GoB (Rotate (f,p)) by Th34; :: according to GOBOARD5:def 5 :: thesis: verum