let S be Language; :: thesis: for U being non empty set
for l being literal Element of S
for I being S,b1 -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 A1: ( 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 (),U & 0 -tuples_on U = ) by ;
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 .--> ();
set J = (l,u) ReassignIn I;
{} .--> u = --> u ;
then reconsider hh = {} .--> u as Function of ,U ;
A2: dom (l .--> ()) = {lo} ;
then A3: dom (l .--> ()) c= dom I by A1;
now :: thesis: for z being Element of holds ii . z = hh . z
let z be Element of ; :: thesis: ii . z = hh . z
thus ii . z = hh . z ; :: thesis: verum
end;
then A4: ii = hh by FUNCT_2:63;
now :: thesis: for z being object st z in dom (l .--> ()) holds
(l .--> ()) . z = I . z
let z be object ; :: thesis: ( z in dom (l .--> ()) implies (l .--> ()) . z = I . z )
assume A5: z in dom (l .--> ()) ; :: thesis: (l .--> ()) . z = I . z
thus (l .--> ()) . z = {} .--> u by
.= I . z by ; :: thesis: verum
end;
then l .--> () tolerates I by ;
then (l,u) ReassignIn I = (l .--> ()) +* I by FUNCT_4:34
.= I by ;
hence (l,u) ReassignIn I = I ; :: thesis: verum