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;
A2: (S -firstChar) . phi = (head ^ tail) . 1 by A1, FOMODEL0:6
.= s by FINSEQ_1:41 ;
reconsider VV = V as |.(ar ((S -firstChar) . phi)).| -element Element of (AllTermsOf S) * by A2;
take VV ; :: thesis: phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . VV)
thus phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . VV) by A2, A1; :: thesis: verum