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