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