let p be XFinSequence of ; :: thesis: ( p is dominated_by_0 implies ( <%0%> ^ p is dominated_by_0 & { N where N is Element of NAT : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {} ) )
reconsider q = 1 --> 0 as XFinSequence of ;
assume A1: p is dominated_by_0 ; :: thesis: ( <%0%> ^ p is dominated_by_0 & { N where N is Element of NAT : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {} )
( dom q = 1 & len q = dom q ) by FUNCOP_1:19;
then A2: q = <%(q . 0)%> by AFINSQ_1:38;
q is dominated_by_0 by Lm3;
then ( q is dominated_by_0 & q . 0 = 0 ) by Th7;
hence <%0%> ^ p is dominated_by_0 by A1, A2, Th11; :: thesis: { N where N is Element of NAT : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {}
set M = { N where N is Element of NAT : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } ;
assume { N where N is Element of NAT : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } <> {} ; :: thesis: contradiction
then consider x being set such that
A3: x in { N where N is Element of NAT : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } by XBOOLE_0:def 1;
consider i being Element of NAT such that
x = i and
A4: 2 * (Sum ((<%0%> ^ p) | i)) = i and
A5: i > 0 by A3;
reconsider i1 = i - 1 as Element of NAT by A5, NAT_1:20;
dom <%0%> = 1 by AFINSQ_1:36;
then i = (dom <%0%>) + i1 ;
then (<%0%> ^ p) | i = <%0%> ^ (p | i1) by AFINSQ_1:63;
then A6: Sum ((<%0%> ^ p) | i) = (Sum <%0%>) + (Sum (p | i1)) by AFINSQ_2:67;
( Sum <%0%> = 0 & i1 < i1 + 1 ) by NAT_1:13, AFINSQ_2:65;
hence contradiction by A1, A4, A6, Th6; :: thesis: verum