let S be Language; :: thesis: for U being non empty set
for l being literal Element of S
for I being S,b₁ -interpreter-like Function ex u being Element of U st
( u = (I . l) . {} & (l,u) ReassignIn I = I )
let U be non empty set ; :: thesis: for l being literal Element of S
for I being S,U -interpreter-like Function ex u being Element of U st
( u = (I . l) . {} & (l,u) ReassignIn I = I )
let l be literal Element of S; :: thesis: for I being S,U -interpreter-like Function ex u being Element of U st
( u = (I . l) . {} & (l,u) ReassignIn I = I )
let I be S,U -interpreter-like Function; :: thesis: ex u being Element of U st
( u = (I . l) . {} & (l,u) ReassignIn I = I )
set O = OwnSymbolsOf S;
(OwnSymbolsOf S) \ (dom I) = {} ;
then B0: ( OwnSymbolsOf S c= dom I & {{}} = {{}} ) by XBOOLE_1:37;
reconsider lo = l as Element of OwnSymbolsOf S by FOMODEL1:def 19;
reconsider i = I . l as Interpreter of l,U ;
( i is Function of (0 -tuples_on U),U & 0 -tuples_on U = {{}} ) by DefInterpreter1, FOMODEL0:10;
then reconsider ii = i as Function of {{}},U ;
reconsider e = {} as Element of {{}} by TARSKI:def 1;
reconsider u = ii . e as Element of U ;
take u ; :: thesis: ( u = (I . l) . {} & (l,u) ReassignIn I = I )
thus u = (I . l) . {} ; :: thesis: (l,u) ReassignIn I = I
set h = {} .--> u;
set H = l .--> ({} .--> u);
set J = (l,u) ReassignIn I;
{} .--> u = {{}} --> u ;
then reconsider hh = {} .--> u as Function of {{}},U ;
B2: dom (l .--> ({} .--> u)) = {lo} by FUNCOP_1:13;
then B1: dom (l .--> ({} .--> u)) c= dom I by B0, XBOOLE_1:1;

now

let z be Element of {{}}; :: thesis: ii . z = hh . z
( ii . z = u & hh . z = u ) by FUNCOP_1:7;
hence ii . z = hh . z ; :: thesis: verum

end;

then B3: ii = hh by FUNCT_2:63;

now

let z be set ; :: thesis: ( z in dom (l .--> ({} .--> u)) implies (l .--> ({} .--> u)) . z = I . z )
assume z in dom (l .--> ({} .--> u)) ; :: thesis: (l .--> ({} .--> u)) . z = I . z
then C0: z in {l} by FUNCOP_1:13;
hence (l .--> ({} .--> u)) . z = {} .--> u by FUNCOP_1:7
.= I . z by B3, C0, TARSKI:def 1 ;
:: thesis: verum

end;

then l .--> ({} .--> u) tolerates I by B1, PARTFUN1:53;
then (l,u) ReassignIn I = (l .--> ({} .--> u)) +* I by FUNCT_4:34
.= I by B2, B0, FUNCT_4:19, XBOOLE_1:1 ;
hence (l,u) ReassignIn I = I ; :: thesis: verum