set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set f = (S,U) -TruthEval ;
let IT1, IT2 be Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN); :: thesis: ( ( for mm being Element of NAT st m = mm holds
IT1 = ((S,U) -TruthEval) . mm ) & ( for mm being Element of NAT st m = mm holds
IT2 = ((S,U) -TruthEval) . mm ) implies IT1 = IT2 )
assume that
A1: for mm being Element of NAT st m = mm holds
IT1 = ((S,U) -TruthEval) . mm and
A2: for mm being Element of NAT st m = mm holds
IT2 = ((S,U) -TruthEval) . mm ; :: thesis: IT1 = IT2
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
thus IT1 = ((S,U) -TruthEval) . mm by A1
.= IT2 by A2 ; :: thesis: verum