let R be non degenerated comRing; :: thesis: for S being comRingExtension of R
for a being Element of R
for b being Element of S
for n being Element of NAT st a = b holds
(X- b) `^ n = (X- a) `^ n
let S be comRingExtension of R; :: thesis: for a being Element of R
for b being Element of S
for n being Element of NAT st a = b holds
(X- b) `^ n = (X- a) `^ n
let a be Element of R; :: thesis: for b being Element of S
for n being Element of NAT st a = b holds
(X- b) `^ n = (X- a) `^ n
let b be Element of S; :: thesis: for n being Element of NAT st a = b holds
(X- b) `^ n = (X- a) `^ n
let n be Element of NAT ; :: thesis: ( a = b implies (X- b) `^ n = (X- a) `^ n )
assume AS: a = b ; :: thesis: (X- b) `^ n = (X- a) `^ n
defpred S₁[ Nat] means (X- b) `^ $1 = (X- a) `^ $1;
(X- b) `^ 0 = 1_. S by POLYNOM5:15
.= 1_. R by FIELD_4:14
.= (X- a) `^ 0 by POLYNOM5:15 ;
then IA: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then H: ( (X- a) `^ k = (X- b) `^ k & X- b = X- a ) by AS, FIELD_4:21;
(X- b) `^ (k + 1) = ((X- b) `^ k) *' (X- b) by POLYNOM5:19
.= ((X- a) `^ k) *' (X- a) by H, FIELD_4:17
.= (X- a) `^ (k + 1) by POLYNOM5:19 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence (X- b) `^ n = (X- a) `^ n ; :: thesis: verum