dom (IncAddr (F,k)) = dom F by Def9;
hence IncAddr (F,k) is initial by AFINSQ_1:67; :: thesis: verum