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

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

per cases ( k <= dom (n --> 0) or k > dom (n --> 0) ) ;

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

A5: (n --> 0) | k = k --> 0 by A4, Lm1;
A6: Sum (k --> 0) = 0 * k by AFINSQ_2:58;
((n --> 0) ^ (m --> 1)) | k = (n --> 0) | k by A4, AFINSQ_1:58;
hence 2 * (Sum (((n --> 0) ^ (m --> 1)) | k)) <= k by A5, A6; :: thesis: verum

end;

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

then reconsider kd = k - (dom (n --> 0)) as Nat by NAT_1:21;
k <= (len (n --> 0)) + (len (m --> 1)) by A3, AFINSQ_1:17;
then k - (len (n --> 0)) <= ((len (m --> 1)) + (len (n --> 0))) - (len (n --> 0)) by XREAL_1:9;
then kd <= m ;
then A8: (m --> 1) | kd = kd --> 1 by Lm1;
reconsider m1 = m --> 1 as XFinSequence of NAT ;
k = kd + (dom (n --> 0)) ;
then ((n --> 0) ^ (m --> 1)) | k = (n --> 0) ^ (m1 | kd) by AFINSQ_1:59;
then A9: Sum (((n --> 0) ^ (m --> 1)) | k) = (Sum (n --> 0)) + (Sum (kd --> 1)) by A8, AFINSQ_2:55;
( dom ((n --> 0) ^ (m --> 1)) = (len (n --> 0)) + (len (m --> 1)) & dom (m --> 1) = m ) by AFINSQ_1:def 3;
then k - n <= (m + n) - n by A3, XREAL_1:9;
then k - n <= n by A1, XXREAL_0:2;
then A10: (k - n) + (k - n) <= n + (k - n) by XREAL_1:6;
( Sum (n --> 0) = n * 0 & Sum (kd --> 1) = kd * 1 ) by AFINSQ_2:58;
hence 2 * (Sum (((n --> 0) ^ (m --> 1)) | k)) <= k by A9, A10; :: thesis: verum

end;

end;

end;

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