theorem Th7: :: FIELD_2:8

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 right_complementable