set A = AllTermsOf S;
let IT1, IT2 be Function of (AllTermsOf S),((AllTermsOf S) *); :: thesis: ( ( for t being Element of AllTermsOf S holds IT1 . t = SubTerms t ) & ( for t being Element of AllTermsOf S holds IT2 . t = SubTerms t ) implies IT1 = IT2 )
assume A2: for t being Element of AllTermsOf S holds IT1 . t = SubTerms t ; :: thesis: ( ex t being Element of AllTermsOf S st not IT2 . t = SubTerms t or IT1 = IT2 )
assume A3: for t being Element of AllTermsOf S holds IT2 . t = SubTerms t ; :: thesis: IT1 = IT2

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

let t be Element of AllTermsOf S; :: thesis: IT1 . t = IT2 . t
thus IT1 . t = SubTerms t by A2
.= IT2 . t by A3 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum