# Definition of subatomic projection of funcoids

I have proved that for every funcoid $f:\prod A\rightarrow\prod B$ (where $A$ and $B$ are indexed families of sets) there exists a funcoid $\mathrm{Pr}^{(A)}_k f$ (subatomic projection) defined by the formula:

$\mathcal{X} \mathrel{\left[ \Pr^{\left( A \right)}_k f \right]} \mathcal{Y} \Leftrightarrow \\ \prod^{\mathsf{RLD}}_{i \in \mathrm{dom}\, A} \left( \left\{ \begin{array}{ll} 1^{\mathfrak{F} \left( A_i \right)} & \mathrm{if}\, i \neq k ;\\ \mathcal{X} & \mathrm{if}\, i = k \end{array} \right. \right) \mathrel{\left[ f \right]} \prod^{\mathsf{RLD}}_{i \in \mathrm{dom}\, B} \left( \left\{ \begin{array}{ll} 1^{\mathfrak{F} \left( B_i \right)} & \mathrm{if}\, i \neq k ;\\ \mathcal{Y} & \mathrm{if}\, i = k \end{array} \right. \right) .$

My draft book is modified to include this new theorem.