theorem Th142: :: FINSEQ_2:144

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