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