( 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