theorem Th4: :: POLYEQ_2:4
for x being Real holds
( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 )