Y:
now for x being Element of R st x = DC p holds
ex b, c being Element of R st
( p = <%c,b,(1. R)%> & x = (b ^2) - (4 '*' c) )let x be
Element of
R;
( x = DC p implies ex b, c being Element of R st
( p = <%c,b,(1. R)%> & x = (b ^2) - (4 '*' c) ) )assume
x = DC p
;
ex b, c being Element of R st
( p = <%c,b,(1. R)%> & x = (b ^2) - (4 '*' c) )then consider a being non
zero Element of
R,
b,
c being
Element of
R such that A:
(
p = <%c,b,a%> &
x = (b ^2) - ((4 '*' a) * c) )
by defDC;
H:
len p = 3
by A, qua3;
3
-' 1
= 3
- 1
by XREAL_0:def 2;
then a =
p . ((len p) -' 1)
by H, A, qua1
.=
LC p
by RATFUNC1:def 6
;
then B:
a = 1. R
by RATFUNC1:def 7;
then
(b ^2) - ((4 '*' a) * c) = (b ^2) - (4 '*' ((1. R) * c))
by REALALG2:5;
hence
ex
b,
c being
Element of
R st
(
p = <%c,b,(1. R)%> &
x = (b ^2) - (4 '*' c) )
by A, B;
verum end;
now for x being Element of R st ex b, c being Element of R st
( p = <%c,b,(1. R)%> & x = (b ^2) - (4 '*' c) ) holds
x = DC plet x be
Element of
R;
( ex b, c being Element of R st
( p = <%c,b,(1. R)%> & x = (b ^2) - (4 '*' c) ) implies x = DC p )assume
ex
b,
c being
Element of
R st
(
p = <%c,b,(1. R)%> &
x = (b ^2) - (4 '*' c) )
;
x = DC pthen consider b,
c being
Element of
R such that C:
(
p = <%c,b,(1. R)%> &
x = (b ^2) - (4 '*' c) )
;
(4 '*' (1. R)) * c = 4
'*' ((1. R) * c)
by REALALG2:5;
hence
x = DC p
by C, defDC;
verum end;
hence
for b1 being Element of R holds
( b1 = Discriminant p iff ex b, c being Element of R st
( p = <%c,b,(1. R)%> & b1 = (b ^2) - (4 '*' c) ) )
by Y; verum