let n be non trivial Nat; :: thesis: for R being Ring
for S being RingExtension of R holds X^ (n,R) = X^ (n,S)
let F be Ring; :: thesis: for S being RingExtension of F holds X^ (n,F) = X^ (n,S)
let E be RingExtension of F; :: thesis: X^ (n,F) = X^ (n,E)
set q = X^ (n,F);
set r = X^ (n,E);
H1: F is Subring of E by FIELD_4:def 1;
then H2: 1. E = 1. F by C0SP1:def 3;

now :: thesis: for o being object st o in NAT holds
(X^ (n,F)) . o = (X^ (n,E)) . o

let o be object ; :: thesis: ( o in NAT implies (X^ (n,F)) . b₁ = (X^ (n,E)) . b₁ )
assume o in NAT ; :: thesis: (X^ (n,F)) . b₁ = (X^ (n,E)) . b₁
then reconsider m = o as Nat ;

per cases ( m = 1 or m = n or ( m <> 1 & m <> n ) ) ;

suppose A: m = 1 ; :: thesis: (X^ (n,F)) . b₁ = (X^ (n,E)) . b₁

then (X^ (n,F)) . m = - (1. F) by Lm10
.= - (1. E) by H1, H2, FIELD_6:17
.= (X^ (n,E)) . m by A, Lm10 ;
hence (X^ (n,F)) . o = (X^ (n,E)) . o ; :: thesis: verum

end;

suppose A: m = n ; :: thesis: (X^ (n,F)) . b₁ = (X^ (n,E)) . b₁

then (X^ (n,F)) . m = 1. F by Lm10
.= 1. E by H1, C0SP1:def 3
.= (X^ (n,E)) . m by A, Lm10 ;
hence (X^ (n,F)) . o = (X^ (n,E)) . o ; :: thesis: verum

end;

suppose A: ( m <> 1 & m <> n ) ; :: thesis: (X^ (n,F)) . b₁ = (X^ (n,E)) . b₁

then (X^ (n,F)) . m = 0. F by Lm11
.= 0. E by H1, C0SP1:def 3
.= (X^ (n,E)) . m by A, Lm11 ;
hence (X^ (n,F)) . o = (X^ (n,E)) . o ; :: thesis: verum

end;

end;

end;

hence X^ (n,F) = X^ (n,E) ; :: thesis: verum