let n be Element of NAT ; :: thesis: for p being XFinSequence of 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 ; :: 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 A1: ( p is dominated_by_0 & 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:19, ZFMISC_1:12;
then ( rng p c= {0 ,1} & rng (n --> 1) c= {0 ,1} ) by A1, Def1, XBOOLE_1:1;
then (rng p) \/ (rng (n --> 1)) c= {0 ,1} by XBOOLE_1:8;
hence rng (p ^ (n --> 1)) c= {0 ,1} by AFINSQ_1:29; :: according to CATALAN2:def 1 :: thesis: for k being Element of NAT st k <= dom (p ^ (n --> 1)) holds
2 * (Sum ((p ^ (n --> 1)) | k)) <= k
let m be Element of NAT ; :: thesis: ( m <= dom (p ^ (n --> 1)) implies 2 * (Sum ((p ^ (n --> 1)) | m)) <= m )
assume A2: m <= dom (p ^ (n --> 1)) ; :: thesis: 2 * (Sum ((p ^ (n --> 1)) | m)) <= m

now

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 & 2 * (Sum (p | m)) <= m ) by A1, Th2, Th6;
hence 2 * (Sum ((p ^ (n --> 1)) | m)) <= m ; :: thesis: verum

end;

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

then reconsider md = m - (dom p) as Element of NAT by NAT_1:21;
( dom (n --> 1) = n & len (n --> 1) = dom (n --> 1) ) by FUNCOP_1:19;
then ( dom (p ^ (n --> 1)) = (len p) + n & dom p = len p ) by AFINSQ_1:def 4;
then md + (dom p) <= n + (dom p) by A2;
then A3: md <= n by XREAL_1:8;
then ( (n --> 1) | md = md --> 1 & Sum (md --> 1) = md * 1 & m = (dom p) + md ) by Lm1, Lm2;
then ( (p ^ (n --> 1)) | m = p ^ (md --> 1) & Sum (p ^ (md --> 1)) = (Sum p) + md ) by Lm4, Th3;
then ( 2 * (Sum ((p ^ (n --> 1)) | m)) = (((2 * (Sum p)) + m) - (dom p)) + md & n - n <= ((len p) - (2 * (Sum p))) - n ) by A1, XREAL_1:11;
then ( 2 * (Sum ((p ^ (n --> 1)) | m)) <= (((2 * (Sum p)) + m) - (dom p)) + n & m - (((len p) - (2 * (Sum p))) - n) <= m - 0 & dom p = len p ) by A3, XREAL_1:8, XREAL_1:12;
hence 2 * (Sum ((p ^ (n --> 1)) | m)) <= m by XXREAL_0:2; :: thesis: verum

end;

end;

end;

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