Disjoint streams of independent fair bits produce independent uniform variables

By [F1], every specified pattern on $n$ distinct coordinates has probability $2^{-n}$. Thus $K_{s,n}$ is uniform on $\{0,\dots ,2^n-1\}$. The events that the first $m$ bits after position $n$ are all zero, or all one, decrease to the corresponding constant-tail events and have probabilities $2^{-m}$. By [F4], both constant-tail events have probability zero. The partial sums defining each $U_s$ are measurable and increase to $U_s$ by [F6].

Fix a dyadic threshold $t=k{2}^{-n}$ with $0\le k\le 2^n$. If $K_{s,n}<k$, then $U_s\le t$; if $K_{s,n}>k$, then $U_s>t$; if $K_{s,n}=k$, then $U_s\le t$ only on the null event $T_{s,n}=0$. Hence $\mathbb{P}(U_s\le k{2}^{-n})=k{2}^{-n}$. For an arbitrary $t\in [0,1]$, dyadic lower and upper approximations differ by at most $2^{-n}$, so monotonicity of the CDF and passage to the limit give $\mathbb{P}(U_s\le t)=t$. Outside $[0,1]$ the CDF is $0$ or $1$.

For finitely many streams and dyadic thresholds $t_s=k_s{2}^{-n}$, the joint event ${\bigcap }_s\{U_s\le t_s\}$ differs by a null set from the event that every prefix integer $K_{s,n}<k_s$. Injectivity within each sequence and pairwise disjointness of their ranges make all prefix coordinates distinct. By [F2] these coordinate bits are independent and by [F1] each is fair, so the probability that each stream's prefix integer is below $k_s$ is the product ${\prod }_s(k_s{2}^{-n})$.

For arbitrary thresholds $t_s\in [0,1]$, dyadic lower and upper approximations squeeze the joint probability between products converging to ${\prod }_s{t}_s$. Thus the joint CDF equals the product-uniform CDF. The lower rectangles ${\prod }_s[0,t_s]$, including the whole cube, are closed under intersections. They generate each coordinate slab $\{x:x_s\le t\}$ by taking the other thresholds to be $1$; complements and finite intersections then give the intersections of the cube with all rational half-open boxes (thresholds outside $[0,1]$ give empty or full slabs). By [F7] these generate the relative Borel sigma-algebra of the cube. Both laws have total mass one there, a finite-measure exhaustion. Thus [F5] identifies the joint law with the product-uniform law. In particular every Borel rectangle has the product of its marginal probabilities, so the rectangle criterion [F3] gives independence of the generated sigma-algebras.