1\THEOREM IMAGE_INSERT pred_sets
2|- !f x s. IMAGE f(x INSERT s) = (f x) INSERT (IMAGE f s)
3\ENDTHEOREM
4