let k be Nat; :: thesis: k --> 0 is dominated_by_0
( rng (k --> 0) c= {0} & {0} c= {0,1} ) by FUNCOP_1:13, ZFMISC_1:7;
hence rng (k --> 0) c= {0,1} ; :: according to CATALAN2:def 1 :: thesis: for k being Nat st k <= dom (k --> 0) holds
2 * (Sum ((k --> 0) | k)) <= k
let n be Nat; :: thesis: ( n <= dom (k --> 0) implies 2 * (Sum ((k --> 0) | n)) <= n )
assume n <= dom (k --> 0) ; :: thesis: 2 * (Sum ((k --> 0) | n)) <= n
then A2: (k --> 0) | n = n --> 0 by Lm1;
Sum (n --> 0) = 0 * n by AFINSQ_2:58;
hence 2 * (Sum ((k --> 0) | n)) <= n by A2; :: thesis: verum