theorem :: POLYEQ_2:13

for a, k, y being Real st a <> 0 & ( for x being Real holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ) holds
(((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0