let S be Polish-language; :: thesis: for s being FinSequence holds
( s is S ^^ 0 -headed & (S ^^ 0) -head s = {} & (S ^^ 0) -tail s = s )
let s be FinSequence; :: thesis: ( s is S ^^ 0 -headed & (S ^^ 0) -head s = {} & (S ^^ 0) -tail s = s )
A1: s = {} ^ s by FINSEQ_1:34;
{} in S ^^ 0 by Th4;
hence ( s is S ^^ 0 -headed & (S ^^ 0) -head s = {} & (S ^^ 0) -tail s = s ) by A1, Th52; :: thesis: verum