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;

hence I +* (x .--> f) is S,U -interpreter-like ; :: thesis: verum

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

then
( I +* (x .--> f) is Interpreter of S,U & I +* (x .--> f) is Function-yielding )
by Def3;let s be own Element of S; :: thesis: (I +* (x .--> f)) . b_{1} is Interpreter of b_{1},U

A2: s in OwnSymbolsOf S by FOMODEL1:def 19;

end;A2: s in OwnSymbolsOf S by FOMODEL1:def 19;

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

end;

suppose A3:
s in dom (x .--> f)
; :: thesis: (I +* (x .--> f)) . b_{1} is Interpreter of b_{1},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;.= f by FUNCOP_1:7, A3 ;

thus (I +* (x .--> f)) . s is Interpreter of s,U by A4, A3, TARSKI:def 1; :: thesis: verum

hence I +* (x .--> f) is S,U -interpreter-like ; :: thesis: verum