let IT1, IT2 be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)); ( ( for phi being wff string of S holds IT1 . phi = (l,t,n,f) Subst2 phi ) & ( for phi being wff string of S holds IT2 . phi = (l,t,n,f) Subst2 phi ) implies IT1 = IT2 )
reconsider IT11 = IT1, IT22 = IT2 as Function of (AllFormulasOf S),(AllFormulasOf S) ;
assume A2:
for phi being wff string of S holds IT1 . phi = (l,t,n,f) Subst2 phi
; ( ex phi being wff string of S st not IT2 . phi = (l,t,n,f) Subst2 phi or IT1 = IT2 )
assume A3:
for phi being wff string of S holds IT2 . phi = (l,t,n,f) Subst2 phi
; IT1 = IT2
hence
IT1 = IT2
by FUNCT_2:12; verum