let k, n be Nat; :: thesis: for p being XFinSequence of NAT 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 NAT ; :: 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) ) ;
then A3: len ((k --> 0) ^ p) = k + (len p) by AFINSQ_1:17;
Sum (k --> 0) = k * 0 by AFINSQ_2:58;
then A4: Sum ((k --> 0) ^ p) = 0 + (Sum p) by AFINSQ_2:55;
k --> 0 is dominated_by_0 by Lm2;
then (k --> 0) ^ p is dominated_by_0 by A1, Th7;
hence ((k --> 0) ^ p) ^ (n --> 1) is dominated_by_0 by A2, A3, A4, Th9; :: thesis: verum