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:98; :: thesis: verum