card (dom f) = card (dom (Shift (f,n))) by CARD_1:5, VALUED_1:27
.= card (Shift (f,n)) by CARD_1:62 ;
hence Shift (f,n) is len f -element by CARD_1:def 7; :: thesis: verum