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 A6: 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 A7: for m being Nat st w is m -wff holds
IT2 = ((I,m) -TruthEval) . w ; :: thesis: IT1 = IT2
consider m being Nat such that
A8: w is m -wff by Def25;
thus IT1 = ((I,m) -TruthEval) . w by A6, A8
.= IT2 by A7, A8 ; :: thesis: verum