set seq = f |_ (Seg n);
for k being Nat st k >= n + 1 holds
(f |_ (Seg n)) . k = 0
proof
let k be Nat; :: thesis: ( k >= n + 1 implies (f |_ (Seg n)) . k = 0 )
assume k >= n + 1 ; :: thesis: (f |_ (Seg n)) . k = 0
then k > n by NAT_1:16, XXREAL_0:2;
then not k in Seg n by FINSEQ_1:1;
then not k in dom (f | (Seg n)) by RELAT_1:57;
then (f |_ (Seg n)) . k = (NAT --> 0) . k by FUNCT_4:11;
hence (f |_ (Seg n)) . k = 0 ; :: thesis: verum
end;
hence f |_ (Seg n) is summable by Th12; :: thesis: verum