theorem e1a: :: FIELD_8:41

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