set q = m --> 1;
assume A1: Domin_0 (n,m) is empty ; :: thesis: 2 * m > n
assume A2: 2 * m <= n ; :: thesis: contradiction
m <= m + m by NAT_1:12;
then reconsider nm = n - m as Nat by A2, NAT_1:21, XXREAL_0:2;
set p = nm --> 0;
(2 * m) - m <= nm by A2, XREAL_1:9;
then A3: (nm --> 0) ^ (m --> 1) is dominated_by_0 by Th5;
( dom ((nm --> 0) ^ (m --> 1)) = (len (nm --> 0)) + (len (m --> 1)) & dom (nm --> 0) = nm ) by AFINSQ_1:def 3;
then A4: dom ((nm --> 0) ^ (m --> 1)) = nm + m ;
A5: Sum ((nm --> 0) ^ (m --> 1)) = (Sum (nm --> 0)) + (Sum (m --> 1)) by AFINSQ_2:55;
( Sum (nm --> 0) = 0 * nm & Sum (m --> 1) = 1 * m ) by AFINSQ_2:58;
hence contradiction by A1, A5, A4, A3, Def2; :: thesis: verum