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

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