theorem LOC1: :: FINANCE5:1

for A, I, y being non empty set
for F being Function of A,I holds { z where z is Element of A : F . z in y } = F " y