let i be Element of NAT ; :: thesis: for p1 being FinSequence
for p2 being FinSubsequence st i >= len p1 holds
p1 misses i Shift p2
let p1 be FinSequence; :: thesis: for p2 being FinSubsequence st i >= len p1 holds
p1 misses i Shift p2
let p2 be FinSubsequence; :: thesis: ( i >= len p1 implies p1 misses i Shift p2 )
assume i >= len p1 ; :: thesis: p1 misses i Shift p2
then dom p1 misses dom (i Shift p2) by Th63;
hence p1 misses i Shift p2 by Lm4; :: thesis: verum