set f = (S,U) -TruthEval ;
reconsider nn = m as Element of NAT by ORDINAL1:def 12;
take
((S,U) -TruthEval) . nn
; for mm being Element of NAT st m = mm holds
((S,U) -TruthEval) . nn = ((S,U) -TruthEval) . mm
let mm be Element of NAT ; ( m = mm implies ((S,U) -TruthEval) . nn = ((S,U) -TruthEval) . mm )
assume
m = mm
; ((S,U) -TruthEval) . nn = ((S,U) -TruthEval) . mm
hence
((S,U) -TruthEval) . nn = ((S,U) -TruthEval) . mm
; verum