for X being set holds 1_ (SymGroup X) = id X