A1: (1 + 1) '*' (1. F_Rat) = (1 '*' (1. F_Rat)) + (1 '*' (1. F_Rat)) by RING_3:62
.= (1 '*' (1. F_Rat)) + (1. F_Rat) by RING_3:60
.= (1. F_Rat) + (1. F_Rat) by RING_3:60
.= 2 by GAUSSINT:13 ;
A2: (2 + 2) '*' (1. F_Rat) = (2 '*' (1. F_Rat)) + (2 '*' (1. F_Rat)) by RING_3:62
.= 4 by A1 ;
thus Discriminant X^2+X+1 = ((1. F_Rat) ^2) - (4 '*' (1. F_Rat)) by FIELD_9:def 10
.= - 3 by A2, GAUSSINT:13 ; :: thesis: verum