let f be non empty FinSequence of the Instructions of SCM+FSA ; :: thesis: ( 1 in dom f & insloc 0 in dom (Load f) )
A1: dom (Load f) = { (m -' 1) where m is Element of NAT : m in dom f } by Def1;
thus 1 in dom f by FINSEQ_5:6; :: thesis: insloc 0 in dom (Load f)
then insloc (1 -' 1) in dom (Load f) by A1;
hence insloc 0 in dom (Load f) by XREAL_1:234; :: thesis: verum