theorem :: YELLOW_2:10

for L, M being non empty RelStr
for f being Function of L,M
for y being Element of (Image f) ex x being Element of L st f . x = y