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

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