let F1, F2 be Field; :: thesis: 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
let E1 be FieldExtension of F1; :: thesis: for E2 being FieldExtension of F2
for K1 being E1 -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
let E2 be FieldExtension of F2; :: thesis: for K1 being E1 -extending FieldExtension of F1
for K2 being E2 -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
let K1 be E1 -extending FieldExtension of F1; :: thesis: for K2 being E2 -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
let K2 be E2 -extending FieldExtension of F2; :: thesis: 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
let h1 be Function of F1,F2; :: thesis: 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
let h2 be Function of E1,E2; :: thesis: for h3 being Function of K1,K2 st h2 is h1 -extending & h3 is h2 -extending holds
h3 is h1 -extending
let h3 be Function of K1,K2; :: thesis: ( h2 is h1 -extending & h3 is h2 -extending implies h3 is h1 -extending )
assume AS: ( h2 is h1 -extending & h3 is h2 -extending ) ; :: thesis: h3 is h1 -extending

now :: thesis: for a being Element of F1 holds h3 . a = h1 . a

let a be Element of F1; :: thesis: h3 . a = h1 . a
thus h3 . a = h3 . (@ (a,E1)) by FIELD_7:def 4
.= h2 . (@ (a,E1)) by AS
.= h2 . a by FIELD_7:def 4
.= h1 . a by AS ; :: thesis: verum

end;

hence h3 is h1 -extending ; :: thesis: verum