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 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 (0 -tuples_on U),U & 0 -tuples_on U = {{}} ) by FOMODEL0:10, Def2;
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 ;
A2: dom (l .--> ({} .--> u)) = {lo} ;
then A3: dom (l .--> ({} .--> u)) c= dom I by A1;
for z being Element of {{}} holds ii . z = hh . z ;
then A4: ii = hh by FUNCT_2:63;
then l .--> ({} .--> u) tolerates I by PARTFUN1:53, A3;
then (l,u) ReassignIn I = (l .--> ({} .--> u)) +* I by FUNCT_4:34
.= I by A2, A1, XBOOLE_1:1, FUNCT_4:19 ;
hence (l,u) ReassignIn I = I ; :: thesis: verum