for n being Nat
for a, b being set holds (a .--> b) * (n |-> a) = n |-> b