dom (f +* (x,y)) = dom f by FUNCT_7:30;
hence len (f +* (x,y)) = len f by FINSEQ_3:29
.= n by CARD_1:def 7 ;
:: according to CARD_1:def 7 :: thesis: verum