for X, Y being non empty set
for f being Function of X,Y
for cFXa, cFXb being Filter of X st cFXb is_filter-finer_than cFXa holds
filter_image (f,cFXb) is_filter-finer_than filter_image (f,cFXa)