A5: n in NAT by ORDINAL1:def 13;
A6: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
( len f = n & len g = n ) by FINSEQ_1:def 18;
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 FINSEQ_1:def 18 :: thesis: verum