let k be Nat; :: thesis: k --> 0 is dominated_by_0
A1: dom (k --> 0 ) = k by FUNCOP_1:19;
( 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 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 A1, Lm1;
Sum (n --> 0 ) = 0 * n by AFINSQ_2:70;
hence 2 * (Sum ((k --> 0 ) | n)) <= n by A2; :: thesis: verum