theorem Th9: :: FIELD_2:10

for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is distributive