theorem resfin (A F: set): $ finite F -> finite (F |` A) $;
F |` A C_ F -> finite F -> finite (F |` A)
F |` A C_ F
finite F -> finite (F |` A)