theorem :: PRE_CIRC:8

for n being Nat
for a being set holds product (n |-> {a}) = {(n |-> a)}