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
C1: for mm being Element of NAT st m = mm holds
IT1 = ((S,U) -TruthEval) . mm and
C2: 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 C1
.= IT2 by C2 ; :: thesis: verum