let k be Nat; :: thesis: for p being XFinSequence of st rng p c= {0,1} & (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} & (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 that
A1: rng p c= {0,1} and
A2: (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } ; :: thesis: p | (2 * k) is dominated_by_0
rng (p | (2 * k)) c= rng p by RELAT_1:70;
hence rng (p | (2 * k)) c= {0,1} by A1, XBOOLE_1:1; :: 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 Element of 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 m <= dom (p | (2 * k)) ; :: thesis: 2 * (Sum ((p | (2 * k)) | m)) <= m
then A3: m c= dom (p | (2 * k)) by NAT_1:39;
A4: dom (p | (2 * k)) c= 2 * k by RELAT_1:58;
then m c= 2 * k by A3, XBOOLE_1:1;
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 A3, A4, RELAT_1:74, XBOOLE_1:1;
then m in M by A6;
hence contradiction by A2, A5, NAT_1:def 1; :: thesis: verum