let IT1, IT2 be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)); :: thesis: ( ( 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 ; :: thesis: ( 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 ; :: thesis: IT1 = IT2

now :: thesis: for x being object st x in AllFormulasOf S holds
IT11 . x = IT22 . x

let x be object ; :: thesis: ( x in AllFormulasOf S implies IT11 . x = IT22 . x )
assume x in AllFormulasOf S ; :: thesis: IT11 . x = IT22 . x
then reconsider phi = x as wff string of S ;
IT1 . phi = (l,t,n,f) Subst2 phi by A2
.= IT2 . phi by A3 ;
hence IT11 . x = IT22 . x ; :: thesis: verum

end;

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