assume not IncAddr F,k is empty ; :: thesis: contradiction
then reconsider f = IncAddr F,k as non empty Function ;
A1: dom f <> {} ;
dom (IncAddr F,k) = dom F by Def15;
hence contradiction by A1; :: thesis: verum