let seq be Complex_Sequence; :: thesis: for x being Nat st ( for k being Nat st k >= x holds
seq . k = 0 ) holds
seq is summable
let x be Nat; :: thesis: ( ( for k being Nat st k >= x holds
seq . k = 0 ) implies seq is summable )
assume A1: for k being Nat st k >= x holds
seq . k = 0 ; :: thesis: seq is summable
for k being Nat holds (seq ^\ x) . k = 0

proof

let k be Nat; :: thesis: (seq ^\ x) . k = 0
B1: k + x >= 0 + x by XREAL_1:6;
(seq ^\ x) . k = seq . (k + x) by NAT_1:def 3;
hence (seq ^\ x) . k = 0 by A1, B1; :: thesis: verum

end;

then seq ^\ x is empty-yielding ;
hence seq is summable by COMSEQ_3:59; :: thesis: verum