theorem split2: :: FIELD_15:50
for F being Field
for E being FieldExtension of F
for n being non zero Nat
for a being Element of F
for b being Element of E st b = a holds
X^ (n,a) = X^ (n,b)