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