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:12;
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