let p, q be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 & q is dominated_by_0 implies p ^ q is dominated_by_0 )
assume that
A1: p is dominated_by_0 and
A2: q is dominated_by_0 ; :: thesis: p ^ q is dominated_by_0
( rng p c= {0,1} & rng q c= {0,1} ) by A1, A2;
then (rng p) \/ (rng q) c= {0,1} by XBOOLE_1:8;
hence rng (p ^ q) c= {0,1} by AFINSQ_1:26; :: according to CATALAN2:def 1 :: thesis: for k being Nat st k <= dom (p ^ q) holds
2 * (Sum ((p ^ q) | k)) <= k
let k be Nat; :: thesis: ( k <= dom (p ^ q) implies 2 * (Sum ((p ^ q) | k)) <= k )
assume k <= dom (p ^ q) ; :: thesis: 2 * (Sum ((p ^ q) | k)) <= k
now :: thesis: 2 * (Sum ((p ^ q) | k)) <= k
per cases ( k <= dom p or k > dom p ) ;
suppose A3: k <= dom p ; :: thesis: 2 * (Sum ((p ^ q) | k)) <= k
then (p ^ q) | k = p | k by AFINSQ_1:58;
hence 2 * (Sum ((p ^ q) | k)) <= k by A1, A3; :: thesis: verum
end;
suppose k > dom p ; :: thesis: 2 * (Sum ((p ^ q) | k)) <= k
then reconsider kd = k - (dom p) as Nat by NAT_1:21;
k = kd + (dom p) ;
then (p ^ q) | k = p ^ (q | kd) by AFINSQ_1:59;
then A4: Sum ((p ^ q) | k) = (Sum p) + (Sum (q | kd)) by AFINSQ_2:55;
( 2 * (Sum (p | (len p))) <= len p & 2 * (Sum (q | kd)) <= kd ) by A1, A2, Th2;
then (2 * (Sum p)) + (2 * (Sum (q | kd))) <= (dom p) + kd by XREAL_1:7;
hence 2 * (Sum ((p ^ q) | k)) <= k by A4; :: thesis: verum
end;
end;
end;
hence 2 * (Sum ((p ^ q) | k)) <= k ; :: thesis: verum