let T be TuringStr ; :: thesis: for t being Tape of T
for s, n being Element of NAT st t storeData <*s,n*> holds
( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )

let t be Tape of T; :: thesis: for s, n being Element of NAT st t storeData <*s,n*> holds
( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )

let s, n be Element of NAT ; :: thesis: ( t storeData <*s,n*> implies ( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) ) )

assume t storeData <*s,n*> ; :: thesis: ( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )

then A1: t is_1_between s,(s + n) + 2 by Th15;
hence ( t . s = 0 & t . ((s + n) + 2) = 0 ) ; :: thesis: for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1

thus for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 by A1; :: thesis: verum