let n be Nat; :: thesis: for p being XFinSequence of NAT st p is dominated_by_0 & n <= (len p) - (2 * (Sum p)) holds
p ^ (n --> 1) is dominated_by_0
let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 & n <= (len p) - (2 * (Sum p)) implies p ^ (n --> 1) is dominated_by_0 )
set q = n --> 1;
assume that
A1: p is dominated_by_0 and
A2: n <= (len p) - (2 * (Sum p)) ; :: thesis: p ^ (n --> 1) is dominated_by_0
( rng (n --> 1) c= {1} & {1} c= {0,1} ) by FUNCOP_1:13, ZFMISC_1:7;
then A3: rng (n --> 1) c= {0,1} ;
rng p c= {0,1} by A1;
then (rng p) \/ (rng (n --> 1)) c= {0,1} by A3, XBOOLE_1:8;
hence rng (p ^ (n --> 1)) c= {0,1} by AFINSQ_1:26; :: according to CATALAN2:def 1 :: thesis: for k being Nat st k <= dom (p ^ (n --> 1)) holds
2 * (Sum ((p ^ (n --> 1)) | k)) <= k
let m be Nat; :: thesis: ( m <= dom (p ^ (n --> 1)) implies 2 * (Sum ((p ^ (n --> 1)) | m)) <= m )
assume A4: m <= dom (p ^ (n --> 1)) ; :: thesis: 2 * (Sum ((p ^ (n --> 1)) | m)) <= m

now :: thesis: 2 * (Sum ((p ^ (n --> 1)) | m)) <= m

per cases ( m <= dom p or m > dom p ) ;

suppose m <= dom p ; :: thesis: 2 * (Sum ((p ^ (n --> 1)) | m)) <= m

then (p ^ (n --> 1)) | m = p | m by AFINSQ_1:58;
hence 2 * (Sum ((p ^ (n --> 1)) | m)) <= m by A1, Th2; :: thesis: verum

end;

suppose m > dom p ; :: thesis: 2 * (Sum ((p ^ (n --> 1)) | m)) <= m

then reconsider md = m - (dom p) as Nat by NAT_1:21;
A5: m = (dom p) + md ;
Sum (md --> 1) = md * 1 by AFINSQ_2:58;
then A6: Sum (p ^ (md --> 1)) = (Sum p) + md by AFINSQ_2:55;
( dom (n --> 1) = n & len (n --> 1) = dom (n --> 1) ) ;
then dom (p ^ (n --> 1)) = (len p) + n by AFINSQ_1:def 3;
then md + (dom p) <= n + (dom p) by A4;
then A7: md <= n by XREAL_1:6;
then (n --> 1) | md = md --> 1 by Lm1;
then (p ^ (n --> 1)) | m = p ^ (md --> 1) by A5, AFINSQ_1:59;
then 2 * (Sum ((p ^ (n --> 1)) | m)) = (((2 * (Sum p)) + m) - (dom p)) + md by A6;
then A8: 2 * (Sum ((p ^ (n --> 1)) | m)) <= (((2 * (Sum p)) + m) - (dom p)) + n by A7, XREAL_1:6;
n - n <= ((len p) - (2 * (Sum p))) - n by A2, XREAL_1:9;
then m - (((len p) - (2 * (Sum p))) - n) <= m - 0 by XREAL_1:10;
hence 2 * (Sum ((p ^ (n --> 1)) | m)) <= m by A8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence 2 * (Sum ((p ^ (n --> 1)) | m)) <= m ; :: thesis: verum