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

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