let S be Language; :: thesis: for U being non empty set
for I being S,b1 -interpreter-like Function
for xx being Function of (),U holds
( ^^^(I * ()),^^^xx,()____ is Element of Funcs ((),U) & AllTermsOf S c= dom (I * ()) )

let U be non empty set ; :: thesis: for I being S,U -interpreter-like Function
for xx being Function of (),U holds
( ^^^(I * ()),^^^xx,()____ is Element of Funcs ((),U) & AllTermsOf S c= dom (I * ()) )

let I be S,U -interpreter-like Function; :: thesis: for xx being Function of (),U holds
( ^^^(I * ()),^^^xx,()____ is Element of Funcs ((),U) & AllTermsOf S c= dom (I * ()) )

set A = AllTermsOf S;
set F = S -firstChar ;
set ST = S -subTerms ;
set SS = AllSymbolsOf S;
set Z = AtomicTermsOf S;
set T = S -termsOfMaxDepth ;
A1: dom () = (() *) \ by FUNCT_2:def 1;
let xx be Function of (),U; :: thesis: ( ^^^(I * ()),^^^xx,()____ is Element of Funcs ((),U) & AllTermsOf S c= dom (I * ()) )
set f = ^^^xx,()__;
set g = ^^^(I * ()),^^^xx,()____;
A2: dom ^^^xx,()__ = dom () by Def6
.= AllTermsOf S by FUNCT_2:def 1 ;
A3: for a being set st a in AllTermsOf S holds
( a in dom (I * ()) & ( a in dom ^^^(I * ()),^^^xx,()____ implies ^^^(I * ()),^^^xx,()____ . a in U ) )
proof
let a be set ; :: thesis: ( a in AllTermsOf S implies ( a in dom (I * ()) & ( a in dom ^^^(I * ()),^^^xx,()____ implies ^^^(I * ()),^^^xx,()____ . a in U ) ) )
assume A4: a in AllTermsOf S ; :: thesis: ( a in dom (I * ()) & ( a in dom ^^^(I * ()),^^^xx,()____ implies ^^^(I * ()),^^^xx,()____ . a in U ) )
then reconsider t = a as termal string of S ;
set n = |.(ar t).|;
reconsider ss = () . t as termal Element of S ;
reconsider s = ss as own Element of S ;
reconsider t1 = s as Element of OwnSymbolsOf S by FOMODEL1:def 19;
( t1 in OwnSymbolsOf S & OwnSymbolsOf S c= dom I ) by Lm2;
hence A5: a in dom (I * ()) by ; :: thesis: ( a in dom ^^^(I * ()),^^^xx,()____ implies ^^^(I * ()),^^^xx,()____ . a in U )
reconsider tt = a as Element of AllTermsOf S by A4;
reconsider i = I . s as Interpreter of s,U ;
(S -subTerms) . tt = SubTerms t by FOMODEL1:def 39;
then reconsider y = () . tt as |.(ar t).| -element FinSequence of AllTermsOf S by FINSEQ_1:def 11;
reconsider z = xx * y as |.(ar t).| -element FinSequence of U ;
len z = |.(ar t).| by CARD_1:def 7;
then reconsider zz = z as Element of |.(ar t).| -tuples_on U by FINSEQ_2:133;
|.(ar t).| -tuples_on U c= dom (I . t1) by Lm3;
then A6: zz in dom i ;
tt in AllTermsOf S ;
then A7: tt in dom () by FUNCT_2:def 1;
assume a in dom ^^^(I * ()),^^^xx,()____ ; :: thesis: ^^^(I * ()),^^^xx,()____ . a in U
then ^^^(I * ()),^^^xx,()____ . t = ((I * ()) . t) . (^^^xx,()__ . t) by FOMODEL0:def 4
.= (I . s) . (^^^xx,()__ . t) by
.= i . zz by ;
hence ^^^(I * ()),^^^xx,()____ . a in U by ; :: thesis: verum
end;
then A8: for a being object st a in AllTermsOf S holds
a in dom (I * ()) ;
A9: dom ^^^(I * ()),^^^xx,()____ = (dom (I * ())) /\ () by
.= AllTermsOf S by ;
then for a being object st a in AllTermsOf S holds
^^^(I * ()),^^^xx,()____ . a in U by A3;
then ^^^(I * ()),^^^xx,()____ is Function of (),U by ;
hence ^^^(I * ()),^^^xx,()____ is Element of Funcs ((),U) by FUNCT_2:8; :: thesis: AllTermsOf S c= dom (I * ())
thus AllTermsOf S c= dom (I * ()) by A8; :: thesis: verum