let S be Polish-language; :: thesis: for s being FinSequence st s in S holds
( S -head s = s & S -tail s = {} )
let s be FinSequence; :: thesis: ( s in S implies ( S -head s = s & S -tail s = {} ) )
assume s in S ; :: thesis: ( S -head s = s & S -tail s = {} )
then ( S -head (s ^ {}) = s & S -tail (s ^ {}) = {} ) by Th52;
hence ( S -head s = s & S -tail s = {} ) by FINSEQ_1:34; :: thesis: verum