set m = len f;
set n = len g;
set l = min ((len f),(len g));
dom <:f,g:> = Seg (min ((len f),(len g))) by Lm13;
hence <:f,g:> is FinSequence-like ; :: thesis: verum