Fixed theorem with unintended free variable.
The theorem about finiteness of generalised unions is now just proved once.