let tm be TuringStr ; :: thesis: for t being Tape of tm
for h being Integer
for s being Symbol of tm
for i being object 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 object 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 object 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 object holds
( (Tape-Chg (t,h,s)) . h = s & ( i <> h implies (Tape-Chg (t,h,s)) . i = t . i ) )
let i be object ; :: 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:94; :: thesis: ( i <> h implies (Tape-Chg (t,h,s)) . i = t . i )
assume i <> h ; :: thesis: (Tape-Chg (t,h,s)) . i = t . i
then not i in dom (h .--> s) by TARSKI:def 1;
hence (Tape-Chg (t,h,s)) . i = t . i by FUNCT_4:11; :: thesis: verum