let k be Nat; :: thesis: for p, q being XFinSequence of NAT 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 NAT ; :: thesis: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k & p = (p | k) ^ q implies q is dominated_by_0 )
assume that
A1: p is dominated_by_0 and
A2: 2 * (Sum (p | k)) = k and
A3: p = (p | k) ^ q ; :: thesis: q is dominated_by_0
A4: len (p | k) = k by A1, A2, Th11;
( rng q c= rng p & rng p c= {0,1} ) by A1, A3, AFINSQ_1:25;
hence rng q c= {0,1} ; :: according to CATALAN2:def 1 :: thesis: for k being Nat st k <= dom q holds
2 * (Sum (q | k)) <= k
let n be 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 A3, AFINSQ_1:59;
then A5: Sum (p | ((len (p | k)) + n)) = (Sum (p | k)) + (Sum (q | n)) by AFINSQ_2:55;
2 * (Sum (p | ((len (p | k)) + n))) <= (len (p | k)) + n by A1, Th2;
then k + (2 * (Sum (q | n))) <= (len (p | k)) + n by A2, A5;
hence 2 * (Sum (q | n)) <= n by A4, XREAL_1:6; :: thesis: verum