set N = (id NAT) ^\ k;
(id NAT) ^\ k is increasing
proof
let e1 be ExtReal; :: according to VALUED_0:def 13 :: thesis: for e2 being ExtReal 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 ExtReal; :: 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 ;
reconsider jk = j + k, ik = i + k as Element of NAT by ORDINAL1:def 12;
A1: ((id NAT) ^\ k) . j = (id NAT) . jk by NAT_1:def 3
.= jk ;
assume A2: e1 < e2 ; :: thesis: ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2
((id NAT) ^\ k) . i = (id NAT) . ik by NAT_1:def 3
.= ik ;
hence ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 by A1, A2, XREAL_1:6; :: thesis: verum
end;
then reconsider N = (id NAT) ^\ k as increasing sequence of NAT ;
thus s ^\ k is subsequence of s :: thesis: verum
proof
take N ; :: according to VALUED_0:def 17 :: thesis: s ^\ k = s * N
thus s ^\ k = (s * (id NAT)) ^\ k by FUNCT_2:17
.= s * N by NAT_1:50 ; :: thesis: verum
end;