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));

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

hence
(s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is AllTermsOf S -valued
by RELAT_1:def 19, TARSKI:def 3; :: thesis: verumy 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;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