let p be quadratic Element of the carrier of (Polynom-Ring (Z/ 2)); :: thesis: ( p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> implies Z/ 2 is SplittingField of p )
assume A: p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> ; :: thesis: Z/ 2 is SplittingField of p
B: Z/ 2 is FieldExtension of Z/ 2 by FIELD_4:6;

now :: thesis: for E being FieldExtension of Z/ 2 st p splits_in E & E is Subfield of Z/ 2 holds
E == Z/ 2

let E be FieldExtension of Z/ 2; :: thesis: ( p splits_in E & E is Subfield of Z/ 2 implies E == Z/ 2 )
assume C: ( p splits_in E & E is Subfield of Z/ 2 ) ; :: thesis: E == Z/ 2
then D: ( the carrier of E c= the carrier of (Z/ 2) & the addF of E = the addF of (Z/ 2) || the carrier of E & the multF of E = the multF of (Z/ 2) || the carrier of E & 1. E = 1. (Z/ 2) & 0. E = 0. (Z/ 2) ) by EC_PF_1:def 1;

now :: thesis: for o being object st o in the carrier of (Z/ 2) holds
o in the carrier of E

let o be object ; :: thesis: ( o in the carrier of (Z/ 2) implies b₁ in the carrier of E )
assume o in the carrier of (Z/ 2) ; :: thesis: b₁ in the carrier of E

per cases then ( o = 0. (Z/ 2) or o = 1. (Z/ 2) ) by cz2, TARSKI:def 2;

suppose o = 0. (Z/ 2) ; :: thesis: b₁ in the carrier of E

hence o in the carrier of E by D; :: thesis: verum

end;

suppose o = 1. (Z/ 2) ; :: thesis: b₁ in the carrier of E

hence o in the carrier of E by D; :: thesis: verum

end;

end;

end;

then the carrier of E = the carrier of (Z/ 2) by D, TARSKI:2;
then Z/ 2 is Subfield of E by D, EC_PF_1:def 1;
hence E == Z/ 2 by C, FIELD_7:def 2; :: thesis: verum

end;

hence Z/ 2 is SplittingField of p by A, z25, B, FIELD_8:def 1; :: thesis: verum