set V = VecSp (E,F);

per cases ( E is F -finite or not E is F -finite ) ;

suppose E is F -finite ; :: thesis: not deg (E,F) is zero

then H1: VecSp (E,F) is finite-dimensional by FIELD_4:def 8;

now :: thesis: not deg (E,F) = 0

assume deg (E,F) = 0 ; :: thesis: contradiction
then A: dim (VecSp (E,F)) = 0 by FIELD_4:def 7;
ModuleStr(# the carrier of (VecSp (E,F)), the addF of (VecSp (E,F)), the ZeroF of (VecSp (E,F)), the lmult of (VecSp (E,F)) #) = (Omega). (VecSp (E,F)) by VECTSP_4:def 4
.= (0). (VecSp (E,F)) by A, H1, VECTSP_9:29 ;
then the carrier of ModuleStr(# the carrier of (VecSp (E,F)), the addF of (VecSp (E,F)), the ZeroF of (VecSp (E,F)), the lmult of (VecSp (E,F)) #) = {(0. (VecSp (E,F)))} by VECTSP_4:def 3;
then 1. E = 0. E by FIELD_4:def 6;
hence contradiction ; :: thesis: verum

end;

hence not deg (E,F) is zero ; :: thesis: verum

end;

suppose not E is F -finite ; :: thesis: not deg (E,F) is zero

then not VecSp (E,F) is finite-dimensional by FIELD_4:def 8;
hence not deg (E,F) is zero by FIELD_4:def 7; :: thesis: verum

end;

end;