let i be Nat; :: thesis: for p1 being FinSequence
for p2 being FinSubsequence st i >= len p1 holds
p1 misses Shift (p2,i)
let p1 be FinSequence; :: thesis: for p2 being FinSubsequence st i >= len p1 holds
p1 misses Shift (p2,i)
let p2 be FinSubsequence; :: thesis: ( i >= len p1 implies p1 misses Shift (p2,i) )
assume i >= len p1 ; :: thesis: p1 misses Shift (p2,i)
then dom p1 misses dom (Shift (p2,i)) by Th47;
hence p1 misses Shift (p2,i) by RELAT_1:179; :: thesis: verum