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