dim (VecSp (E,F)) is Nat ;
hence deg (E,F) is natural by Def7, Def6; :: thesis: verum