(<*s*> ^ w1) ^ w2 = <*s*> ^ (w1 ^ w2) by FINSEQ_1:32;
hence for b₁ being string of S st b₁ = (<*s*> ^ w1) ^ w2 holds
not b₁ is 0wff ; :: thesis: verum