[STATEMENT]
lemma cblinfun_extension_apply:
  assumes "cblinfun_extension_exists S f"
    and "v \<in> S"
  shows "(cblinfun_extension S f) *\<^sub>V v = f v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_extension S f *\<^sub>V v = f v
[PROOF STEP]
by (smt assms cblinfun_extension_def cblinfun_extension_exists_def tfl_some)