theorem e1a: :: FIELD_12:10

for F1, F2, L being Field
for E1 being FieldExtension of F1
for K1 being b₄ -extending FieldExtension of F1
for h1 being Function of F1,L
for h2 being Function of E1,L
for h3 being Function of K1,L st h2 is h1 -extending & h3 is h2 -extending holds
h3 is h1 -extending