F = f . 0 by dA;
then F is Subfield of SeqField f by Fsub;
hence SeqField f is F -extending by FIELD_4:7; :: thesis: verum