The split cap on merged vectors

The multiplicative midpoint of the cap recursion: the split cap (smaller cap tensored with one evaluation) evaluated on a transported merge of model vectors is the product of the smaller cap value and the strand evaluation.

theorem RS.omegaFun_capTensor_merge {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (x : (superPow (stdSuperPair k ℓ) (m + m)).even) (y : (superPow (stdSuperPair k ℓ) 2).even) : (omegaFun f P (((HomSpace.tensor f (m + m) 0 2 0) (bundleCapClass f m)) (evClass f))) ((stdToOmega f P e (m + m + 2)).evenMap ((powMerge (stdSuperPair k ℓ) (m + m) 2).evenMap (evenPair x y))) = capVal f P e m x * (omegaFun f P (evClass f)) ((stdToOmega f P e 2).evenMap y)

The split cap is multiplicative over the merge.