let S be Language; :: thesis: for l being literal Element of S
for t being termal string of S holds l Subst1 t in Funcs ((AllFormulasOf S),(AllFormulasOf S))
let l be literal Element of S; :: thesis: for t being termal string of S holds l Subst1 t in Funcs ((AllFormulasOf S),(AllFormulasOf S))
let t be termal string of S; :: thesis: l Subst1 t in Funcs ((AllFormulasOf S),(AllFormulasOf S))
set FF = AllFormulasOf S;
set g = l AtomicSubst t;
set AF = AtomicFormulasOf S;
set E = the Element of AllFormulasOf S;
set f = id (AllFormulasOf S);
set IT = (id (AllFormulasOf S)) +* (l AtomicSubst t);
set SS = AllSymbolsOf S;
reconsider FFF = AllFormulasOf S as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
(AtomicFormulasOf S) \ (AllFormulasOf S) = {} ;
then reconsider AFF = AtomicFormulasOf S as Subset of (AllFormulasOf S) by XBOOLE_1:37;
( dom (id (AllFormulasOf S)) = AllFormulasOf S & dom (l AtomicSubst t) = AFF ) by FUNCT_2:def 1;
then A1: dom ((id (AllFormulasOf S)) +* (l AtomicSubst t)) = (AllFormulasOf S) null AFF by FUNCT_4:def 1;
reconsider gg = l AtomicSubst t as AFF -valued Function ;
reconsider ff = id (AllFormulasOf S) as AllFormulasOf S -valued Function ;
( (id (AllFormulasOf S)) +* (l AtomicSubst t) = (id (AllFormulasOf S)) +* (l AtomicSubst t) & dom ((id (AllFormulasOf S)) +* (l AtomicSubst t)) = AllFormulasOf S & rng ((id (AllFormulasOf S)) +* (l AtomicSubst t)) c= AllFormulasOf S ) by RELAT_1:def 19, A1;
hence l Subst1 t in Funcs ((AllFormulasOf S),(AllFormulasOf S)) by FUNCT_2:def 2; :: thesis: verum