set N = (id NAT ) ^\ k;
(id NAT ) ^\ k is increasing

proof

let e1 be ext-real number ; :: according to VALUED_0:def 13 :: thesis: for e2 being ext-real number st e1 in dom ((id NAT ) ^\ k) & e2 in dom ((id NAT ) ^\ k) & e1 < e2 holds
((id NAT ) ^\ k) . e1 < ((id NAT ) ^\ k) . e2
let e2 be ext-real number ; :: thesis: ( e1 in dom ((id NAT ) ^\ k) & e2 in dom ((id NAT ) ^\ k) & e1 < e2 implies ((id NAT ) ^\ k) . e1 < ((id NAT ) ^\ k) . e2 )
assume ( e1 in dom ((id NAT ) ^\ k) & e2 in dom ((id NAT ) ^\ k) ) ; :: thesis: ( not e1 < e2 or ((id NAT ) ^\ k) . e1 < ((id NAT ) ^\ k) . e2 )
then reconsider i = e1, j = e2 as Element of NAT ;
A: ((id NAT ) ^\ k) . i = (id NAT ) . (i + k) by NAT_1:def 3
.= i + k by FUNCT_1:35 ;
B: ((id NAT ) ^\ k) . j = (id NAT ) . (j + k) by NAT_1:def 3
.= j + k by FUNCT_1:35 ;
assume e1 < e2 ; :: thesis: ((id NAT ) ^\ k) . e1 < ((id NAT ) ^\ k) . e2
hence ((id NAT ) ^\ k) . e1 < ((id NAT ) ^\ k) . e2 by A, B, XREAL_1:8; :: thesis: verum

end;

then reconsider N = (id NAT ) ^\ k as increasing sequence of NAT ;
take N ; :: according to VALUED_0:def 17 :: thesis: s ^\ k = s * N
thus s ^\ k = (s * (id NAT )) ^\ k by FUNCT_2:23
.= s * N by NAT_1:51 ; :: thesis: verum