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

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