let x be Element of ExtREAL ; :: thesis: for y being Real
for k being Nat st x = y holds
x |^ k = y |^ k
let y be Real; :: thesis: for k being Nat st x = y holds
x |^ k = y |^ k
let k be Nat; :: thesis: ( x = y implies x |^ k = y |^ k )
defpred S₁[ Nat] means x |^ $1 = y |^ $1;
assume A1: x = y ; :: thesis: x |^ k = y |^ k
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

reconsider y1 = y as Element of REAL by XREAL_0:def 1;
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then (x |^ k) * x = (y |^ k) * y by A1, EXTREAL1:1;
then (x |^ k) * x = y |^ (k + 1) by NEWTON:6;
hence S₁[k + 1] by Th10; :: thesis: verum

end;

x |^ 0 = 1. by Th6, FINSEQ_2:58;
then A3: S₁[ 0 ] by NEWTON:4;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A2);
hence x |^ k = y |^ k ; :: thesis: verum