for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is Field by Th6, Th8, Th9, Th7, Th10;