F is Subfield of unionField (S,f,E) by Fsuba;
hence unionField (S,f,E) is F -extending by FIELD_4:7; :: thesis: verum