for X, Y being non empty set
for S being semiring_of_sets of X
for f being Function of X,Y st f is one-to-one holds
f .: S is semiring_of_sets of Y by Thm11, Thm12;