let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 implies ( <%0%> ^ p is dominated_by_0 & { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {} ) )
reconsider q = 1 --> 0 as XFinSequence of NAT ;
assume A1: p is dominated_by_0 ; :: thesis: ( <%0%> ^ p is dominated_by_0 & { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {} )
( dom q = 1 & len q = dom q ) ;
then A2: q = <%(q . 0)%> by AFINSQ_1:34;
q is dominated_by_0 by Lm2;
then ( q is dominated_by_0 & q . 0 = 0 ) ;
hence <%0%> ^ p is dominated_by_0 by A1, A2, Th7; :: thesis: { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {}
set M = { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } ;
assume { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A3: x in { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } by XBOOLE_0:def 1;
consider i being Nat such that
x = i and
A4: 2 * (Sum ((<%0%> ^ p) | i)) = i and
A5: i > 0 by A3;
reconsider i1 = i - 1 as Nat by A5, NAT_1:20;
dom <%0%> = 1 by AFINSQ_1:33;
then i = (dom <%0%>) + i1 ;
then (<%0%> ^ p) | i = <%0%> ^ (p | i1) by AFINSQ_1:59;
then A6: Sum ((<%0%> ^ p) | i) = (Sum <%0%>) + (Sum (p | i1)) by AFINSQ_2:55;
( Sum <%0%> = 0 & i1 < i1 + 1 ) by AFINSQ_2:53, NAT_1:13;
hence contradiction by A1, A4, A6, Th2; :: thesis: verum