set FC = S -firstChar ;
set IT = <*s*> ^ w;
set SS = AllSymbolsOf S;
(S -firstChar) . (<*s*> ^ w) = (<*s*> ^ w) . 1 by FOMODEL0:6
.= s by FINSEQ_1:41 ;
hence for b₁ being string of S st b₁ = <*s*> ^ w holds
not b₁ is 0wff ; :: thesis: verum