:: POLYEQ_2 semantic presentation

begin

definition
let a, b, c, d, e, x be ( ( complex ) ( complex ) number ) ;
func Polynom (a,b,c,d,e,x) -> ( ( ) ( ) set ) equals :: POLYEQ_2:def 1
((((a : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * (x : ( ( ) ( ) M2(K6(b : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( ) set ) )) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (b : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * (x : ( ( ) ( ) M2(K6(b : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( ) set ) )) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (c : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * (x : ( ( ) ( ) M2(K6(b : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( ) set ) )) ^2) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + (d : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) * x : ( ( ) ( ) M2(K6(b : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) + e : ( ( ) ( complex real ext-real ) M2( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) )) : ( ( ) ( ) set ) ;
end;

registration
let a, b, c, d, e, x be ( ( complex ) ( complex ) number ) ;
cluster Polynom (a : ( ( complex ) ( complex ) set ) ,b : ( ( complex ) ( complex ) set ) ,c : ( ( complex ) ( complex ) set ) ,d : ( ( complex ) ( complex ) set ) ,e : ( ( complex ) ( complex ) set ) ,x : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) -> complex ;
end;

registration
let a, b, c, d, e, x be ( ( real ) ( complex real ext-real ) number ) ;
cluster Polynom (a : ( ( real ) ( complex real ext-real ) set ) ,b : ( ( real ) ( complex real ext-real ) set ) ,c : ( ( real ) ( complex real ext-real ) set ) ,d : ( ( real ) ( complex real ext-real ) set ) ,e : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex ) set ) -> real ;
end;

theorem :: POLYEQ_2:1
for a, c, e, x being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & e : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & (c : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * e : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,c : ( ( real ) ( complex real ext-real ) number ) ,0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,e : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) holds
( x : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & ( x : ( ( real ) ( complex real ext-real ) number ) = sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) : ( ( real ) ( complex real ext-real ) set ) or x : ( ( real ) ( complex real ext-real ) number ) = sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) : ( ( real ) ( complex real ext-real ) set ) or x : ( ( real ) ( complex real ext-real ) number ) = - (sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) or x : ( ( real ) ( complex real ext-real ) number ) = - (sqrt (((- c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (delta (a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,e : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) ) : ( ( real ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) ) ;

theorem :: POLYEQ_2:2
for a, b, c, x, y being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & y : ( ( real ) ( complex real ext-real ) number ) = x : ( ( real ) ( complex real ext-real ) number ) + (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) : ( ( ) ( complex real ext-real ) set ) & Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,a : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) holds
( x : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & (((a : ( ( real ) ( complex real ext-real ) number ) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (b : ( ( real ) ( complex real ext-real ) number ) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) - (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) ;

theorem :: POLYEQ_2:3
for a, b, c, x, y being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & ((b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (8 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) > 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & y : ( ( real ) ( complex real ext-real ) number ) = x : ( ( real ) ( complex real ext-real ) number ) + (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) : ( ( ) ( complex real ext-real ) set ) & Polynom (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ,a : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) holds
for y1, y2 being ( ( real ) ( complex real ext-real ) number ) st y1 : ( ( real ) ( complex real ext-real ) number ) = ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) + (sqrt (((b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (8 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) & y2 : ( ( real ) ( complex real ext-real ) number ) = ((- b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) - (sqrt (((b : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) - ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * c : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (8 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / (2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) holds
( x : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & ( x : ( ( real ) ( complex real ext-real ) number ) = (y1 : ( ( real ) ( complex real ext-real ) number ) + (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y1 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) or x : ( ( real ) ( complex real ext-real ) number ) = (y2 : ( ( real ) ( complex real ext-real ) number ) + (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) or x : ( ( real ) ( complex real ext-real ) number ) = (y1 : ( ( real ) ( complex real ext-real ) number ) - (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y1 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) or x : ( ( real ) ( complex real ext-real ) number ) = (y2 : ( ( real ) ( complex real ext-real ) number ) - (sqrt (delta (1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ,(- y2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( complex ) ( complex real ext-real ) set ) ,1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) )) : ( ( ) ( complex real ext-real ) set ) ) : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) / 2 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) ) ) ;

theorem :: POLYEQ_2:4
for x being ( ( real ) ( complex real ext-real ) number ) holds
( x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) set ) = (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) set ) & (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) = x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_2:5
for x, y being ( ( real ) ( complex real ext-real ) number ) st x : ( ( real ) ( complex real ext-real ) number ) + y : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(x : ( ( real ) ( complex real ext-real ) number ) + y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) set ) = ((((x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) + (((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (y : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + ((((x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) + (((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (y : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_2:6
for x, y being ( ( real ) ( complex real ext-real ) number ) st x : ( ( real ) ( complex real ext-real ) number ) + y : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(x : ( ( real ) ( complex real ext-real ) number ) + y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) set ) = ((x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) + ((((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((6 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) * (y : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (y : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_2:7
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being ( ( real ) ( complex real ext-real ) number ) st ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a1 : ( ( real ) ( complex real ext-real ) number ) ,a2 : ( ( real ) ( complex real ext-real ) number ) ,a3 : ( ( real ) ( complex real ext-real ) number ) ,a4 : ( ( real ) ( complex real ext-real ) number ) ,a5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Polynom (b1 : ( ( real ) ( complex real ext-real ) number ) ,b2 : ( ( real ) ( complex real ext-real ) number ) ,b3 : ( ( real ) ( complex real ext-real ) number ) ,b4 : ( ( real ) ( complex real ext-real ) number ) ,b5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
( a5 : ( ( real ) ( complex real ext-real ) number ) = b5 : ( ( real ) ( complex real ext-real ) number ) & ((a1 : ( ( real ) ( complex real ext-real ) number ) - a2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + a3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) - a4 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = ((b1 : ( ( real ) ( complex real ext-real ) number ) - b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + b3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) - b4 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & ((a1 : ( ( real ) ( complex real ext-real ) number ) + a2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + a3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + a4 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = ((b1 : ( ( real ) ( complex real ext-real ) number ) + b2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + b3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + b4 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_2:8
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being ( ( real ) ( complex real ext-real ) number ) st ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a1 : ( ( real ) ( complex real ext-real ) number ) ,a2 : ( ( real ) ( complex real ext-real ) number ) ,a3 : ( ( real ) ( complex real ext-real ) number ) ,a4 : ( ( real ) ( complex real ext-real ) number ) ,a5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Polynom (b1 : ( ( real ) ( complex real ext-real ) number ) ,b2 : ( ( real ) ( complex real ext-real ) number ) ,b3 : ( ( real ) ( complex real ext-real ) number ) ,b4 : ( ( real ) ( complex real ext-real ) number ) ,b5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
( a1 : ( ( real ) ( complex real ext-real ) number ) - b1 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = b3 : ( ( real ) ( complex real ext-real ) number ) - a3 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & a2 : ( ( real ) ( complex real ext-real ) number ) - b2 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = b4 : ( ( real ) ( complex real ext-real ) number ) - a4 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_2:9
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being ( ( real ) ( complex real ext-real ) number ) st ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a1 : ( ( real ) ( complex real ext-real ) number ) ,a2 : ( ( real ) ( complex real ext-real ) number ) ,a3 : ( ( real ) ( complex real ext-real ) number ) ,a4 : ( ( real ) ( complex real ext-real ) number ) ,a5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Polynom (b1 : ( ( real ) ( complex real ext-real ) number ) ,b2 : ( ( real ) ( complex real ext-real ) number ) ,b3 : ( ( real ) ( complex real ext-real ) number ) ,b4 : ( ( real ) ( complex real ext-real ) number ) ,b5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
( a1 : ( ( real ) ( complex real ext-real ) number ) = b1 : ( ( real ) ( complex real ext-real ) number ) & a2 : ( ( real ) ( complex real ext-real ) number ) = b2 : ( ( real ) ( complex real ext-real ) number ) & a3 : ( ( real ) ( complex real ext-real ) number ) = b3 : ( ( real ) ( complex real ext-real ) number ) & a4 : ( ( real ) ( complex real ext-real ) number ) = b4 : ( ( real ) ( complex real ext-real ) number ) & a5 : ( ( real ) ( complex real ext-real ) number ) = b5 : ( ( real ) ( complex real ext-real ) number ) ) ;

definition
let a1, x1, x2, x3, x4, x be ( ( real ) ( complex real ext-real ) number ) ;
func Four0 (a1,x1,x2,x3,x4,x) -> ( ( ) ( ) set ) equals :: POLYEQ_2:def 2
a1 : ( ( real ) ( complex real ext-real ) set ) * ((((x : ( ( real ) ( complex real ext-real ) set ) - x1 : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) set ) - x2 : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) set ) - x3 : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) set ) - x4 : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ;
end;

registration
let a1, x1, x2, x3, x4, x be ( ( real ) ( complex real ext-real ) number ) ;
cluster Four0 (a1 : ( ( real ) ( complex real ext-real ) set ) ,x1 : ( ( real ) ( complex real ext-real ) set ) ,x2 : ( ( real ) ( complex real ext-real ) set ) ,x3 : ( ( real ) ( complex real ext-real ) set ) ,x4 : ( ( real ) ( complex real ext-real ) set ) ,x : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( ) set ) -> real ;
end;

theorem :: POLYEQ_2:10
for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being ( ( real ) ( complex real ext-real ) number ) st a1 : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a1 : ( ( real ) ( complex real ext-real ) number ) ,a2 : ( ( real ) ( complex real ext-real ) number ) ,a3 : ( ( real ) ( complex real ext-real ) number ) ,a4 : ( ( real ) ( complex real ext-real ) number ) ,a5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Four0 (a1 : ( ( real ) ( complex real ext-real ) number ) ,x1 : ( ( real ) ( complex real ext-real ) number ) ,x2 : ( ( real ) ( complex real ext-real ) number ) ,x3 : ( ( real ) ( complex real ext-real ) number ) ,x4 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
(((((a1 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a2 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a3 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a4 : ( ( real ) ( complex real ext-real ) number ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + a5 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) / a1 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) = (((((x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (((x1 : ( ( real ) ( complex real ext-real ) number ) + x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * ((x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((((x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - ((((x : ( ( real ) ( complex real ext-real ) number ) - x1 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) - x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) - x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_2:11
for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being ( ( real ) ( complex real ext-real ) number ) st a1 : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a1 : ( ( real ) ( complex real ext-real ) number ) ,a2 : ( ( real ) ( complex real ext-real ) number ) ,a3 : ( ( real ) ( complex real ext-real ) number ) ,a4 : ( ( real ) ( complex real ext-real ) number ) ,a5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Four0 (a1 : ( ( real ) ( complex real ext-real ) number ) ,x1 : ( ( real ) ( complex real ext-real ) number ) ,x2 : ( ( real ) ( complex real ext-real ) number ) ,x3 : ( ( real ) ( complex real ext-real ) number ) ,x4 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
(((((a1 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a2 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a3 : ( ( real ) ( complex real ext-real ) number ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (a4 : ( ( real ) ( complex real ext-real ) number ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + a5 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) / a1 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) = ((((x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) - ((((x1 : ( ( real ) ( complex real ext-real ) number ) + x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x2 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x3 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * (x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - ((((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ;

theorem :: POLYEQ_2:12
for a1, a2, a3, a4, a5, x1, x2, x3, x4 being ( ( real ) ( complex real ext-real ) number ) st a1 : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & ( for x being ( ( real ) ( complex real ext-real ) number ) holds Polynom (a1 : ( ( real ) ( complex real ext-real ) number ) ,a2 : ( ( real ) ( complex real ext-real ) number ) ,a3 : ( ( real ) ( complex real ext-real ) number ) ,a4 : ( ( real ) ( complex real ext-real ) number ) ,a5 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) = Four0 (a1 : ( ( real ) ( complex real ext-real ) number ) ,x1 : ( ( real ) ( complex real ext-real ) number ) ,x2 : ( ( real ) ( complex real ext-real ) number ) ,x3 : ( ( real ) ( complex real ext-real ) number ) ,x4 : ( ( real ) ( complex real ext-real ) number ) ,x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) holds
( a2 : ( ( real ) ( complex real ext-real ) number ) / a1 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) = - (((x1 : ( ( real ) ( complex real ext-real ) number ) + x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & a3 : ( ( real ) ( complex real ext-real ) number ) / a1 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) = ((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x1 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (x2 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + (x3 : ( ( real ) ( complex real ext-real ) number ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) & a4 : ( ( real ) ( complex real ext-real ) number ) / a1 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) = - (((((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x1 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((x2 : ( ( real ) ( complex real ext-real ) number ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & a5 : ( ( real ) ( complex real ext-real ) number ) / a1 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) M2( COMPLEX : ( ( ) ( V33() V39() ) set ) )) = ((x1 : ( ( real ) ( complex real ext-real ) number ) * x2 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x3 : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x4 : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: POLYEQ_2:13
for a, k, y being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) & ( for x being ( ( real ) ( complex real ext-real ) number ) holds (x : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) + (a : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) = ((k : ( ( real ) ( complex real ext-real ) number ) * a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * x : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * ((x : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) + (a : ( ( real ) ( complex real ext-real ) number ) ^2) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ) holds
(((y : ( ( real ) ( complex real ext-real ) number ) |^ 4 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) - (k : ( ( real ) ( complex real ext-real ) number ) * (y : ( ( real ) ( complex real ext-real ) number ) |^ 3 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - (k : ( ( real ) ( complex real ext-real ) number ) * y : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + 1 : ( ( ) ( non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() ) M3( REAL : ( ( ) ( V33() V34() V35() V39() ) set ) , NAT : ( ( ) ( V33() V34() V35() V36() V37() V38() V39() ) M2(K6(REAL : ( ( ) ( V33() V34() V35() V39() ) set ) ) : ( ( ) ( ) set ) )) )) ;