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

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