set l = min ((len f),(len g));
Z1: ( len f = m & len g = m ) by CARD_1:def 7;
reconsider h = <:f,g:> as FinSequence ;
reconsider ll = min ((len f),(len g)) as Element of NAT by ORDINAL1:def 12;
dom h = Seg ll by Lm27;
then len h = ll by FINSEQ_1:def 3;
hence <:f,g:> is m -element by Z1, CARD_1:def 7; :: thesis: verum