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 14, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } by XBOOLE_0:def 3;
then I in (SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 14, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ) \/ { [K,{},<*dC,fB*>] where K is Element of Segm 14, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } by XBOOLE_0:def 3;
hence I is Instruction of SCM+FSA by XBOOLE_0:def 3; :: thesis: verum