J: Char (Z/ 2) = 2 by RING_3:def 6;
Z/ 2 is Subring of embField (canHomP X^2+X+1) by FIELD_4:def 1;
then I: Char (embField (canHomP X^2+X+1)) = 2 by J, RING_3:89;
H: 2 '*' alpha = 2 '*' ((1. (embField (canHomP X^2+X+1))) * alpha)
.= (2 '*' (1. (embField (canHomP X^2+X+1)))) * alpha by REALALG2:5
.= (0. (embField (canHomP X^2+X+1))) * alpha by I, REALALG2:24 ;
then alpha + alpha = 0. (embField (canHomP X^2+X+1)) by RING_5:2;
then (0. (embField (canHomP X^2+X+1))) - alpha = alpha + (alpha - alpha) by RLVECT_1:def 3
.= alpha + (0. (embField (canHomP X^2+X+1))) by RLVECT_1:15 ;
hence H3: - alpha = alpha ; :: thesis: ( alpha " = alpha-1 & alpha " <> alpha )
thus alpha " = alpha-1 by lemZ2, H3, RLVECT_1:31; :: thesis: alpha " <> alpha

now :: thesis: not alpha " = alpha

assume alpha " = alpha ; :: thesis: contradiction
then alpha = (- alpha) + (- (1. (embField (canHomP X^2+X+1)))) by RLVECT_1:31, lemZ2;
then alpha + alpha = (alpha + (- alpha)) + (- (1. (embField (canHomP X^2+X+1)))) by RLVECT_1:def 3
.= (0. (embField (canHomP X^2+X+1))) + (- (1. (embField (canHomP X^2+X+1)))) by RLVECT_1:5 ;
then - (0. (embField (canHomP X^2+X+1))) = - (- (1. (embField (canHomP X^2+X+1)))) by H, RING_5:2;
hence contradiction ; :: thesis: verum

end;

hence alpha " <> alpha ; :: thesis: verum