set ww = <*l*> ^ w;
set F = S -firstChar ;
(S -firstChar) . (<*l*> ^ w) = (<*l*> ^ w) . 1 by FOMODEL0:6
.= l by FINSEQ_1:41 ;
hence for b₁ being string of S st b₁ = <*l*> ^ w holds
b₁ is exal ; :: thesis: verum