theorem :: TOPMETR2:1

for f, g being Function st f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ) holds
f +* g is one-to-one