theorem resisf (A F: set): $ isfun F -> isfun (F |` A) $;
F |` A C_ F -> isfun F -> isfun (F |` A)
F |` A C_ F
isfun F -> isfun (F |` A)