Changes

Just to be on the safe side, I state this again in more standard terms.  The cartesian power <math>\underline\mathbb{B}^k,</math> as a cartesian product, is characterized by the possession of <math>k\!</math> projection maps <math>\pi_j : \underline\mathbb{B}^k \to \underline\mathbb{B},</math> for <math>j = 1 ~\text{to}~ k,</math> along with the property that any <math>k\!</math> maps <math>f_j : W \to \underline\mathbb{B},</math> from an arbitrary set <math>W\!</math> to <math>\underline\mathbb{B},</math> determine a unique map <math>f! : W \to \underline\mathbb{B}^k</math> such that <math>\pi_j (f!(w)) = f_j (w),\!</math> for all <math>j = 1 ~\text{to}~ k,</math> and for all <math>w \in W.</math>

Just to be on the safe side, I state this again in more standard terms.  The cartesian power <math>\underline\mathbb{B}^k,</math> as a cartesian product, is characterized by the possession of <math>k\!</math> projection maps <math>\pi_j : \underline\mathbb{B}^k \to \underline\mathbb{B},</math> for <math>j = 1 ~\text{to}~ k,</math> along with the property that any <math>k\!</math> maps <math>f_j : W \to \underline\mathbb{B},</math> from an arbitrary set <math>W\!</math> to <math>\underline\mathbb{B},</math> determine a unique map <math>f! : W \to \underline\mathbb{B}^k</math> such that <math>\pi_j (f!(w)) = f_j (w),\!</math> for all <math>j = 1 ~\text{to}~ k,</math> and for all <math>w \in W.</math>

Now suppose that the arbitrary set <math>W\!</math> in this construction is just the relevant universe <math>X.\!</math> Given that the function <math>f! : X \to \underline\mathbb{B}^k</math> is uniquely determined by the imagination <math>\underline{f} : (X \to \underline\mathbb{B})^k,</math> that is, by the <math>k\!</math>-tuple of propositions <math>\underline{f} = (f_1, \ldots, f_k),</math> it is safe to identify <math>f!\!</math> and <math>\underline{f}</math> as being a single function, and this makes it convenient on many occasions to refer to the identified function by means of its explicitly descriptive name <math>^{\backprime\backprime} (f_1, \ldots, f_k) \, ^{\prime\prime}.</math>  This facility of address is especially appropriate whenever a concrete term or a constructive precision is demanded by the context of discussion.

Now suppose that the arbitrary set W in this construction is just the relevant universe U.  Given that the function f! : U -> Bk is uniquely determined by the imagination f : (U -> B)k, that is, by the k-tuple of propositions f = <f1, ..., fk>, it is safe to identify f! and f as being a single function, and this makes it convenient on many occasions to refer to the identified function by means of its explicitly descriptive name "<f1, ..., fk>". This facility of address is especially appropriate whenever a concrete term or a constructive precision is demanded by the context of discussion.

=====1.3.10.7.  Stretching Operations=====

=====1.3.10.7.  Stretching Operations=====