let f1, f2 be complex-valued FinSequence; :: thesis: len (f1 + f2) = min (len f1),(len f2)
set g = f1 + f2;
consider n1 being Nat such that
H1: dom f1 = Seg n1 by FINSEQ_1:def 2;
n1 in NAT by ORDINAL1:def 13;
then H1a: len f1 = n1 by H1, FINSEQ_1:def 3;
consider n2 being Nat such that
H2: dom f2 = Seg n2 by FINSEQ_1:def 2;
n2 in NAT by ORDINAL1:def 13;
then H2a: len f2 = n2 by H2, FINSEQ_1:def 3;
H3: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;

now

per cases ( n1 <= n2 or n2 <= n1 ) ;

case A: n1 <= n2 ; :: thesis: len (f1 + f2) = min (len f1),(len f2)

then dom f1 c= dom f2 by H1, H2, FINSEQ_1:7;
then B: dom (f1 + f2) = Seg n1 by H1, H3, XBOOLE_1:28;
min n1,n2 = n1 by A, XXREAL_0:def 9;
hence len (f1 + f2) = min (len f1),(len f2) by B, H1a, H2a, FINSEQ_1:def 3; :: thesis: verum

end;

case A: n2 <= n1 ; :: thesis: len (f1 + f2) = min (len f1),(len f2)

then dom f2 c= dom f1 by H1, H2, FINSEQ_1:7;
then B: dom (f1 + f2) = Seg n2 by H2, H3, XBOOLE_1:28;
min n1,n2 = n2 by A, XXREAL_0:def 9;
hence len (f1 + f2) = min (len f1),(len f2) by B, H1a, H2a, FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

hence len (f1 + f2) = min (len f1),(len f2) ; :: thesis: verum