let A, B be set ; :: thesis: for f being Function st A c= dom f & f .: A c= B holds
A c= f " B
let f be Function; :: thesis: ( A c= dom f & f .: A c= B implies A c= f " B )
assume A c= dom f ; :: thesis: ( not f .: A c= B or A c= f " B )
then A1: A c= f " (f .: A) by Th75;
assume f .: A c= B ; :: thesis: A c= f " B
then f " (f .: A) c= f " B by RELAT_1:143;
hence A c= f " B by A1; :: thesis: verum