let I be Instruction of SCM; :: thesis: I is Instruction of SCM+FSA
I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } by XBOOLE_0:def 3;
hence I is Instruction of SCM+FSA by XBOOLE_0:def 3; :: thesis: verum