set f = minimal_polynom (z,K);
A7: not minimal_polynom (z,K) is zero by A1, A2, Def7;
reconsider f = minimal_polynom (z,K) as Polynomial of K ;
deg f <> - 1 by A7;
then A8: len f <> 0 ;
(len f) + 1 > 0 + 1 by A8, XREAL_1:8;
then len f >= 1 by NAT_1:13;
hence deg (minimal_polynom (z,K)) is Element of NAT by INT_1:3; :: thesis: verum