let S be Language; :: thesis: for U being non empty set

for l being literal Element of S

for I being S,b_{1} -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;

then A4: ii = hh by FUNCT_2:63;

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

for l being literal Element of S

for I being S,b

( 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;

then A4: ii = hh by FUNCT_2:63;

now :: thesis: for z being object st z in dom (l .--> ({} .--> u)) holds

(l .--> ({} .--> u)) . z = I . z

then
l .--> ({} .--> u) tolerates I
by PARTFUN1:53, A3;(l .--> ({} .--> u)) . z = I . z

let z be object ; :: thesis: ( z in dom (l .--> ({} .--> u)) implies (l .--> ({} .--> u)) . z = I . z )

assume A5: z in dom (l .--> ({} .--> u)) ; :: thesis: (l .--> ({} .--> u)) . z = I . z

thus (l .--> ({} .--> u)) . z = {} .--> u by FUNCOP_1:7, A5

.= I . z by A4, A5, TARSKI:def 1 ; :: thesis: verum

end;assume A5: z in dom (l .--> ({} .--> u)) ; :: thesis: (l .--> ({} .--> u)) . z = I . z

thus (l .--> ({} .--> u)) . z = {} .--> u by FUNCOP_1:7, A5

.= I . z by A4, A5, TARSKI:def 1 ; :: thesis: verum

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