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
A1: dom f1 = Seg n1 by FINSEQ_1:def 2;
n1 in NAT by ORDINAL1:def 12;
then A2: len f1 = n1 by A1, FINSEQ_1:def 3;
consider n2 being Nat such that
A3: dom f2 = Seg n2 by FINSEQ_1:def 2;
n2 in NAT by ORDINAL1:def 12;
then A4: len f2 = n2 by A3, FINSEQ_1:def 3;
A5: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;

now :: thesis: ( ( n1 <= n2 & len (f1 + f2) = min ((len f1),(len f2)) ) or ( n2 <= n1 & len (f1 + f2) = min ((len f1),(len f2)) ) )

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

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

then dom f1 c= dom f2 by A1, A3, FINSEQ_1:5;
then A7: dom (f1 + f2) = Seg n1 by A1, A5, XBOOLE_1:28;
min (n1,n2) = n1 by A6, XXREAL_0:def 9;
hence len (f1 + f2) = min ((len f1),(len f2)) by A2, A4, A7, FINSEQ_1:def 3; :: thesis: verum

end;

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

then dom f2 c= dom f1 by A1, A3, FINSEQ_1:5;
then A9: dom (f1 + f2) = Seg n2 by A3, A5, XBOOLE_1:28;
min (n1,n2) = n2 by A8, XXREAL_0:def 9;
hence len (f1 + f2) = min ((len f1),(len f2)) by A2, A4, A9, FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

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