let tm be TuringStr ; :: thesis: for t being Tape of tm
for h being Integer
for s being Symbol of tm
for i being set holds
( (Tape-Chg t,h,s) . h = s & ( i <> h implies (Tape-Chg t,h,s) . i = t . i ) )
let t be Tape of tm; :: thesis: for h being Integer
for s being Symbol of tm
for i being set holds
( (Tape-Chg t,h,s) . h = s & ( i <> h implies (Tape-Chg t,h,s) . i = t . i ) )
let h be Integer; :: thesis: for s being Symbol of tm
for i being set holds
( (Tape-Chg t,h,s) . h = s & ( i <> h implies (Tape-Chg t,h,s) . i = t . i ) )
let s be Symbol of tm; :: thesis: for i being set holds
( (Tape-Chg t,h,s) . h = s & ( i <> h implies (Tape-Chg t,h,s) . i = t . i ) )
let i be set ; :: thesis: ( (Tape-Chg t,h,s) . h = s & ( i <> h implies (Tape-Chg t,h,s) . i = t . i ) )
set t1 = Tape-Chg t,h,s;
set p = h .--> s;
thus (Tape-Chg t,h,s) . h = s by FUNCT_7:96; :: thesis: ( i <> h implies (Tape-Chg t,h,s) . i = t . i )
A1: dom (h .--> s) = {h} by FUNCOP_1:19;
assume i <> h ; :: thesis: (Tape-Chg t,h,s) . i = t . i
then not i in dom (h .--> s) by A1, TARSKI:def 1;
hence (Tape-Chg t,h,s) . i = t . i by FUNCT_4:12; :: thesis: verum