begin
theorem
for
a,
b,
c being ( ( ) (
complex real ext-real )
Real)
for
z being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
delta (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
>= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
/ (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
/ (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) holds
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= - (b : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) ;
theorem
for
a,
b,
c being ( ( ) (
complex real ext-real )
Real)
for
z being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
delta (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
< 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= (- (b : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
+ (((sqrt (- (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V69() V75() ) set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) holds
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= (- (b : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
+ ((- ((sqrt (- (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V69() V75() ) set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ;
theorem
for
a,
b,
c being ( ( ) (
complex real ext-real )
Real)
for
z,
z1,
z2 being ( (
complex ) (
complex )
number ) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
z being ( (
complex ) (
complex )
number ) holds
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
z : ( (
complex ) (
complex )
number ) ) : ( ( ) (
complex )
set )
= Quard (
a : ( ( ) (
complex real ext-real )
Real) ,
z1 : ( (
complex ) (
complex )
number ) ,
z2 : ( (
complex ) (
complex )
number ) ,
z : ( (
complex ) (
complex )
number ) ) : ( ( ) ( )
set ) ) holds
(
b : ( ( ) (
complex real ext-real )
Real)
/ a : ( ( ) (
complex real ext-real )
Real) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
= - (z1 : ( ( complex ) ( complex ) number ) + z2 : ( ( complex ) ( complex ) number ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) &
c : ( ( ) (
complex real ext-real )
Real)
/ a : ( ( ) (
complex real ext-real )
Real) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
= z1 : ( (
complex ) (
complex )
number )
* z2 : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) ;
theorem
for
a,
b,
c,
d,
a9,
b9,
c9,
d9 being ( ( ) (
complex real ext-real )
Real) st ( for
z being ( (
complex ) (
complex )
number ) holds
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
d : ( ( ) (
complex real ext-real )
Real) ,
z : ( (
complex ) (
complex )
number ) ) : ( ( ) (
complex )
set )
= Polynom (
a9 : ( ( ) (
complex real ext-real )
Real) ,
b9 : ( ( ) (
complex real ext-real )
Real) ,
c9 : ( ( ) (
complex real ext-real )
Real) ,
d9 : ( ( ) (
complex real ext-real )
Real) ,
z : ( (
complex ) (
complex )
number ) ) : ( ( ) (
complex )
set ) ) holds
(
a : ( ( ) (
complex real ext-real )
Real)
= a9 : ( ( ) (
complex real ext-real )
Real) &
b : ( ( ) (
complex real ext-real )
Real)
= b9 : ( ( ) (
complex real ext-real )
Real) &
c : ( ( ) (
complex real ext-real )
Real)
= c9 : ( ( ) (
complex real ext-real )
Real) &
d : ( ( ) (
complex real ext-real )
Real)
= d9 : ( ( ) (
complex real ext-real )
Real) ) ;
theorem
for
b,
c,
d being ( ( ) (
complex real ext-real )
Real)
for
z being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) st
b : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
delta (
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
d : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
>= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
d : ( ( ) (
complex real ext-real )
Real) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
set )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= ((- c : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) + (sqrt (delta (b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) ,d : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
/ (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= ((- c : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) - (sqrt (delta (b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) ,d : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
/ (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) holds
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= - (c : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) ;
theorem
for
b,
c,
d being ( ( ) (
complex real ext-real )
Real)
for
z being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) st
b : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
delta (
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
d : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
< 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
d : ( ( ) (
complex real ext-real )
Real) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
set )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= (- (c : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
+ (((sqrt (- (delta (b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) ,d : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V69() V75() ) set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) holds
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= (- (c : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
+ ((- ((sqrt (- (delta (b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) ,d : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V69() V75() ) set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ;
theorem
for
a,
b,
c being ( ( ) (
complex real ext-real )
Real)
for
z being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
delta (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
>= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
set )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) + (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
/ (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= ((- b : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) - (sqrt (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
/ (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= - (b : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) holds
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ;
theorem
for
a,
b,
c being ( ( ) (
complex real ext-real )
Real)
for
z being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) st
a : ( ( ) (
complex real ext-real )
Real)
<> 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
delta (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
< 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
Polynom (
a : ( ( ) (
complex real ext-real )
Real) ,
b : ( ( ) (
complex real ext-real )
Real) ,
c : ( ( ) (
complex real ext-real )
Real) ,
0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
set )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= (- (b : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
+ (((sqrt (- (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V69() V75() ) set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) & not
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= (- (b : ( ( ) ( complex real ext-real ) Real) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) )
+ ((- ((sqrt (- (delta (a : ( ( ) ( complex real ext-real ) Real) ,b : ( ( ) ( complex real ext-real ) Real) ,c : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) / (2 : ( ( ) ( non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() ) Element of NAT : ( ( ) ( V69() V70() V71() V72() V73() V74() V75() ) Element of K19(REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V69() V70() V71() V75() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V69() V75() ) set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) holds
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= 0 : ( ( ) (
empty ordinal natural complex real ext-real non
positive non
negative V43()
V44()
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K19(
REAL : ( ( ) (
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ;
begin
theorem
for
z1,
z2,
z3,
s1,
s2,
s3 being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) st ( for
z being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) holds
Polynom (
z1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ,
z2 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ,
z3 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
set )
= Polynom (
s1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ,
s2 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ,
s3 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ,
z : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) : ( ( ) (
complex )
set ) ) holds
(
z1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= s1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) &
z2 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= s2 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) &
z3 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) )
= s3 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) (
V69()
V75() )
set ) ) ) ;