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