let A, I, y be non empty set ; :: thesis: for F being Function of A,I holds { z where z is Element of A : F . z in y } = F " y
let F be Function of A,I; :: thesis: { z where z is Element of A : F . z in y } = F " y
for x being object holds
( x in { z where z is Element of A : F . z in y } iff x in F " y )

proof

let x be object ; :: thesis: ( x in { z where z is Element of A : F . z in y } iff x in F " y )

hereby :: thesis: ( x in F " y implies x in { z where z is Element of A : F . z in y } )

assume x in { z where z is Element of A : F . z in y } ; :: thesis: x in F " y
then consider z being Element of A such that
A1: ( x = z & F . z in y ) ;
z in A ;
then z in dom F by FUNCT_2:def 1;
hence x in F " y by FUNCT_1:def 7, A1; :: thesis: verum

end;

assume x in F " y ; :: thesis: x in { z where z is Element of A : F . z in y }
then ( x in dom F & F . x in y ) by FUNCT_1:def 7;
hence x in { z where z is Element of A : F . z in y } ; :: thesis: verum

end;

hence { z where z is Element of A : F . z in y } = F " y by TARSKI:2; :: thesis: verum