let n be Nat; :: thesis: for p being XFinSequence of NAT st p is dominated_by_0 holds
2 * (Sum (p | ((2 * n) + 1))) < (2 * n) + 1
let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 implies 2 * (Sum (p | ((2 * n) + 1))) < (2 * n) + 1 )
assume p is dominated_by_0 ; :: thesis: 2 * (Sum (p | ((2 * n) + 1))) < (2 * n) + 1
then A1: 2 * (Sum (p | ((2 * n) + 1))) <= (2 * n) + 1 by Th2;
assume 2 * (Sum (p | ((2 * n) + 1))) >= (2 * n) + 1 ; :: thesis: contradiction
then 2 * (Sum (p | ((2 * n) + 1))) = (2 * n) + 1 by A1, XXREAL_0:1;
then 2 * ((Sum (p | ((2 * n) + 1))) - n) = 1 ;
hence contradiction by INT_1:9; :: thesis: verum