let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 & { N where N is 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 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 Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } ;
consider q being XFinSequence of NAT such that
A3: p = (p | 1) ^ q by Th1;
take q ; :: thesis: ( p = <%0%> ^ q & q is dominated_by_0 )
A4: rng p c= {0,1} by A1;
rng q c= rng p by A3, AFINSQ_1:25;
then A5: rng q c= {0,1} by A4;
len p >= 1 by A2, NAT_1:14;
then Segm 1 c= Segm (len p) by NAT_1:39;
then A6: dom (p | 1) = 1 by RELAT_1:62;
A7: p | 1 = <%((p | 1) . 0)%> by A6, AFINSQ_1:34;
0 in Segm 1 by NAT_1:44;
then A8: (p | 1) . 0 = p . 0 by A6, FUNCT_1:47;
hence p = <%0%> ^ q by A1, A3, A7, Th3; :: 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;
reconsider i = i as Nat ;
p | (1 + i) = (p | 1) ^ (q | i) by A3, A6, AFINSQ_1:59;
then A10: Sum (p | (1 + i)) = (Sum <%(p . 0)%>) + (Sum (q | i)) by A7, A8, AFINSQ_2:55;
A11: 2 * (Sum (q | i)) >= i + 1 by A9, NAT_1:13;
Sum <%(p . 0)%> = p . 0 by AFINSQ_2:53;
then A12: Sum (p | (1 + i)) = 0 + (Sum (q | i)) by A1, A10, Th3;
then 1 + i >= 2 * (Sum (q | i)) by A1, Th2;
then 1 + i = 2 * (Sum (q | i)) by A11, XXREAL_0:1;
then 1 + i in { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } by A12;
hence contradiction by A2; :: thesis: verum