theorem inS: :: FIELD_12:46

for F being Field
for E being FieldExtension of F
for L being b₁ -monomorphic Field
for f being Monomorphism of F,L
for K being strict FieldExtension of F
for g being Function of K,L st g is monomorphism holds
( [K,g] in Ext_Set (f,E) iff ( E is FieldExtension of K & F is Subfield of K & g is f -extending ) )