theorem lemred: :: FIELD_9:28

for F being non 2 -characteristic Field
for a being non zero Element of F
for b, c, w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
for r1, r2 being Element of F st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2))