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