let F be Field; :: thesis: for a, b being Element of F st b ^2 = a holds
eval ((X^2- a),b) = 0. F
let a, b be Element of F; :: thesis: ( b ^2 = a implies eval ((X^2- a),b) = 0. F )
assume b ^2 = a ; :: thesis: eval ((X^2- a),b) = 0. F
then A: - a = - (b * b) by O_RING_1:def 1
.= b * (- b) by VECTSP_1:8 ;
thus eval ((X^2- a),b) = eval (<%(- a),(- (0. F)),(1. F)%>,b)
.= eval (<%(b * (- b)),(- (b + (- b))),(1. F)%>,b) by A, RLVECT_1:5
.= eval (((rpoly (1,b)) *' (rpoly (1,(- b)))),b) by lemred3z
.= (eval ((rpoly (1,b)),b)) * (eval ((rpoly (1,(- b))),b)) by POLYNOM4:24
.= (b - b) * (eval ((X- (- b)),b)) by HURWITZ:29
.= (0. F) * (eval ((X- (- b)),b)) by RLVECT_1:15
.= 0. F ; :: thesis: verum