Let X and Tx be given.

Assume Hfd: finite_dimensional_space X Tx.

Apply Hfd to the current goal.

Assume HTx Hexm.

An exact proof term for the current goal is HTx.

∎