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