set SS = AllSymbolsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
set ST = SubTerms t;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
reconsider TTT = AllTermsOf S as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . (SubTerms t)) by Def37;
then rng ((S -multiCat) . (SubTerms t)) c= rng t by FINSEQ_1:30;
then (S -multiCat) . (SubTerms t) is rng t -valued by RELAT_1:def 19;
hence for b₁ being Relation st b₁ = SubTerms t holds
b₁ is (rng t) * -valued by FOMODEL0:42; :: thesis: verum