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