let S be Polish-language; :: thesis: for s, t being FinSequence st s in S holds
( S -head (s ^ t) = s & S -tail (s ^ t) = t )
let s, t be FinSequence; :: thesis: ( s in S implies ( S -head (s ^ t) = s & S -tail (s ^ t) = t ) )
assume A1: s in S ; :: thesis: ( S -head (s ^ t) = s & S -tail (s ^ t) = t )
set u = s ^ t;
s ^ t is S -headed by A1;
hence S -head (s ^ t) = s by A1, Def22; :: thesis: S -tail (s ^ t) = t
hence S -tail (s ^ t) = t by Def23; :: thesis: verum