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