A7: n in NAT by ORDINAL1:def 13;
A8: dom (f (#) g) = (dom f) /\ (dom g) by VALUED_1:def 4;
( 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 A7, A8, FINSEQ_1:def 3; :: according to FINSEQ_1:def 18 :: thesis: verum