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

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

hence
IT1 = IT2
by FUNCT_2:12; :: thesis: verumIT11 . 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;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