A1: dom (- f) = dom f by VALUED_1:8;
len f = n by FINSEQ_1:def 18;
hence len (- f) = n by A1, FINSEQ_3:31; :: according to FINSEQ_1:def 18 :: thesis: verum