let n be Nat; :: thesis: for p being XFinSequence of NAT st p is dominated_by_0 holds
p | n is dominated_by_0
let p be XFinSequence of NAT ; :: 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: Segm k c= Segm (len (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, Th2; :: thesis: verum
end;
( rng (p | n) c= rng p & rng p c= {0,1} ) by A1;
then rng (p | n) c= {0,1} ;
hence p | n is dominated_by_0 by A2; :: thesis: verum