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