thus 3 = (len X^3-2) - 1 by LL1
.= deg X^3-2 by HURWITZ:def 2 ; :: thesis: ( deg X^3-1 = 3 & deg X^2+X+1 = 2 & deg X^2-2 = 2 )
thus 3 = (len X^3-1) - 1 by LL1
.= deg X^3-1 by HURWITZ:def 2 ; :: thesis: ( deg X^2+X+1 = 2 & deg X^2-2 = 2 )
1. F_Rat <> 0. F_Rat ;
hence deg X^2+X+1 = 2 by FIELD_9:18; :: thesis: deg X^2-2 = 2
thus deg X^2-2 = 2 by FIELD_9:18; :: thesis: verum