set g = x .--> f;
set O = OwnSymbolsOf S;
set h = I +* (x .--> f);
( OwnSymbolsOf S c= dom I & dom I c= (dom I) \/ (dom (x .--> f)) ) by Lm2, XBOOLE_1:7;
then A1: OwnSymbolsOf S c= (dom I) \/ (dom (x .--> f)) ;
reconsider I = I as Interpreter of S,U by Def4;
now :: thesis: for s being own Element of S holds (I +* (x .--> f)) . s is Interpreter of s,U
let s be own Element of S; :: thesis: (I +* (x .--> f)) . b1 is Interpreter of b1,U
A2: s in OwnSymbolsOf S by FOMODEL1:def 19;
per cases ( s in dom (x .--> f) or not s in dom (x .--> f) ) ;
suppose A3: s in dom (x .--> f) ; :: thesis: (I +* (x .--> f)) . b1 is Interpreter of b1,U
then A4: (I +* (x .--> f)) . s = (x .--> f) . s by FUNCT_4:def 1, A2, A1
.= f by FUNCOP_1:7, A3 ;
thus (I +* (x .--> f)) . s is Interpreter of s,U by A4, A3, TARSKI:def 1; :: thesis: verum
end;
suppose not s in dom (x .--> f) ; :: thesis: (I +* (x .--> f)) . b1 is Interpreter of b1,U
then (I +* (x .--> f)) . s = I . s by FUNCT_4:def 1, A1, A2;
hence (I +* (x .--> f)) . s is Interpreter of s,U by Def3; :: thesis: verum
end;
end;
end;
then ( I +* (x .--> f) is Interpreter of S,U & I +* (x .--> f) is Function-yielding ) by Def3;
hence I +* (x .--> f) is S,U -interpreter-like ; :: thesis: verum