let a, b be real number ; :: thesis: for n being natural number st 0 <= a & a < b & 1 <= n holds
a |^ n < b |^ n
let n be natural number ; :: thesis: ( 0 <= a & a < b & 1 <= n implies a |^ n < b |^ n )
assume that
A1: 0 <= a and
A2: a < b and
A3: 1 <= n ; :: thesis: a |^ n < b |^ n

per cases ( a > 0 or a = 0 ) by A1;

suppose a > 0 ; :: thesis: a |^ n < b |^ n

hence a |^ n < b |^ n by A2, A3, Lm1; :: thesis: verum

end;

suppose A4: a = 0 ; :: thesis: a |^ n < b |^ n

reconsider k = n, k1 = 1 as Integer ;
reconsider m = k - k1 as Element of NAT by A3, INT_1:18;
a |^ n = a |^ (m + 1)
.= (a |^ m) * (a |^ 1) by NEWTON:13
.= (a |^ m) * ((a GeoSeq ) . (0 + 1)) by Def1
.= (a |^ m) * (((a GeoSeq ) . 0 ) * 0 ) by A4, Th4
.= 0 ;
hence a |^ n < b |^ n by A1, A2, Th13; :: thesis: verum

end;

end;