let x be Element of ExtREAL ; :: thesis: for y being real number
for k being natural number st x = y holds
x |^ k = y |^ k
let y be real number ; :: thesis: for k being natural number st x = y holds
x |^ k = y |^ k
let k be natural number ; :: thesis: ( x = y implies x |^ k = y |^ k )
assume A1: x = y ; :: thesis: x |^ k = y |^ k
defpred S₁[ natural number ] means x |^ $1 = y |^ $1;
x |^ 0 = 1. by Th6, FINSEQ_2:72;
then A2: S₁[ 0 ] by NEWTON:9;
A3: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

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

end;

for k being natural number holds S₁[k] from NAT_1:sch 2(A2, A3);
hence x |^ k = y |^ k ; :: thesis: verum