Let Xi and i be given.
We will prove product_component Xi i = (apply_fun Xi i) 0.
Use reflexivity.
∎