let E be FieldExtension of F; :: thesis: ( E is F -quadratic implies E is F -finite )
assume E is F -quadratic ; :: thesis: E is F -finite
then VecSp (E,F) is finite-dimensional by FIELD_4:def 7;
hence E is F -finite by FIELD_4:def 8; :: thesis: verum