set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
set IT = l Subst1 t;
AllFormulasOf S c= (AllSymbolsOf S) * by XBOOLE_1:1;
then ( l Subst1 t in Funcs ((AllFormulasOf S),(AllFormulasOf S)) & Funcs ((AllFormulasOf S),(AllFormulasOf S)) c= Funcs ((AllFormulasOf S),((AllSymbolsOf S) *)) ) by Lm43, FUNCT_5:56;
hence l Subst1 t is Element of Funcs ((AllFormulasOf S),((AllSymbolsOf S) *)) ; :: thesis: verum