A (non‐central) chi‐squared mixture of non‐central chi‐squareds is (non‐central) chi‐squared and related results, corollaries and applications. Issue 1 (11th August 2021)