theorem Fi1a: :: FIELD_9:56

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds (X- (sqrt a)) *' (X+ (sqrt a)) = X^2- a