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 ;
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 ;
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 ;
then A7: dom (f1 + f2) = Seg n1 by ;
min (n1,n2) = n1 by ;
hence len (f1 + f2) = min ((len f1),(len f2)) by ; :: thesis: verum
end;
case A8: n2 <= n1 ; :: thesis: len (f1 + f2) = min ((len f1),(len f2))
then dom f2 c= dom f1 by ;
then A9: dom (f1 + f2) = Seg n2 by ;
min (n1,n2) = n2 by ;
hence len (f1 + f2) = min ((len f1),(len f2)) by ; :: thesis: verum
end;
end;
end;
hence len (f1 + f2) = min ((len f1),(len f2)) ; :: thesis: verum