let S be Polish-language; :: thesis: for q being Element of S ^^ 1 holds decomp (S,1,q) = <*q*>
let q be Element of S ^^ 1; :: thesis: decomp (S,1,q) = <*q*>
set w = decomp (S,1,q);
1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then consider k being Nat such that
A2: 1 = k + 1 and
A3: (decomp (S,1,q)) . 1 = S -head ((S ^^ k) -tail q) by Def32;
(decomp (S,1,q)) . 1 = S -head q by A2, A3, Th58
.= q ;
hence decomp (S,1,q) = <*q*> by Th62, FINSEQ_1:40; :: thesis: verum