let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being Int-Location
for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let I be Program of SCM+FSA; :: thesis: for a being Int-Location
for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let a be Int-Location ; :: thesis: for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let l be Element of NAT ; :: thesis: (s +* (Start-At (l,SCM+FSA))) . a = s . a
Start-At (l,SCM+FSA) c= I +* (Start-At (l,SCM+FSA)) by FUNCT_4:26;
then A: dom (Start-At (l,SCM+FSA)) c= dom (I +* (Start-At (l,SCM+FSA))) by RELAT_1:25;
not a in dom (Start-At (l,SCM+FSA)) by A, SCMFSA6B:12;
hence (s +* (Start-At (l,SCM+FSA))) . a = s . a by FUNCT_4:12; :: thesis: verum