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
Exec (i,s) = IncIC (s,1)
let i be Instruction of (STC N); :: thesis: for s being State of (STC N) st InsCode i = 1 holds
Exec (i,s) = IncIC (s,1)
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies Exec (i,s) = IncIC (s,1) )
set M = STC N;
assume A1: InsCode i = 1 ; :: thesis: Exec (i,s) = IncIC (s,1)

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 Def11;
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;
consider f being Function of (product the Object-Kind of (STC N)),(product the Object-Kind of (STC N)) such that
A4: for s being Element of product the Object-Kind of (STC N) holds f . s = s +* (0 .--> (succ (s . 0))) and
A5: the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) by Def11;
A6: 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 A4;
hence f . s = s +* (0 .--> (succ (s . 0))) ; :: thesis: verum

end;

A7: the ZeroF of (STC N) = 0 by Def11;
A8: Start-At (((IC s) + 1),(STC N)) = 0 .--> (succ (s . 0)) by A7, NAT_1:38;
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 A5, A2, FUNCT_4:11
.= f by A3, FUNCOP_1:7 ;
hence Exec (i,s) = IncIC (s,1) by A8, A6; :: thesis: verum