set SS = AllSymbolsOf S;
set UU = the non empty set ;
set II = the Element of the non empty set -InterpretersOf S;
reconsider nn = m as Element of NAT by ORDINAL1:def 12;
reconsider IT = dom (( the Element of the non empty set -InterpretersOf S,nn) -TruthEval) as Subset of (((AllSymbolsOf S) *) \ {{}}) ;
take IT ; :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
IT = dom ((I,mm) -TruthEval)
let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
IT = dom ((I,mm) -TruthEval)
set III = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: for mm being Element of NAT st m = mm holds
IT = dom ((I,mm) -TruthEval)
let mm be Element of NAT ; :: thesis: ( m = mm implies IT = dom ((I,mm) -TruthEval) )
assume m = mm ; :: thesis: IT = dom ((I,mm) -TruthEval)
hence IT = dom ((I,mm) -TruthEval) by Lm14; :: thesis: verum