let k be Nat; :: thesis: for p being XFinSequence of NAT st rng p c= {0,1} & (2 * k) + 1 = min* { N where N is Nat : 2 * (Sum (p | N)) > N } holds
p | (2 * k) is dominated_by_0
let p be XFinSequence of NAT ; :: thesis: ( rng p c= {0,1} & (2 * k) + 1 = min* { N where N is Nat : 2 * (Sum (p | N)) > N } implies p | (2 * k) is dominated_by_0 )
set M = { N where N is Nat : 2 * (Sum (p | N)) > N } ;
set q = p | (2 * k);
assume that
A1: rng p c= {0,1} and
A2: (2 * k) + 1 = min* { N where N is Nat : 2 * (Sum (p | N)) > N } ; :: thesis: p | (2 * k) is dominated_by_0
thus rng (p | (2 * k)) c= {0,1} by A1; :: according to CATALAN2:def 1 :: thesis: for k being Nat st k <= dom (p | (2 * k)) holds
2 * (Sum ((p | (2 * k)) | k)) <= k
reconsider M = { N where N is Nat : 2 * (Sum (p | N)) > N } as non empty Subset of NAT by A2, NAT_1:def 1;
let m be Nat; :: thesis: ( m <= dom (p | (2 * k)) implies 2 * (Sum ((p | (2 * k)) | m)) <= m )
assume A3: m <= dom (p | (2 * k)) ; :: thesis: 2 * (Sum ((p | (2 * k)) | m)) <= m
then A4: Segm m c= Segm (len (p | (2 * k))) by NAT_1:39;
len (p | (2 * k)) <= 2 * k by AFINSQ_1:55;
then Segm (len (p | (2 * k))) c= Segm (2 * k) by NAT_1:39;
then Segm m c= Segm (2 * k) by A4;
then m <= 2 * k by NAT_1:39;
then A5: m < (2 * k) + 1 by NAT_1:13;
assume A6: 2 * (Sum ((p | (2 * k)) | m)) > m ; :: thesis: contradiction
reconsider m = m as Element of NAT by ORDINAL1:def 12;
( (p | (2 * k)) | m = p | m & m in NAT ) by A4, RELAT_1:74, XBOOLE_1:1, A3;
then m in M by A6;
hence contradiction by A2, A5, NAT_1:def 1; :: thesis: verum