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 )
assume A1: abs x <= 1 ; :: thesis: abs (x |^ n) <= 1
defpred S₁[ Element of NAT ] means abs (x |^ $1) <= 1;
for k being Element of NAT holds S₁[k]

proof

A2: S₁[ 0 ]

proof

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

end;

A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: abs (x |^ (k + 1)) = abs ((x |^ k) * x) by NEWTON:11
.= (abs (x |^ k)) * (abs x) by COMPLEX1:151 ;
A6: 0 <= abs x by COMPLEX1:132;
0 <= abs (x |^ k) by COMPLEX1:132;
hence S₁[k + 1] by A1, A4, A5, A6, XREAL_1:162; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3); :: thesis: verum

end;

hence abs (x |^ n) <= 1 ; :: thesis: verum