:: deftheorem defines Permutations NUMBER17:def 5 :
for A being relational set holds Permutations A = { (Permutations f) where f is Element of A : f in A } ;