set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set n = |.(ar s).|;
set D = |.(ar s).| -tuples_on (AllTermsOf S);
set f = s -compound ;
set IT = (s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S));
now :: thesis: for y being object st y in rng ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) holds
y in AllTermsOf S
let y be object ; :: thesis: ( y in rng ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) implies y in AllTermsOf S )
assume y in rng ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) ; :: thesis: y in AllTermsOf S
then y in (s -compound) .: (|.(ar s).| -tuples_on (AllTermsOf S)) ;
then consider x being object such that
A1: ( x in dom (s -compound) & x in |.(ar s).| -tuples_on (AllTermsOf S) & y = (s -compound) . x ) by FUNCT_1:def 6;
reconsider V = x as |.(ar s).| -element FinSequence of AllTermsOf S by FOMODEL0:12, A1;
reconsider VV = V as |.(ar s).| -element Element of (AllTermsOf S) * ;
reconsider Ss = ((AllSymbolsOf S) *) \ {{}} as Subset of ((AllSymbolsOf S) *) ;
VV is Element of Ss * ;
then ( s -compound VV is termal string of S & VV is Element of ((AllSymbolsOf S) *) * ) ;
then (s -compound) . VV is termal string of S by Def2;
hence y in AllTermsOf S by FOMODEL1:def 32, A1; :: thesis: verum
end;
hence (s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is AllTermsOf S -valued by RELAT_1:def 19, TARSKI:def 3; :: thesis: verum