for x being Nat holds ((Sequel f) ^\ (dom f)) . x = 0

proof

let x be Nat; :: thesis: ((Sequel f) ^\ (dom f)) . x = 0
reconsider n = (len f) + x as Nat ;
(len f) + x >= (len f) + 0 by XREAL_1:6;
then B1: not n in Segm (len f) by NAT_1:44;
((Sequel f) ^\ (dom f)) . x = (Sequel f) . ((len f) + x) by NAT_1:def 3
.= f . n by SFX
.= 0 by B1, FUNCT_1:def 2 ;
hence ((Sequel f) ^\ (dom f)) . x = 0 ; :: thesis: verum

end;

hence (Sequel f) ^\ (dom f) is empty-yielding ; :: thesis: verum