A2: dom (c (#) f) = dom f by VALUED_1:def 5;
len f = n by CARD_1:def 13;
hence len (c (#) f) = n by A2, FINSEQ_3:31; :: according to CARD_1:def 13 :: thesis: verum