let p be Element of Ext_Set (f,E); :: thesis: p is pair
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 is pair by A; :: thesis: verum