for X, Y being set
for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds
X = Y by Th87;