let x be Real; :: thesis: for n being Element of NAT holds abs (x |^ n) = (abs x) |^ n
let n be Element of NAT ; :: thesis: abs (x |^ n) = (abs x) |^ n
defpred S₁[ Element of NAT ] means abs (x |^ $1) = (abs x) |^ $1;
A1: S₁[ 0 ]

proof

abs (x |^ 0 ) = abs 1 by NEWTON:9
.= 1 by ABSVALUE:def 1 ;
hence S₁[ 0 ] by NEWTON:9; :: thesis: verum

end;

A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
abs (x |^ (k + 1)) = abs (x * (x |^ k)) by NEWTON:11
.= (abs x) * (abs (x |^ k)) by COMPLEX1:151
.= (abs x) |^ (k + 1) by A3, NEWTON:11 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence abs (x |^ n) = (abs x) |^ n ; :: thesis: verum