theorem z22: :: FIELD_9:40

( X^2+1 = X-1 *' X-1 & Roots X^2+1 = {(1. (Z/ 2))} )