theorem split1: :: FIELD_15:49

for F being Field
for n being non zero Nat
for a, b being Element of F holds
( b is_a_root_of X^ (n,a) iff b |^ n = a )