:: deftheorem defines (*) EUCLID_7:def 2 :
for D being set
for F being FinSequence of D
for h being Permutation of (dom F) holds F (*) h = F * h;