let n be Element of 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
then ( rng (p | n) c= rng p & rng p c= {0 ,1} ) by Def1, RELAT_1:99;
then A2: rng (p | n) c= {0 ,1} by XBOOLE_1:1;
for k being Element of NAT st k <= dom (p | n) holds
2 * (Sum ((p | n) | k)) <= k

proof

let k be Element of NAT ; :: thesis: ( k <= dom (p | n) implies 2 * (Sum ((p | n) | k)) <= k )
assume A3: k <= dom (p | n) ; :: thesis: 2 * (Sum ((p | n) | k)) <= k
( k c= dom (p | n) & dom (p | n) = (dom p) /\ n ) by A3, NAT_1:40, RELAT_1:90;
then (p | n) | k = p | k by RELAT_1:103, XBOOLE_1:18;
hence 2 * (Sum ((p | n) | k)) <= k by A1, Th6; :: thesis: verum

end;

hence p | n is dominated_by_0 by A2, Def1; :: thesis: verum