let n, k be Nat; :: thesis: for p being XFinSequence of st p is dominated_by_0 & n <= (k + (len p)) - (2 * (Sum p)) holds
((k --> 0) ^ p) ^ (n --> 1) is dominated_by_0
let p be XFinSequence of ; :: thesis: ( p is dominated_by_0 & n <= (k + (len p)) - (2 * (Sum p)) implies ((k --> 0) ^ p) ^ (n --> 1) is dominated_by_0 )
assume that
A1: p is dominated_by_0 and
A2: n <= (k + (len p)) - (2 * (Sum p)) ; :: thesis: ((k --> 0) ^ p) ^ (n --> 1) is dominated_by_0
set q = k --> 0;
( dom (k --> 0) = k & len (k --> 0) = dom (k --> 0) ) by FUNCOP_1:19;
then A3: len ((k --> 0) ^ p) = k + (len p) by AFINSQ_1:20;
Sum (k --> 0) = k * 0 by AFINSQ_2:70;
then A4: Sum ((k --> 0) ^ p) = 0 + (Sum p) by AFINSQ_2:67;
k --> 0 is dominated_by_0 by Lm3;
then (k --> 0) ^ p is dominated_by_0 by A1, Th11;
hence ((k --> 0) ^ p) ^ (n --> 1) is dominated_by_0 by A2, A3, A4, Th13; :: thesis: verum