set l = min ((len f),(len g));
A1: ( 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 Lm13;
then len h = ll by FINSEQ_1:def 3;
hence <:f,g:> is m -element by CARD_1:def 7, A1; :: thesis: verum