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