set A = AllTermsOf S;

let IT1, IT2 be Function of (AllTermsOf S),U; :: thesis: ( ( for t being Element of AllTermsOf S holds IT1 . t = I -TermEval t ) & ( for t being Element of AllTermsOf S holds IT2 . t = I -TermEval t ) implies IT1 = IT2 )

assume A2: for t being Element of AllTermsOf S holds IT1 . t = I -TermEval t ; :: thesis: ( ex t being Element of AllTermsOf S st not IT2 . t = I -TermEval t or IT1 = IT2 )

assume A3: for t being Element of AllTermsOf S holds IT2 . t = I -TermEval t ; :: thesis: IT1 = IT2

let IT1, IT2 be Function of (AllTermsOf S),U; :: thesis: ( ( for t being Element of AllTermsOf S holds IT1 . t = I -TermEval t ) & ( for t being Element of AllTermsOf S holds IT2 . t = I -TermEval t ) implies IT1 = IT2 )

assume A2: for t being Element of AllTermsOf S holds IT1 . t = I -TermEval t ; :: thesis: ( ex t being Element of AllTermsOf S st not IT2 . t = I -TermEval t or IT1 = IT2 )

assume A3: for t being Element of AllTermsOf S holds IT2 . t = I -TermEval t ; :: thesis: IT1 = IT2

now :: thesis: for t being Element of AllTermsOf S holds IT1 . t = IT2 . t

hence
IT1 = IT2
by FUNCT_2:63; :: thesis: verumlet t be Element of AllTermsOf S; :: thesis: IT1 . t = IT2 . t

thus IT1 . t = I -TermEval t by A2

.= IT2 . t by A3 ; :: thesis: verum

end;thus IT1 . t = I -TermEval t by A2

.= IT2 . t by A3 ; :: thesis: verum