let k be Element of NAT ; :: thesis: for p being XFinSequence of st rng p c= {0 ,1} & not p is dominated_by_0 & (2 * k) + 1 = min* { n where n is Element of NAT : 2 * (Sum (p | n)) > n } holds
p | (2 * k) is dominated_by_0
let p be XFinSequence of ; :: thesis: ( rng p c= {0 ,1} & not p is dominated_by_0 & (2 * k) + 1 = min* { n where n is Element of NAT : 2 * (Sum (p | n)) > n } implies p | (2 * k) is dominated_by_0 )
set M = { n where n is Element of NAT : 2 * (Sum (p | n)) > n } ;
set q = p | (2 * k);
assume A1: ( rng p c= {0 ,1} & not p is dominated_by_0 & (2 * k) + 1 = min* { n where n is Element of NAT : 2 * (Sum (p | n)) > n } ) ; :: thesis: p | (2 * k) is dominated_by_0
then reconsider M = { n where n is Element of NAT : 2 * (Sum (p | n)) > n } as non empty Subset of NAT by NAT_1:def 1;
rng (p | (2 * k)) c= rng p by RELAT_1:99;
hence rng (p | (2 * k)) c= {0 ,1} by A1, XBOOLE_1:1; :: according to CATALAN2:def 1 :: thesis: for k being Element of NAT st k <= dom (p | (2 * k)) holds
2 * (Sum ((p | (2 * k)) | k)) <= k
let m be Element of NAT ; :: thesis: ( m <= dom (p | (2 * k)) implies 2 * (Sum ((p | (2 * k)) | m)) <= m )
assume A2: m <= dom (p | (2 * k)) ; :: thesis: 2 * (Sum ((p | (2 * k)) | m)) <= m
assume A3: 2 * (Sum ((p | (2 * k)) | m)) > m ; :: thesis: contradiction
( m c= dom (p | (2 * k)) & dom (p | (2 * k)) c= 2 * k ) by A2, NAT_1:40, RELAT_1:87;
then m c= 2 * k by XBOOLE_1:1;
then ( (p | (2 * k)) | m = p | m & m <= 2 * k & 2 * k < (2 * k) + 1 ) by NAT_1:13, NAT_1:40, RELAT_1:103;
then ( m in M & m < (2 * k) + 1 ) by A3, XXREAL_0:2;
hence contradiction by A1, NAT_1:def 1; :: thesis: verum