let a be Integer; :: thesis: for n being Nat holds (In (a,INT)) |^ n = (In (a,INT.Ring)) |^ n
let n be Nat; :: thesis: (In (a,INT)) |^ n = (In (a,INT.Ring)) |^ n
(In (a,INT)) |^ n = (In (a,INT.Ring)) |^ n

proof

defpred S₁[ Nat] means (In (a,INT)) |^ $1 = (In (a,INT.Ring)) |^ $1;
(In (a,INT.Ring)) |^ 0 = 1_ INT.Ring by BINOM:8;
then A1: S₁[ 0 ] by NEWTON:4;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then (In (a,INT)) |^ (k + 1) = (In (a,INT.Ring)) * ((In (a,INT.Ring)) |^ k) by NEWTON:6
.= ((In (a,INT.Ring)) |^ 1) * ((In (a,INT.Ring)) |^ k) by BINOM:8
.= (In (a,INT.Ring)) |^ (k + 1) by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (In (a,INT)) |^ n = (In (a,INT.Ring)) |^ n ; :: thesis: verum

end;

hence (In (a,INT)) |^ n = (In (a,INT.Ring)) |^ n ; :: thesis: verum