I'm surprised nobody's done these!

**40** : Preimages preserve set operations (see 41), and partitions are collections of subsets defined by set operations. Then {union over f*(partition)} = f*(union over partition) = f*(Y) = X, and similarly for empty pairwise intersection.

**41** : Ah, I just saw this hadn't been proven yet. Yes, because the logical operations and set operations "commute" in the definition of the preimage set - i.e. f*(S and T) = {x in X : f(x) in S and T} = {x in X : f(x) in S} and {x in X : f(x) in T}, and similarly for or.

**40** : Preimages preserve set operations (see 41), and partitions are collections of subsets defined by set operations. Then {union over f*(partition)} = f*(union over partition) = f*(Y) = X, and similarly for empty pairwise intersection.

**41** : Ah, I just saw this hadn't been proven yet. Yes, because the logical operations and set operations "commute" in the definition of the preimage set - i.e. f*(S and T) = {x in X : f(x) in S and T} = {x in X : f(x) in S} and {x in X : f(x) in T}, and similarly for or.