set IT = STC N;
set Ok = the Object-Kind of (STC N);
A1: NAT in {NAT} by TARSKI:def 1;
dom (NAT .--> NAT) = {NAT} by FUNCOP_1:19;
then A2: NAT in dom (NAT .--> NAT) by TARSKI:def 1;
A3: the Instructions of (STC N) = {[1,0,0],[0,0,0]} by AMISTD_1:def 11;
let s be State of (STC N); :: according to AMI_1:def 13 :: thesis: for i being Instruction of (STC N)
for l being Element of NAT holds (Exec (i,s)) . l = s . l
let i be Instruction of (STC N); :: thesis: for l being Element of NAT holds (Exec (i,s)) . l = s . l
let l be Element of NAT ; :: thesis: (Exec (i,s)) . l = s . l
consider f being Function of (product the Object-Kind of (STC N)),(product the Object-Kind of (STC N)) such that
A6: for s being Element of product the Object-Kind of (STC N) holds f . s = s +* (NAT .--> (succ (s . NAT))) and
A7: the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) by AMISTD_1:def 11;
B6: for s being State of (STC N) holds f . s = s +* (NAT .--> (succ (s . NAT)))

proof

let s be State of (STC N); :: thesis: f . s = s +* (NAT .--> (succ (s . NAT)))
reconsider s = s as Element of product the Object-Kind of (STC N) by PBOOLE:155;
f . s = s +* (NAT .--> (succ (s . NAT))) by A6;
hence f . s = s +* (NAT .--> (succ (s . NAT))) ; :: thesis: verum

end;

reconsider ss = s as Element of product the Object-Kind of (STC N) by PBOOLE:155;
not NAT in NAT ;
then l <> NAT ;
then not l in {NAT} by TARSKI:def 1;
then A8: not l in dom (NAT .--> (succ (s . NAT))) by FUNCOP_1:19;

per cases ( i = [1,0,0] or i = [0,0,0] ) by A3, TARSKI:def 2;

suppose A9: i = [1,0,0] ; :: thesis: (Exec (i,s)) . l = s . l

then A10: i in {[1,0,0]} by TARSKI:def 1;

now

assume i in dom ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) ; :: thesis: contradiction
then i in {[0,0,0]} by FUNCOP_1:19;
then i = [0,0,0] by TARSKI:def 1;
hence contradiction by A9, MCART_1:28; :: thesis: verum

end;

then the Execution of (STC N) . i = ([1,0,0] .--> f) . i by A7, FUNCT_4:12
.= f by A10, FUNCOP_1:13 ;
hence (Exec (i,s)) . l = (s +* (NAT .--> (succ (s . NAT)))) . l by B6
.= s . l by A8, FUNCT_4:12 ;
:: thesis: verum

end;

suppose i = [0,0,0] ; :: thesis: (Exec (i,s)) . l = s . l

then A11: i in {[0,0,0]} by TARSKI:def 1;
then i in dom ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) by FUNCOP_1:19;
then the Execution of (STC N) . i = ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) . i by A7, FUNCT_4:14
.= id (product the Object-Kind of (STC N)) by A11, FUNCOP_1:13 ;
then ( the Execution of (STC N) . i) . ss = ss by FUNCT_1:35;
hence (Exec (i,s)) . l = s . l ; :: thesis: verum

end;

end;