let k be Element of NAT ; :: thesis: k --> 0 is dominated_by_0
( rng (k --> 0 ) c= {0 } & {0 } c= {0 ,1} ) by FUNCOP_1:19, ZFMISC_1:12;
hence rng (k --> 0 ) c= {0 ,1} by XBOOLE_1:1; :: according to CATALAN2:def 1 :: thesis: for k being Element of NAT st k <= dom (k --> 0 ) holds
2 * (Sum ((k --> 0 ) | k)) <= k
let n be Element of NAT ; :: thesis: ( n <= dom (k --> 0 ) implies 2 * (Sum ((k --> 0 ) | n)) <= n )
assume A1: n <= dom (k --> 0 ) ; :: thesis: 2 * (Sum ((k --> 0 ) | n)) <= n
dom (k --> 0 ) = k by FUNCOP_1:19;
then ( (k --> 0 ) | n = n --> 0 & Sum (n --> 0 ) = 0 * n ) by A1, Lm1, Lm2;
hence 2 * (Sum ((k --> 0 ) | n)) <= n ; :: thesis: verum