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

proof

let k be Nat; :: thesis: ( k <= dom (p | n) implies 2 * (Sum ((p | n) | k)) <= k )
assume k <= dom (p | n) ; :: thesis: 2 * (Sum ((p | n) | k)) <= k
then A3: k c= dom (p | n) by NAT_1:39;
dom (p | n) = (dom p) /\ n by RELAT_1:61;
then (p | n) | k = p | k by A3, RELAT_1:74, XBOOLE_1:18;
hence 2 * (Sum ((p | n) | k)) <= k by A1, Th6; :: thesis: verum

end;

( rng (p | n) c= rng p & rng p c= {0,1} ) by A1, Def1, RELAT_1:70;
then rng (p | n) c= {0,1} by XBOOLE_1:1;
hence p | n is dominated_by_0 by A2, Def1; :: thesis: verum