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

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