A1:
dom (c + f) = dom f
by VALUED_1:def 2;

len f = n by CARD_1:def 7;

hence len (c + f) = n by A1, FINSEQ_3:29; :: according to CARD_1:def 7 :: thesis: verum

len f = n by CARD_1:def 7;

hence len (c + f) = n by A1, FINSEQ_3:29; :: according to CARD_1:def 7 :: thesis: verum