let S, T be Polish-language; :: thesis: for p being FinSequence st S -head p in T holds
( p is T -headed & S -head p = T -head p )
let p be FinSequence; :: thesis: ( S -head p in T implies ( p is T -headed & S -head p = T -head p ) )
set q = S -head p;
set r = S -tail p;
assume A1: S -head p in T ; :: thesis: ( p is T -headed & S -head p = T -head p )
p = (S -head p) ^ (S -tail p) ;
hence ( p is T -headed & S -head p = T -head p ) by A1, POLNOT_1:52; :: thesis: verum