let f, g be FinSequence; :: thesis: dom <:f,g:> = Seg (min ((len f),(len g)))
set m = len f;
set n = len g;
set l = min ((len f),(len g));
thus dom <:f,g:> = (dom f) /\ (dom g) by FUNCT_3:def 7
.= (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 ; :: thesis: verum