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