1\THEOREM IMAGE_UNION pred_sets
2|- !f s t. IMAGE f(s UNION t) = (IMAGE f s) UNION (IMAGE f t)
3\ENDTHEOREM
4