p in Ext_Set (f,E) ;
then consider K being Element of SubFields E, g being Function of K,L such that
A: ( p = [K,g] & ex K1 being FieldExtension of F ex g1 being Function of K1,L st
( K1 = K & g1 = g & g1 is monomorphism & g1 is f -extending ) ) ;
thus p `2 is Function of (p `1),L by A; :: thesis: verum