take <*> NAT ; :: thesis: <*> NAT is Cardinal-yielding
thus <*> NAT is Cardinal-yielding ; :: thesis: verum