take s ; :: thesis: ex N being increasing sequence of NAT st s = s * N
reconsider N = id NAT as increasing sequence of NAT ;
take N ; :: thesis: s = s * N
thus s = s * N by FUNCT_2:23; :: thesis: verum