for k being Nat st k >= len f holds
(Sequel f) . k = 0

proof

let k be Nat; :: thesis: ( k >= len f implies (Sequel f) . k = 0 )
assume A1: k >= len f ; :: thesis: (Sequel f) . k = 0
k in dom (NAT --> 0) by ORDINAL1:def 12;
then A2: k in (dom (NAT --> 0)) \/ (dom f) by XBOOLE_0:def 3;
not k in Segm (len f) by A1, NAT_1:44;
then ((NAT --> 0) +* f) . k = (NAT --> 0) . k by A2, FUNCT_4:def 1;
hence (Sequel f) . k = 0 ; :: thesis: verum

end;

hence Sequel f is summable by FIC; :: thesis: verum