A5: n in NAT by ORDINAL1:def 12;
A6: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
( len f = n & len g = n ) by CARD_1:def 7;
then ( dom f = Seg n & dom g = Seg n ) by FINSEQ_1:def 3;
hence len (f + g) = n by A5, A6, FINSEQ_1:def 3; :: according to CARD_1:def 7 :: thesis: verum