let f1, f2 be complex-valued FinSequence; 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 ( ( 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
;
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;
verum end; case A8:
n2 <= n1
;
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;
verum end; end; end;
hence
len (f1 + f2) = min ((len f1),(len f2))
; verum