:: deftheorem Def9a defines -head POLNOT_1:def 22 :
for S being Polish-language
for p, b₃ being FinSequence holds
( ( p is S -headed implies ( b₃ = S -head p iff ( b₃ in S & ex r being FinSequence st p = b₃ ^ r ) ) ) & ( not p is S -headed implies ( b₃ = S -head p iff b₃ = {} ) ) );