A2: dom (f ") = dom f by VALUED_1:def 7;
len f = n by CARD_1:def 7;
hence len (f ") = n by A2, FINSEQ_3:29; :: according to CARD_1:def 7 :: thesis: verum