consider a1 being non zero Element of R, c1 being Element of R such that
H: p = <%c1,(0. R),a1%> by defpur;

Y: now :: thesis: for x being Element of R st x = DC p holds
ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) )

let x be Element of R; :: thesis: ( x = DC p implies ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) ) )
assume x = DC p ; :: thesis: ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) )
then consider b, c being Element of R such that
A: ( p = <%c,b,(1. R)%> & x = (b ^2) - (4 '*' c) ) by defDCm;
B: b = <%c1,(0. R),a1%> . 1 by A, H, qua1
.= 0. R by qua1 ;
thus ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) ) by A, B; :: thesis: verum

end;

now :: thesis: for x being Element of R st ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) ) holds
x = DC p

let x be Element of R; :: thesis: ( ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) ) implies x = DC p )
assume ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) ) ; :: thesis: x = DC p
then consider c being Element of R such that
C: ( p = <%c,(0. R),(1. R)%> & x = - (4 '*' c) ) ;
- (4 '*' c) = ((0. R) ^2) - (4 '*' ((1. R) * c)) ;
hence x = DC p by C, defDCm; :: thesis: verum

end;

hence for b₁ being Element of R holds
( b₁ = Discriminant p iff ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & b₁ = - (4 '*' c) ) ) by Y; :: thesis: verum