let S be Polish-language; :: thesis: for s, t being FinSequence st s is S -headed holds
( s ^ t is S -headed & S -head (s ^ t) = S -head s & S -tail (s ^ t) = (S -tail s) ^ t )
let s, t be FinSequence; :: thesis: ( s is S -headed implies ( s ^ t is S -headed & S -head (s ^ t) = S -head s & S -tail (s ^ t) = (S -tail s) ^ t ) )
assume s is S -headed ; :: thesis: ( s ^ t is S -headed & S -head (s ^ t) = S -head s & S -tail (s ^ t) = (S -tail s) ^ t )
then consider q, r being FinSequence such that
A1: q in S and
A2: s = q ^ r ;
A3: s ^ t = q ^ (r ^ t) by A2, FINSEQ_1:32;
hence s ^ t is S -headed by A1; :: thesis: ( S -head (s ^ t) = S -head s & S -tail (s ^ t) = (S -tail s) ^ t )
thus S -head (s ^ t) = q by A1, A3, Th52
.= S -head s by A1, A2, Th52 ; :: thesis: S -tail (s ^ t) = (S -tail s) ^ t
thus S -tail (s ^ t) = r ^ t by A1, A3, Th52
.= (S -tail s) ^ t by A1, A2, Th52 ; :: thesis: verum