let n be Element of NAT ; :: thesis: for x being real number st abs x <= 1 holds
abs (x |^ n) <= 1
let x be real number ; :: thesis: ( abs x <= 1 implies abs (x |^ n) <= 1 )
defpred S₁[ Element of NAT ] means abs (x |^ $1) <= 1;
assume A1: abs x <= 1 ; :: thesis: abs (x |^ n) <= 1
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] )
A3: abs (x |^ (k + 1)) = abs ((x |^ k) * x) by NEWTON:11
.= (abs (x |^ k)) * (abs x) by COMPLEX1:151 ;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A1, A3, COMPLEX1:132, XREAL_1:162; :: thesis: verum

end;

abs (x |^ 0) = abs 1 by NEWTON:9
.= 1 by ABSVALUE:def 1 ;
then A4: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A2);
hence abs (x |^ n) <= 1 ; :: thesis: verum