dom (F ^^ G) = (dom F) /\ (dom G) by Def4
.= (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-like by FINSEQ_1:def 2; :: thesis: verum