F is Subfield of embField (canHomP p)
by FIELD_2:17;

then F is Subring of embField (canHomP p) by pr1;

hence embField (canHomP p) is F -extending by FIELD_4:def 1; :: thesis: verum

then F is Subring of embField (canHomP p) by pr1;

hence embField (canHomP p) is F -extending by FIELD_4:def 1; :: thesis: verum