theorem :: GRFUNC_1:12

for f, g being Function st f is one-to-one holds
f /\ g is one-to-one by Th10, XBOOLE_1:17;