RAT 0 = {(<*> RAT)} by FINSEQ_2:94
.= {{}} ;
hence RAT 0 = {0} ; :: thesis: verum