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