set g = x .--> f;
set O = OwnSymbolsOf S;
set h = I +* (x .--> f);
B1: dom (x .--> f) = {x} by FUNCOP_1:13;
( OwnSymbolsOf S c= dom I & dom I c= (dom I) \/ (dom (x .--> f)) ) by Lm18, XBOOLE_1:7;
then B2: OwnSymbolsOf S c= (dom I) \/ (dom (x .--> f)) by XBOOLE_1:1;
reconsider I = I as Interpreter of S,U by DefInterpreterLike;

now

let s be own Element of S; :: thesis: (I +* (x .--> f)) . b₁ is Interpreter of b₁,U
Z1: s in OwnSymbolsOf S by FOMODEL1:def 19;

per cases ( s in dom (x .--> f) or not s in dom (x .--> f) ) ;

suppose C1: s in dom (x .--> f) ; :: thesis: (I +* (x .--> f)) . b₁ is Interpreter of b₁,U

then Z0: (I +* (x .--> f)) . s = (x .--> f) . s by Z1, B2, FUNCT_4:def 1
.= f by B1, C1, FUNCOP_1:7 ;
thus (I +* (x .--> f)) . s is Interpreter of s,U by Z0, C1, B1, TARSKI:def 1; :: thesis: verum

end;

suppose not s in dom (x .--> f) ; :: thesis: (I +* (x .--> f)) . b₁ is Interpreter of b₁,U

then (I +* (x .--> f)) . s = I . s by B2, Z1, FUNCT_4:def 1;
hence (I +* (x .--> f)) . s is Interpreter of s,U by DefInterpreter2; :: thesis: verum

end;

end;

end;

then ( I +* (x .--> f) is Interpreter of S,U & I +* (x .--> f) is Function-yielding ) by DefInterpreter2;
hence I +* (x .--> f) is S,U -interpreter-like by DefInterpreterLike; :: thesis: verum