:: deftheorem defines Permutations NUMBER17:def 3 :
for f being Function holds Permutations f = { (f * p) where p is Permutation of (dom f) : verum } ;