let Omega, Omega2 be non empty set ; :: thesis: for F being Function of Omega,Omega2
for y being non empty set holds { z where z is Element of Omega : F . z is Element of y } = F " y

let F be Function of Omega,Omega2; :: thesis: for y being non empty set holds { z where z is Element of Omega : F . z is Element of y } = F " y
let y be non empty set ; :: thesis: { z where z is Element of Omega : F . z is Element of y } = F " y
set D = { z where z is Element of Omega : F . z is Element of y } ;
for x being object holds
( x in { z where z is Element of Omega : F . z is Element of y } iff x in F " y )
proof
let x be object ; :: thesis: ( x in { z where z is Element of Omega : F . z is Element of y } iff x in F " y )
hereby :: thesis: ( x in F " y implies x in { z where z is Element of Omega : F . z is Element of y } )
assume x in { z where z is Element of Omega : F . z is Element of y } ; :: thesis: x in F " y
then consider z being Element of Omega such that
A1: ( x = z & F . z is Element of y ) ;
z in Omega ;
then A2: z in dom F by FUNCT_2:def 1;
F . z in y by A1;
then z in F " y by ;
hence x in F " y by A1; :: thesis: verum
end;
assume x in F " y ; :: thesis: x in { z where z is Element of Omega : F . z is Element of y }
then A3: ( x in dom F & F . x in y ) by FUNCT_1:def 7;
thus x in { z where z is Element of Omega : F . z is Element of y } by A3; :: thesis: verum
end;
hence { z where z is Element of Omega : F . z is Element of y } = F " y by TARSKI:2; :: thesis: verum