let IT1, IT2 be Element of BOOLEAN ; :: thesis: ( ( for m being Nat st w is m -wff holds
IT1 = ((I,m) -TruthEval) . w ) & ( for m being Nat st w is m -wff holds
IT2 = ((I,m) -TruthEval) . w ) implies IT1 = IT2 )
assume A5: for m being Nat st w is m -wff holds
IT1 = ((I,m) -TruthEval) . w ; :: thesis: ( ex m being Nat st
( w is m -wff & not IT2 = ((I,m) -TruthEval) . w ) or IT1 = IT2 )
assume A6: for m being Nat st w is m -wff holds
IT2 = ((I,m) -TruthEval) . w ; :: thesis: IT1 = IT2
consider m being Nat such that
A7: w is m -wff by Def24;
thus IT1 = ((I,m) -TruthEval) . w by A5, A7
.= IT2 by A6, A7 ; :: thesis: verum