A1: ( len f = n & len g = m ) by CARD_1:def 7;
reconsider f = f as FinSequence of COMPLEX by NEWTON02:103;
reconsider g = g as FinSequence of COMPLEX by NEWTON02:103;
len (f + g) = min ((len f),(len g)) by NEWTON04:23;
hence f + g is min (n,m) -element by A1, CARD_1:def 7; :: thesis: verum