let T be TuringStr ; :: thesis: for t being Tape of T
for h being Integer
for s being Symbol of T st t . h = s holds
Tape-Chg (t,h,s) = t
let t be Tape of T; :: thesis: for h being Integer
for s being Symbol of T st t . h = s holds
Tape-Chg (t,h,s) = t
let h be Integer; :: thesis: for s being Symbol of T st t . h = s holds
Tape-Chg (t,h,s) = t
let s be Symbol of T; :: thesis: ( t . h = s implies Tape-Chg (t,h,s) = t )
ex f being Function st
( t = f & dom f = INT & rng f c= the Symbols of T ) by FUNCT_2:def 2;
then A1: h in dom t by INT_1:def 2;
assume t . h = s ; :: thesis: Tape-Chg (t,h,s) = t
hence Tape-Chg (t,h,s) = t by A1, FUNCT_7:96; :: thesis: verum