let D be non empty set ; for f, g being FinSequence of D
for n being Nat st not g is_substring_of f,n holds
for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
let f, g be FinSequence of D; for n being Nat st not g is_substring_of f,n holds
for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
let n be Nat; ( not g is_substring_of f,n implies for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g )
assume A1:
not g is_substring_of f,n
; for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
hence
for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
; verum