let m be Nat; :: thesis: for S being Language
for U being non empty set
for l being literal Element of S
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
let S be Language; :: thesis: for U being non empty set
for l being literal Element of S
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
let U be non empty set ; :: thesis: for l being literal Element of S
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
let l be literal Element of S; :: thesis: for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
let phi1 be wff string of S; :: thesis: for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
let I be Element of U -InterpretersOf S; :: thesis: for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set psi = <*l*> ^ phi1;
set FF = AllFormulasOf S;
set Phim = S -formulasOfMaxDepth m;
let f be PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN; :: thesis: ( dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff implies ( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE ) )
assume ( dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff ) ; :: thesis: ( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
set LH = f -ExFunctor (I,(<*l*> ^ phi1));
reconsider psii = <*l*> ^ phi1, phi11 = phi1 as FinSequence of AllSymbolsOf S by FOMODEL0:26;
A1: (<*l*> ^ phi11) /^ 1 = phi11 by FINSEQ_6:45;

hereby :: thesis: ( ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE implies f -ExFunctor (I,(<*l*> ^ phi1)) = 1 )

assume f -ExFunctor (I,(<*l*> ^ phi1)) = 1 ; :: thesis: ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE
then consider u being Element of U, v being literal Element of S such that
A2: ( (<*l*> ^ phi1) . 1 = v & f . (((v,u) ReassignIn I),((<*l*> ^ phi1) /^ 1)) = TRUE ) by Def15;
take u = u; :: thesis: f . (((l,u) ReassignIn I),phi1) = TRUE
thus f . (((l,u) ReassignIn I),phi1) = TRUE by A2, A1, FINSEQ_1:41; :: thesis: verum

end;

given u being Element of U such that A3: f . (((l,u) ReassignIn I),phi1) = TRUE ; :: thesis: f -ExFunctor (I,(<*l*> ^ phi1)) = 1
ex u1 being Element of U ex l1 being literal Element of S st
( psii . 1 = l1 & f . (((l1,u1) ReassignIn I),(psii /^ 1)) = TRUE ) by A1, FINSEQ_1:41, A3;
hence f -ExFunctor (I,(<*l*> ^ phi1)) = 1 by Def15; :: thesis: verum