let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 & { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} & len p > 0 implies ex q being XFinSequence of NAT st
( p = <%0 %> ^ q & q is dominated_by_0 ) )
assume that
A1: p is dominated_by_0 and
A2: ( { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} & len p > 0 ) ; :: thesis: ex q being XFinSequence of NAT st
( p = <%0 %> ^ q & q is dominated_by_0 )
set M = { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } ;
consider q being XFinSequence of NAT such that
A3: p = (p | 1) ^ q by Th5;
take q ; :: thesis: ( p = <%0 %> ^ q & q is dominated_by_0 )
A4: rng p c= {0 ,1} by A1, Def1;
rng q c= rng p by A3, AFINSQ_1:28;
then A5: rng q c= {0 ,1} by A4, XBOOLE_1:1;
len p >= 1 by A2, NAT_1:14;
then 1 c= dom p by NAT_1:40;
then A6: dom (p | 1) = 1 by RELAT_1:91;
len (p | 1) = dom (p | 1) ;
then A7: p | 1 = <%((p | 1) . 0 )%> by A6, AFINSQ_1:38;
0 in 1 by NAT_1:45;
then A8: (p | 1) . 0 = p . 0 by A6, FUNCT_1:70;
hence p = <%0 %> ^ q by A1, A3, A7, Th7; :: thesis: q is dominated_by_0
assume not q is dominated_by_0 ; :: thesis: contradiction
then consider i being Nat such that
i <= dom q and
A9: 2 * (Sum (q | i)) > i by A5, Def1;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
p | (1 + i) = (p | 1) ^ (q | i) by A3, A6, AFINSQ_1:63;
then A10: Sum (p | (1 + i)) = (Sum <%(p . 0 )%>) + (Sum (q | i)) by A7, A8, AFINSQ_2:67;
A11: 2 * (Sum (q | i)) >= i + 1 by A9, NAT_1:13;
Sum <%(p . 0 )%> = p . 0 by AFINSQ_2:65;
then A12: Sum (p | (1 + i)) = 0 + (Sum (q | i)) by A1, A10, Th7;
then 1 + i >= 2 * (Sum (q | i)) by A1, Th6;
then 1 + i = 2 * (Sum (q | i)) by A11, XXREAL_0:1;
then 1 + i in { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } by A12;
hence contradiction by A2; :: thesis: verum