A1: ( dom <%0%> = 1 & rng <%0%> = {0} ) by AFINSQ_1:33;
set q1 = 1 --> 1;
set q0 = 1 --> 0;
let m be Nat; :: thesis: for p being XFinSequence of NAT st m = min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } & m > 0 & p is dominated_by_0 holds
ex q being XFinSequence of NAT st
( p | m = ((1 --> 0) ^ q) ^ (1 --> 1) & q is dominated_by_0 )
let p be XFinSequence of NAT ; :: thesis: ( m = min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } & m > 0 & p is dominated_by_0 implies ex q being XFinSequence of NAT st
( p | m = ((1 --> 0) ^ q) ^ (1 --> 1) & q is dominated_by_0 ) )
assume that
A2: ( m = min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } & m > 0 ) and
A3: p is dominated_by_0 ; :: thesis: ex q being XFinSequence of NAT st
( p | m = ((1 --> 0) ^ q) ^ (1 --> 1) & q is dominated_by_0 )
reconsider M = { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } as non empty Subset of NAT by A2, NAT_1:def 1;
min* M in M by NAT_1:def 1;
then consider n being Nat such that
A4: n = min* M and
A5: 2 * (Sum (p | n)) = n and
A6: n > 0 ;
reconsider n1 = n - 1 as Nat by A6, NAT_1:20;
Sum (p | n) <> 0 by A5, A6;
then n >= 2 * 1 by A5, NAT_1:14, XREAL_1:64;
then A7: n1 >= 2 - 1 by XREAL_1:9;
then A8: Segm 1 c= Segm n1 by NAT_1:39;
then A9: (p | n1) | 1 = p | 1 by RELAT_1:74;
A10: n1 < n1 + 1 by NAT_1:13;
n <= len p by A3, A5, Th11;
then A11: n1 < len p by A10, XXREAL_0:2;
then 1 < len p by A7, XXREAL_0:2;
then len (p | 1) = 1 by AFINSQ_1:11;
then A12: p | 1 = <%((p | 1) . 0)%> by AFINSQ_1:34;
p | 1 is dominated_by_0 by A3, Th6;
then (p | 1) . 0 = 0 by Th3;
then A13: p | 1 = 1 --> 0 by A12, A1, FUNCOP_1:9;
consider q being XFinSequence of NAT such that
A14: p | n1 = ((p | n1) | 1) ^ q by Th1;
set qq = ((1 --> 0) ^ q) ^ (1 --> 1);
take q ; :: thesis: ( p | m = ((1 --> 0) ^ q) ^ (1 --> 1) & q is dominated_by_0 )
A15: p | (n1 + 1) = (p | n1) ^ (1 --> 1) by A3, A5, Th13;
hence p | m = ((1 --> 0) ^ q) ^ (1 --> 1) by A2, A4, A14, A8, A13, RELAT_1:74; :: thesis: q is dominated_by_0
( rng q c= rng ((1 --> 0) ^ q) & rng ((1 --> 0) ^ q) c= rng (((1 --> 0) ^ q) ^ (1 --> 1)) ) by AFINSQ_1:24, AFINSQ_1:25;
then A16: rng q c= rng (((1 --> 0) ^ q) ^ (1 --> 1)) ;
p | m is dominated_by_0 by A3, Th6;
then rng (((1 --> 0) ^ q) ^ (1 --> 1)) c= {0,1} by A2, A4, A14, A13, A9, A15;
hence rng q c= {0,1} by A16; :: according to CATALAN2:def 1 :: thesis: for k being Nat st k <= dom q holds
2 * (Sum (q | k)) <= k
A17: dom (1 --> 0) = 1 ;
len (p | n1) = n1 by A11, AFINSQ_1:11;
then A18: n1 = (len (1 --> 0)) + (len q) by A14, A13, A9, AFINSQ_1:17;
let k be Nat; :: thesis: ( k <= dom q implies 2 * (Sum (q | k)) <= k )
assume k <= dom q ; :: thesis: 2 * (Sum (q | k)) <= k
then A19: (len (1 --> 0)) + k <= n1 by A18, XREAL_1:6;
then Segm ((len (1 --> 0)) + k) c= Segm n1 by NAT_1:39;
then A20: (p | n1) | (1 + k) = p | (1 + k) by RELAT_1:74;
A21: 1 + k < n by A15, A19, NAT_1:13;
A22: 2 * (Sum (p | (1 + k))) < 1 + k

proof

assume A23: 2 * (Sum (p | (1 + k))) >= 1 + k ; :: thesis: contradiction
2 * (Sum (p | (k + 1))) <= k + 1 by A3, Th2;
then 2 * (Sum (p | (1 + k))) = 1 + k by A23, XXREAL_0:1;
then 1 + k in M ;
hence contradiction by A4, A21, NAT_1:def 1; :: thesis: verum

end;

(p | n1) | (1 + k) = (1 --> 0) ^ (q | k) by A14, A13, A9, A17, AFINSQ_1:59;
then A24: Sum (p | (1 + k)) = (Sum (1 --> 0)) + (Sum (q | k)) by A20, AFINSQ_2:55;
Sum (1 --> 0) = 0 * 1 by AFINSQ_2:58;
hence 2 * (Sum (q | k)) <= k by A24, A22, NAT_1:13; :: thesis: verum