set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
consider s being relational Element of S, V being |.(ar s).| -element Element of (AllTermsOf S) * such that
A1: phi = <*s*> ^ ((S -multiCat) . V) by Def35;
reconsider ss = s as Element of AllSymbolsOf S ;
reconsider head = <*ss*> as FinSequence of AllSymbolsOf S ;
reconsider tail = (S -multiCat) . V as FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
(S -firstChar) . phi = (head ^ tail) . 1 by A1, FOMODEL0:6
.= s by FINSEQ_1:41 ;
hence for b₁ being Element of S st b₁ = (S -firstChar) . phi holds
b₁ is relational ; :: thesis: verum