let S, T be Polish-language; 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; ( 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
; ( 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, Th17
.=
T -head u
by A1, A3, A4, Th17
; S -tail u = T -tail u
thus S -tail u =
r
by A3, A4, Th17
.=
T -tail u
by A1, A3, A4, Th17
; verum