let S be Polish-language; :: thesis: for q being Element of S ^^ 0 holds decomp (S,0,q) = {}
let q be Element of S ^^ 0; :: thesis: decomp (S,0,q) = {}
dom (decomp (S,0,q)) = Seg 0 by Def32;
hence decomp (S,0,q) = {} ; :: thesis: verum