set h = (x,u) ReassignIn I;
set n = abs (ar x);
( abs (ar x) = 0 & {{}} = 0 -tuples_on U ) by FOMODEL0:10;
then reconsider f = {{}} --> u as Function of ((abs (ar x)) -tuples_on U),U ;
reconsider ff = f as Interpreter of x,U by DefInterpreter1;
(x,u) ReassignIn I = I +* (x .--> ff) ;
hence (x,u) ReassignIn I is S,U -interpreter-like ; :: thesis: verum