for G being Group
for E being non empty set
for a being Element of E
for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T))