dom ((<*> NAT) mod n) = dom (<*> NAT) by EULER_2:def 1;
then len ((<*> NAT) mod n) = len (<*> NAT) by FINSEQ_3:29;
hence (<*> NAT) mod n = <*> NAT ; :: thesis: verum