let f be FinSequence of NAT ; :: thesis: for tm1, tm2 being TuringStr
for t1 being Tape of tm1
for t2 being Tape of tm2 st t1 = t2 & t1 storeData f holds
t2 storeData f
let tm1, tm2 be TuringStr ; :: thesis: for t1 being Tape of tm1
for t2 being Tape of tm2 st t1 = t2 & t1 storeData f holds
t2 storeData f
let t1 be Tape of tm1; :: thesis: for t2 being Tape of tm2 st t1 = t2 & t1 storeData f holds
t2 storeData f
let t2 be Tape of tm2; :: thesis: ( t1 = t2 & t1 storeData f implies t2 storeData f )
assume that
A1: t1 = t2 and
A2: t1 storeData f ; :: thesis: t2 storeData f

now :: thesis: for i being Nat st 1 <= i & i < len f holds
t2 is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i)

let i be Nat; :: thesis: ( 1 <= i & i < len f implies t2 is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i) )
set m = (Sum (Prefix (f,i))) + (2 * (i - 1));
set n = (Sum (Prefix (f,(i + 1)))) + (2 * i);
assume ( 1 <= i & i < len f ) ; :: thesis: t2 is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i)
then A3: t1 is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i) by A2;
then A4: for k being Integer st (Sum (Prefix (f,i))) + (2 * (i - 1)) < k & k < (Sum (Prefix (f,(i + 1)))) + (2 * i) holds
t1 . k = 1 ;
( t1 . ((Sum (Prefix (f,i))) + (2 * (i - 1))) = 0 & t1 . ((Sum (Prefix (f,(i + 1)))) + (2 * i)) = 0 ) by A3;
hence t2 is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i) by A1, A4; :: thesis: verum

end;

hence t2 storeData f ; :: thesis: verum