let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for iloc, a being Element of NAT holds s . a = (s +* (Start-At (iloc,S))) . a
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for iloc, a being Element of NAT holds s . a = (s +* (Start-At (iloc,S))) . a
let s be State of S; :: thesis: for iloc, a being Element of NAT holds s . a = (s +* (Start-At (iloc,S))) . a
let iloc, a be Element of NAT ; :: thesis: s . a = (s +* (Start-At (iloc,S))) . a
A1: a in NAT ;
NAT c= the carrier of S by Def2;
then a in the carrier of S by A1;
then a in dom s by PARTFUN1:def 4;
then A2: ( dom (Start-At (iloc,S)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,S))) ) by FUNCOP_1:19, XBOOLE_0:def 3;
a <> IC by Def12;
then not a in {(IC )} by TARSKI:def 1;
hence s . a = (s +* (Start-At (iloc,S))) . a by A2, FUNCT_4:def 1; :: thesis: verum