:: deftheorem defines Per CALCUL_2:def 2 :
for D being non empty set
for f being FinSequence of D
for P being Permutation of (dom f) holds Per (f,P) = P * f;