for a, b being set holds (a .--> b) " = b .--> a