let N be non empty with_non-empty_elements set ; :: thesis: for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = succ (IC s)
let i be Instruction of (STC N); :: thesis: for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = succ (IC s)
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies IC (Exec (i,s)) = succ (IC s) )
set M = STC N;
assume A1: InsCode i = 1 ; :: thesis: IC (Exec (i,s)) = succ (IC s)

A2: now

assume i in {[0,0,0]} ; :: thesis: contradiction
then i = [0,0,0] by TARSKI:def 1;
hence contradiction by A1, RECDEF_2:def 1; :: thesis: verum

end;

the Instructions of (STC N) = {[1,0,0],[0,0,0]} by AMISTD_1:def 7;
then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def 2;
then A3: i in {[1,0,0]} by A1, RECDEF_2:def 1, TARSKI:def 1;
A4: 0 in {0} by TARSKI:def 1;
then A5: 0 in dom (0 .--> (succ (s . 0))) by FUNCOP_1:13;
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 +* (0 .--> (succ (s . 0))) 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 7;
A8: for s being State of (STC N) holds f . s = s +* (0 .--> (succ (s . 0)))

proof

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

end;

A9: the ZeroF of (STC N) = 0 by AMISTD_1:def 7;
dom ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) = {[0,0,0]} by FUNCOP_1:13;
then the Execution of (STC N) . i = ([1,0,0] .--> f) . i by A7, A2, FUNCT_4:11
.= f by A3, FUNCOP_1:7 ;
hence IC (Exec (i,s)) = (s +* (0 .--> (succ (s . 0)))) . 0 by A9, A8
.= (0 .--> (succ (s . 0))) . 0 by A5, FUNCT_4:13
.= succ (IC s) by A9, A4, FUNCOP_1:7 ;
:: thesis: verum