reconsider N = id NAT as increasing sequence of NAT ;
take s ; :: thesis: ex N being increasing sequence of NAT st s = s * N
take N ; :: thesis: s = s * N
dom s = NAT by PARTFUN1:def 2;
hence s = s * N by RELAT_1:52; :: thesis: verum