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

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

suppose k <= dom p ; :: thesis: 2 * (Sum ((p ^ q) | k)) <= k

then ( (p ^ q) | k = p | k & 2 * (Sum (p | k)) <= k ) by A1, Def1, Th2;
hence 2 * (Sum ((p ^ q) | k)) <= k ; :: thesis: verum

end;

suppose k > dom p ; :: thesis: 2 * (Sum ((p ^ q) | k)) <= k

then reconsider kd = k - (dom p) as Element of NAT by NAT_1:21;
( k = kd + (dom p) & q | kd is dominated_by_0 ) by A1, Th10;
then ( (p ^ q) | k = p ^ (q | kd) & 2 * (Sum (p | (len p))) <= len p & 2 * (Sum (q | kd)) <= kd & len p = dom p & p | (dom p) = p ) by A1, Th3, Th6, RELAT_1:98;
then ( Sum ((p ^ q) | k) = (Sum p) + (Sum (q | kd)) & (2 * (Sum p)) + (2 * (Sum (q | kd))) <= (dom p) + kd ) by Lm4, XREAL_1:9;
hence 2 * (Sum ((p ^ q) | k)) <= k ; :: thesis: verum

end;

end;

end;

hence 2 * (Sum ((p ^ q) | k)) <= k ; :: thesis: verum