let X, X1 be set ; :: thesis: for F being Function st X c= F " X1 holds
F .: X c= X1
let F be Function; :: thesis: ( X c= F " X1 implies F .: X c= X1 )
assume X c= F " X1 ; :: thesis: F .: X c= X1
then A1: F .: X c= F .: (F " X1) by RELAT_1:123;
F .: (F " X1) c= X1 by FUNCT_1:75;
hence F .: X c= X1 by A1; :: thesis: verum