dom (F ^^ G) = (dom F) /\ (dom G) by Def2M
.= (Seg (len F)) /\ (dom G) by FINSEQ_1:def 3
.= (Seg (len F)) /\ (Seg (len G)) by FINSEQ_1:def 3
.= Seg (min (len F),(len G)) by FINSEQ_2:2 ;
hence F ^^ G is FinSequence-yielding FinSequence by FINSEQ_1:def 2; :: thesis: verum