theorem Th76: :: POLYNOM9:76

for M being Jpolynom of 4, F_Complex ex K2 being INT -valued Polynomial of 6,F_Real st
( ( for f being Function of 6,F_Real st f . 5 <> 0 holds
eval (K2,f) = ((power F_Real) . ((f /. 5),8)) * (eval ((Jsqrt M),(@ <%((- (f . 0)) + ((f . 4) / (f . 5))),(f . 1),(f . 2),(f . 3)%>))) ) & ( for f being INT -valued Function of 6,F_Real st f . 5 <> 0 & eval (K2,f) = 0 holds
f . 5 divides f . 4 ) )