let s be State of SCM+FSA; :: thesis: for a being Int-Location
for l being Nat holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let a be Int-Location; :: thesis: for l being Nat holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let l be Nat; :: thesis: (s +* (Start-At (l,SCM+FSA))) . a = s . a
not a in dom (Start-At (l,SCM+FSA)) by SCMFSA_2:102;
hence (s +* (Start-At (l,SCM+FSA))) . a = s . a by FUNCT_4:11; :: thesis: verum