let n, m be Element of NAT ; :: thesis: ( n >= m implies (n --> 0 ) ^ (m --> 1) is dominated_by_0 )
assume A1: n >= m ; :: thesis: (n --> 0 ) ^ (m --> 1) is dominated_by_0
set p = (n --> 0 ) ^ (m --> 1);
thus rng ((n --> 0 ) ^ (m --> 1)) c= {0 ,1} :: according to CATALAN2:def 1 :: thesis: for k being Element of NAT st k <= dom ((n --> 0 ) ^ (m --> 1)) holds
2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k

proof

( rng (n --> 0 ) c= {0 } & rng (m --> 1) c= {1} & {0 } c= {0 ,1} & {1} c= {0 ,1} ) by FUNCOP_1:19, ZFMISC_1:12;
then ( rng (n --> 0 ) c= {0 ,1} & rng (m --> 1) c= {0 ,1} ) by XBOOLE_1:1;
then (rng (n --> 0 )) \/ (rng (m --> 1)) c= {0 ,1} by XBOOLE_1:8;
hence rng ((n --> 0 ) ^ (m --> 1)) c= {0 ,1} by AFINSQ_1:29; :: thesis: verum

end;

let k be Element of NAT ; :: thesis: ( k <= dom ((n --> 0 ) ^ (m --> 1)) implies 2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k )
assume A2: k <= dom ((n --> 0 ) ^ (m --> 1)) ; :: thesis: 2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k

now

per cases ( k <= dom (n --> 0 ) or k > dom (n --> 0 ) ) ;

suppose A3: k <= dom (n --> 0 ) ; :: thesis: 2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k

dom (n --> 0 ) = n by FUNCOP_1:19;
then ( ((n --> 0 ) ^ (m --> 1)) | k = (n --> 0 ) | k & (n --> 0 ) | k = k --> 0 & Sum (k --> 0 ) = 0 * k ) by A3, Lm1, Lm2, Th2;
hence 2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k ; :: thesis: verum

end;

suppose k > dom (n --> 0 ) ; :: thesis: 2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k

then reconsider kd = k - (dom (n --> 0 )) as Element of NAT by NAT_1:21;
dom ((n --> 0 ) ^ (m --> 1)) = len ((n --> 0 ) ^ (m --> 1)) ;
then k <= (len (n --> 0 )) + (len (m --> 1)) by A2, AFINSQ_1:20;
then ( k - (len (n --> 0 )) <= ((len (m --> 1)) + (len (n --> 0 ))) - (len (n --> 0 )) & dom (n --> 0 ) = len (n --> 0 ) ) by XREAL_1:11;
then ( kd <= len (m --> 1) & len (m --> 1) = dom (m --> 1) ) ;
then ( kd <= m & k = kd + (dom (n --> 0 )) ) by FUNCOP_1:19;
then ( ((n --> 0 ) ^ (m --> 1)) | k = (n --> 0 ) ^ ((m --> 1) | kd) & (m --> 1) | kd = kd --> 1 ) by Lm1, Th3;
then ( Sum (((n --> 0 ) ^ (m --> 1)) | k) = (Sum (n --> 0 )) + (Sum (kd --> 1)) & Sum (n --> 0 ) = n * 0 & Sum (kd --> 1) = kd * 1 ) by Lm2, Lm4;
then A4: ( Sum (((n --> 0 ) ^ (m --> 1)) | k) = kd & dom (n --> 0 ) = n & dom ((n --> 0 ) ^ (m --> 1)) = (len (n --> 0 )) + (len (m --> 1)) & len (n --> 0 ) = dom (n --> 0 ) & dom (n --> 0 ) = n & len (m --> 1) = dom (m --> 1) & dom (m --> 1) = m ) by AFINSQ_1:def 4, FUNCOP_1:19;
then k - n <= (m + n) - n by A2, XREAL_1:11;
then k - n <= n by A1, XXREAL_0:2;
then (k - n) + (k - n) <= n + (k - n) by XREAL_1:8;
hence 2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k by A4; :: thesis: verum

end;

end;

end;

hence 2 * (Sum (((n --> 0 ) ^ (m --> 1)) | k)) <= k ; :: thesis: verum