let k be Element of NAT ; :: thesis: for p, q being XFinSequence of st p is dominated_by_0 & 2 * (Sum (p | k)) = k & p = (p | k) ^ q holds
q is dominated_by_0
let p, q be XFinSequence of ; :: thesis: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k & p = (p | k) ^ q implies q is dominated_by_0 )
assume A1: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k & p = (p | k) ^ q ) ; :: thesis: q is dominated_by_0
then ( rng q c= rng p & rng p c= {0 ,1} ) by Def1, AFINSQ_1:28;
hence rng q c= {0 ,1} by XBOOLE_1:1; :: according to CATALAN2:def 1 :: thesis: for k being Element of NAT st k <= dom q holds
2 * (Sum (q | k)) <= k
let n be Element of NAT ; :: thesis: ( n <= dom q implies 2 * (Sum (q | n)) <= n )
assume n <= dom q ; :: thesis: 2 * (Sum (q | n)) <= n
p | ((len (p | k)) + n) = (p | k) ^ (q | n) by A1, Th3;
then ( 2 * (Sum (p | ((len (p | k)) + n))) <= (len (p | k)) + n & Sum (p | ((len (p | k)) + n)) = (Sum (p | k)) + (Sum (q | n)) ) by A1, Lm4, Th6;
then ( k + (2 * (Sum (q | n))) <= (len (p | k)) + n & len (p | k) = k ) by A1, Th15;
hence 2 * (Sum (q | n)) <= n by XREAL_1:8; :: thesis: verum