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.

Leave a Reply