let S be Polish-language; :: thesis: for m, n being Nat
for s being FinSequence st m + 1 <= n & s in S ^^ n holds
( s is S ^^ m -headed & (S ^^ m) -tail s is S -headed )
let m, n be Nat; :: thesis: for s being FinSequence st m + 1 <= n & s in S ^^ n holds
( s is S ^^ m -headed & (S ^^ m) -tail s is S -headed )
let s be FinSequence; :: thesis: ( m + 1 <= n & s in S ^^ n implies ( s is S ^^ m -headed & (S ^^ m) -tail s is S -headed ) )
assume that
A1: m + 1 <= n and
A2: s in S ^^ n ; :: thesis: ( s is S ^^ m -headed & (S ^^ m) -tail s is S -headed )
consider l being Nat such that
A3: (m + 1) + l = n by A1, NAT_1:10;
A4: m + (1 + l) = n by A3;
then S ^^ n is S ^^ m -headed by Th51;
hence s is S ^^ m -headed by A2; :: thesis: (S ^^ m) -tail s is S -headed
set u = (S ^^ m) -tail s;
s in (S ^^ m) ^ (S ^^ (1 + l)) by A2, A4, Th10;
then (S ^^ m) -tail s in S ^^ (1 + l) by Th54;
then A6: (S ^^ m) -tail s in (S ^^ 1) ^ (S ^^ l) by Th10;
S ^ (S ^^ l) is S -headed ;
hence (S ^^ m) -tail s is S -headed by A6; :: thesis: verum