set K = unionField (S,f,E);
set g = unionExt (S,f,E);
A: unionExt (S,f,E) is monomorphism by inSb;
unionField (S,f,E) is Subfield of E by inSa;
then B: E is FieldExtension of unionField (S,f,E) by FIELD_4:7;
C: F is Subfield of unionField (S,f,E) by FIELD_4:7;
unionExt (S,f,E) is f -extending by inSb;
hence [(unionField (S,f,E)),(unionExt (S,f,E))] is Element of Ext_Set (f,E) by A, B, C, inS; :: thesis: verum