let k be Nat; :: thesis: for S being COM-Struct holds Shift ((Stop S),k) = k .--> (halt S)
let S be COM-Struct ; :: thesis: Shift ((Stop S),k) = k .--> (halt S)
A1: dom (Shift ((Stop S),k)) = { (m + k) where m is Nat : m in dom (Stop S) } by VALUED_1:def 12;
A2: 0 in dom (Stop S) by TARSKI:def 1;
A3: dom (Shift ((Stop S),k)) = {k}

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {k} c= dom (Shift ((Stop S),k))

let x be object ; :: thesis: ( x in dom (Shift ((Stop S),k)) implies x in {k} )
assume x in dom (Shift ((Stop S),k)) ; :: thesis: x in {k}
then consider m being Nat such that
A4: x = m + k and
A5: m in dom (Stop S) by A1;
m in {0} by A5;
then m = 0 by TARSKI:def 1;
hence x in {k} by A4, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {k} or x in dom (Shift ((Stop S),k)) )
assume x in {k} ; :: thesis: x in dom (Shift ((Stop S),k))
then x = 0 + k by TARSKI:def 1;
hence x in dom (Shift ((Stop S),k)) by A1, A2; :: thesis: verum

end;

A6: dom (k .--> (halt S)) = {k} ;
for x being object st x in {k} holds
(Shift ((Stop S),k)) . x = (k .--> (halt S)) . x

proof

let x be object ; :: thesis: ( x in {k} implies (Shift ((Stop S),k)) . x = (k .--> (halt S)) . x )
assume x in {k} ; :: thesis: (Shift ((Stop S),k)) . x = (k .--> (halt S)) . x
then A7: x = 0 + k by TARSKI:def 1;
0 in dom (Stop S) by TARSKI:def 1;
hence (Shift ((Stop S),k)) . x = (Stop S) . 0 by A7, VALUED_1:def 12
.= halt S
.= (k .--> (halt S)) . x by A7, FUNCOP_1:72 ;
:: thesis: verum

end;

hence Shift ((Stop S),k) = k .--> (halt S) by A3, A6, FUNCT_1:2; :: thesis: verum