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