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