theorem Th2: :: RING_EMB:2

for a, b being non empty set ex c being non empty set st
( a /\ c = {} & ex f being Function st
( f is one-to-one & dom f = b & rng f = c ) )