let F1, F2 be Field; :: thesis:
let E1 be FieldExtension of F1; :: thesis:
let E2 be FieldExtension of F2; :: thesis:
let K1 be E1 -extending FieldExtension of F1; :: thesis:
let K2 be E2 -extending FieldExtension of F2; :: thesis:
let h1 be Function of F1,F2; :: thesis:
let h2 be Function of E1,E2; :: thesis:
let h3 be Function of K1,K2; :: thesis:
assume AS: ( h2 is h1 -extending & h3 is h2 -extending ) ; :: thesis:

let a be Element of F1; :: thesis:
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:

end;

hence h3 is h1 -extending ; :: thesis: