for E being non empty finite set
for G being finite Group
for p being prime Nat
for T being LeftOperation of G,E st G is p -group holds
(card (the_fixed_points_of T)) mod p = (card E) mod p