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