set seq = f |_ (Seg n);

for k being Nat st k >= n + 1 holds

(f |_ (Seg n)) . k = 0

for k being Nat st k >= n + 1 holds

(f |_ (Seg n)) . k = 0

proof

hence
f |_ (Seg n) is summable
by Th12; :: thesis: verum
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;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