set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set n = abs (ar s);
set D = (abs (ar s)) -tuples_on (AllTermsOf S);
set f = s -compound ;
set IT = (s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S));

now

let y be set ; :: thesis: ( y in rng ((s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S))) implies y in AllTermsOf S )
assume y in rng ((s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S))) ; :: thesis: y in AllTermsOf S
then y in (s -compound) .: ((abs (ar s)) -tuples_on (AllTermsOf S)) by RELAT_1:115;
then consider x being set such that
C1: ( x in dom (s -compound) & x in (abs (ar s)) -tuples_on (AllTermsOf S) & y = (s -compound) . x ) by FUNCT_1:def 6;
reconsider V = x as abs (ar s) -element FinSequence of AllTermsOf S by C1, FOMODEL0:12;
reconsider VV = V as abs (ar s) -element Element of (AllTermsOf S) * by FINSEQ_1:def 11;
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 DefCompound1;
hence y in AllTermsOf S by C1, FOMODEL1:def 32; :: thesis: verum

end;

then rng ((s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S))) c= AllTermsOf S by TARSKI:def 3;
hence (s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) is AllTermsOf S -valued by RELAT_1:def 19; :: thesis: verum