let k be Nat; :: thesis: for p being XFinSequence of st p is dominated_by_0 holds
2 * (Sum (p | k)) <= k
let p be XFinSequence of ; :: 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

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, Def1; :: thesis: verum

end;

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

then dom p c= k by NAT_1:40;
then A3: p | k = p by RELAT_1:97;
( 2 * (Sum (p | (len p))) <= dom p & p | (len p) = p ) by A1, Def1, RELAT_1:97;
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