let p be quadratic Polynomial of (Z/ 2); :: thesis: ( p splits_in Z/ 2 iff p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> )
H: p in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} by pz2;

A: now :: thesis: ( p splits_in Z/ 2 implies p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> )

assume p splits_in Z/ 2 ; :: thesis: p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>
then consider a being non zero Element of (Z/ 2), q being Ppoly of Z/ 2 such that
A1: p = a * q by FIELD_4:def 5;
thus p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> by A1, z24; :: thesis: verum

end;

now :: thesis: ( p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> implies p splits_in Z/ 2 )

assume p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> ; :: thesis: p splits_in Z/ 2

per cases then ( p = <%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%> or p = <%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%> or p = <%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> ) by H, ENUMSET1:def 2;

suppose p = <%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%> ; :: thesis: p splits_in Z/ 2

then B: p = (rpoly (1,(- (0. (Z/ 2))))) *' <%(0. (Z/ 2)),(1. (Z/ 2))%> by z21, RING_5:10
.= (1. (Z/ 2)) * ((rpoly (1,(0. (Z/ 2)))) *' (rpoly (1,(0. (Z/ 2))))) by RING_5:10 ;
rpoly (1,(0. (Z/ 2))) is Ppoly of Z/ 2 by RING_5:51;
then (rpoly (1,(0. (Z/ 2)))) *' (rpoly (1,(0. (Z/ 2)))) is Ppoly of Z/ 2 by RING_5:52;
hence p splits_in Z/ 2 by B, FIELD_4:def 5; :: thesis: verum

end;

suppose p = <%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%> ; :: thesis: p splits_in Z/ 2

then B: p = (rpoly (1,(- (1. (Z/ 2))))) *' <%(1. (Z/ 2)),(- (- (1. (Z/ 2))))%> by z22, RING_5:10
.= (1. (Z/ 2)) * ((rpoly (1,(1. (Z/ 2)))) *' (rpoly (1,(1. (Z/ 2))))) by RING_5:10, cz2a ;
rpoly (1,(1. (Z/ 2))) is Ppoly of Z/ 2 by RING_5:51;
then (rpoly (1,(1. (Z/ 2)))) *' (rpoly (1,(1. (Z/ 2)))) is Ppoly of Z/ 2 by RING_5:52;
hence p splits_in Z/ 2 by B, FIELD_4:def 5; :: thesis: verum

end;

suppose p = <%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> ; :: thesis: p splits_in Z/ 2

then B: p = (rpoly (1,(- (0. (Z/ 2))))) *' <%(1. (Z/ 2)),(- (- (1. (Z/ 2))))%> by z23, RING_5:10
.= (1. (Z/ 2)) * ((rpoly (1,(0. (Z/ 2)))) *' (rpoly (1,(1. (Z/ 2))))) by RING_5:10, cz2a ;
( rpoly (1,(1. (Z/ 2))) is Ppoly of Z/ 2 & rpoly (1,(0. (Z/ 2))) is Ppoly of Z/ 2 ) by RING_5:51;
then (rpoly (1,(1. (Z/ 2)))) *' (rpoly (1,(0. (Z/ 2)))) is Ppoly of Z/ 2 by RING_5:52;
hence p splits_in Z/ 2 by B, FIELD_4:def 5; :: thesis: verum

end;

end;

end;

hence ( p splits_in Z/ 2 iff p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> ) by A; :: thesis: verum