let k be Nat; :: thesis: for p being XFinSequence of NAT st p is dominated_by_0 holds
2 * (Sum (p | k)) <= k
let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 implies 2 * (Sum (p | k)) <= k )
assume A1: p is dominated_by_0 ; :: thesis: 2 * (Sum (p | k)) <= k

now :: thesis: 2 * (Sum (p | k)) <= k

per cases ( k <= dom p or k > dom p ) ;

suppose k <= dom p ; :: thesis: 2 * (Sum (p | k)) <= k

hence 2 * (Sum (p | k)) <= k by A1; :: thesis: verum

end;

suppose A2: k > dom p ; :: thesis: 2 * (Sum (p | k)) <= k

then Segm (len p) c= Segm k by NAT_1:39;
then A3: p | k = p by RELAT_1:68;
( 2 * (Sum (p | (len p))) <= dom p & p | (len p) = p ) by A1;
hence 2 * (Sum (p | k)) <= k by A2, A3, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence 2 * (Sum (p | k)) <= k ; :: thesis: verum