let m be positive Nat; :: thesis: for n being Nat
for m0 being Element of F_Real st m = m0 holds
m |^ n = m0 |^ n
let n be Nat; :: thesis: for m0 being Element of F_Real st m = m0 holds
m |^ n = m0 |^ n
let m0 be Element of F_Real; :: thesis: ( m = m0 implies m |^ n = m0 |^ n )
assume A1: m = m0 ; :: thesis: m |^ n = m0 |^ n
defpred S₁[ Nat] means m |^ $1 = m0 |^ $1;
m |^ 0 = 1_ F_Real by NEWTON:4;
then A2: S₁[ 0 ] by BINOM:8;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then m |^ (n + 1) = m0 * (m0 |^ n) by A1, NEWTON:6
.= (m0 |^ 1) * (m0 |^ n) by BINOM:8 ;
hence S₁[n + 1] by BINOM:10; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence m |^ n = m0 |^ n ; :: thesis: verum