:: deftheorem defines \ TRANSGEO:def 1 :
for A being non empty set
for f, g being Permutation of A holds f \ g = (g * f) * (g ");