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