reconsider p = <%(0. F),(0. F),(1. F)%> as quadratic Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
DC p = - (4 '*' (0. F)) by defDCpq
.= (- 4) '*' ((1. F) * (0. F)) by RING_3:63
.= ((- 4) '*' (1. F)) * (0. F) by REALALG2:5 ;
then p is DC-square ;
hence ex b₁ being quadratic Element of the carrier of (Polynom-Ring F) st
( b₁ is monic & b₁ is DC-square ) ; :: thesis: verum