let F be Field; :: thesis: 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)
let E be FieldExtension of F; :: thesis: 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)
let n be non zero Nat; :: thesis: for a being Element of F
for b being Element of E st b = a holds
X^ (n,a) = X^ (n,b)
let a be Element of F; :: thesis: for b being Element of E st b = a holds
X^ (n,a) = X^ (n,b)
let b be Element of E; :: thesis: ( b = a implies X^ (n,a) = X^ (n,b) )
assume AS: b = a ; :: thesis: X^ (n,a) = X^ (n,b)
H1: F is Subring of E by FIELD_4:def 1;
then H2: - b = - a by AS, FIELD_6:17;

now :: thesis: for i being Nat holds (X^ (n,a)) . i = (X^ (n,b)) . i

let i be Nat; :: thesis: (X^ (n,a)) . b₁ = (X^ (n,b)) . b₁

per cases ( i = 0 or i = n or ( i <> 0 & i <> n ) ) ;

suppose A: i = 0 ; :: thesis: (X^ (n,a)) . b₁ = (X^ (n,b)) . b₁

hence (X^ (n,a)) . i = - b by H2, Lm10
.= (X^ (n,b)) . i by A, Lm10 ;
:: thesis: verum

end;

suppose A: i = n ; :: thesis: (X^ (n,a)) . b₁ = (X^ (n,b)) . b₁

hence (X^ (n,a)) . i = 1. F by Lm10
.= 1. E by H1, C0SP1:def 3
.= (X^ (n,b)) . i by A, Lm10 ;
:: thesis: verum

end;

suppose A: ( i <> 0 & i <> n ) ; :: thesis: (X^ (n,a)) . b₁ = (X^ (n,b)) . b₁

hence (X^ (n,a)) . i = 0. F by Lm11
.= 0. E by H1, C0SP1:def 3
.= (X^ (n,b)) . i by A, Lm11 ;
:: thesis: verum

end;

end;

end;

hence X^ (n,a) = X^ (n,b) ; :: thesis: verum