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